DL0094 — signed_recursive_determinant_integer_invariant

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

∀ d. ∀ x. ∀ y. ∀ z. ∀ n. ∀ m. ∀ k. ∀ i. ∀ j. ∀ u. ∀ v. ∀ w. ∀ x0. IntegerMatrixEntrywiseEqual(x,y,z,n,m,k,i,j,d,d) → SignedRecursiveDeterminant(x,y,z,n,d,u,v) → SignedRecursiveDeterminant(m,k,i,j,d,w,x0) → u + x0 = w + v

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

Definition DAG

SignedAlternatingCofactorFold(ab,ac,db,dc,eb,ec,fb,fc,l,p,n) · 2 SignedRecursiveDeterminant(pb,pc,nb,nc,d,p,n) · 2 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) · 1

Actual proof prerequisites

signed_recursive_determinant_zero_value signed_recursive_determinant_successor_decomposition matrix_integer_cofactor_streams_from_recursion matrix_integer_first_row_equality matrix_integer_cofactor_fold_balance

Original expanded first-order statement

forall d. (forall mdr_ab_determinant_integer_invariance mdr_ac_determinant_integer_invariance mdr_bb_determinant_integer_invariance mdr_bc_determinant_integer_invariance mdr_eb_determinant_integer_invariance mdr_ec_determinant_integer_invariance mdr_fb_determinant_integer_invariance mdr_fc_determinant_integer_invariance mdr_p_determinant_integer_invariance mdr_n_determinant_integer_invariance mdr_P_determinant_integer_invariance mdr_N_determinant_integer_invariance. (forall ics_index_determinant_integer_invarianceentries ics_value0_determinant_integer_invarianceentries ics_value1_determinant_integer_invarianceentries ics_value2_determinant_integer_invarianceentries ics_value3_determinant_integer_invarianceentries. (exists ics_gap_determinant_integer_invarianceentries_bound. ics_gap_determinant_integer_invarianceentries_bound + S (ics_index_determinant_integer_invarianceentries) = ((d) * (d))) -> (((exists fs_h_ics_determinant_integer_invarianceentries_at0. fs_h_ics_determinant_integer_invarianceentries_at0 + S (ics_value0_determinant_integer_invarianceentries) = S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_ac_determinant_integer_invariance)) /\ exists fs_q_ics_determinant_integer_invarianceentries_at0. mdr_ab_determinant_integer_invariance = fs_q_ics_determinant_integer_invarianceentries_at0 * S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_ac_determinant_integer_invariance) + (ics_value0_determinant_integer_invarianceentries))) -> (((exists fs_h_ics_determinant_integer_invarianceentries_at1. fs_h_ics_determinant_integer_invarianceentries_at1 + S (ics_value1_determinant_integer_invarianceentries) = S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_bc_determinant_integer_invariance)) /\ exists fs_q_ics_determinant_integer_invarianceentries_at1. mdr_bb_determinant_integer_invariance = fs_q_ics_determinant_integer_invarianceentries_at1 * S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_bc_determinant_integer_invariance) + (ics_value1_determinant_integer_invarianceentries))) -> (((exists fs_h_ics_determinant_integer_invarianceentries_at2. fs_h_ics_determinant_integer_invarianceentries_at2 + S (ics_value2_determinant_integer_invarianceentries) = S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_ec_determinant_integer_invariance)) /\ exists fs_q_ics_determinant_integer_invarianceentries_at2. mdr_eb_determinant_integer_invariance = fs_q_ics_determinant_integer_invarianceentries_at2 * S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_ec_determinant_integer_invariance) + (ics_value2_determinant_integer_invarianceentries))) -> (((exists fs_h_ics_determinant_integer_invarianceentries_at3. fs_h_ics_determinant_integer_invarianceentries_at3 + S (ics_value3_determinant_integer_invarianceentries) = S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_fc_determinant_integer_invariance)) /\ exists fs_q_ics_determinant_integer_invarianceentries_at3. mdr_fb_determinant_integer_invariance = fs_q_ics_determinant_integer_invarianceentries_at3 * S ((S (ics_index_determinant_integer_invarianceentries)) * mdr_fc_determinant_integer_invariance) + (ics_value3_determinant_integer_invarianceentries))) -> ics_value0_determinant_integer_invarianceentries + ics_value3_determinant_integer_invarianceentries = ics_value2_determinant_integer_invarianceentries + ics_value1_determinant_integer_invarianceentries) -> (exists mdr_b_determinant_integer_invariancefirst mdr_c_determinant_integer_invariancefirst mdr_l_determinant_integer_invariancefirst mdr_i_determinant_integer_invariancefirst. ((forall mdr_i_determinant_integer_invariancefirsth. (exists mdr_gap_determinant_integer_invariancefirsthi. mdr_gap_determinant_integer_invariancefirsthi + S (mdr_i_determinant_integer_invariancefirsth) = (mdr_l_determinant_integer_invariancefirst)) -> exists mdr_d_determinant_integer_invariancefirsth mdr_pb_determinant_integer_invariancefirsth mdr_pc_determinant_integer_invariancefirsth mdr_nb_determinant_integer_invariancefirsth mdr_nc_determinant_integer_invariancefirsth mdr_p_determinant_integer_invariancefirsth mdr_n_determinant_integer_invariancefirsth. ((exists mdr_z_determinant_integer_invariancefirsthr. ((exists mdr_a_determinant_integer_invariancefirsthrc mdr_b_determinant_integer_invariancefirsthrc mdr_c_determinant_integer_invariancefirsthrc mdr_e_determinant_integer_invariancefirsthrc mdr_f_determinant_integer_invariancefirsthrc. ((mdr_a_determinant_integer_invariancefirsthrc = ((mdr_d_determinant_integer_invariancefirsth) + (mdr_pb_determinant_integer_invariancefirsth)) * S ((mdr_d_determinant_integer_invariancefirsth) + (mdr_pb_determinant_integer_invariancefirsth)) + ((mdr_pb_determinant_integer_invariancefirsth) + (mdr_pb_determinant_integer_invariancefirsth))) /\ ((mdr_b_determinant_integer_invariancefirsthrc = ((mdr_pc_determinant_integer_invariancefirsth) + (mdr_nb_determinant_integer_invariancefirsth)) * S ((mdr_pc_determinant_integer_invariancefirsth) + (mdr_nb_determinant_integer_invariancefirsth)) + ((mdr_nb_determinant_integer_invariancefirsth) + (mdr_nb_determinant_integer_invariancefirsth))) /\ ((mdr_c_determinant_integer_invariancefirsthrc = ((mdr_a_determinant_integer_invariancefirsthrc) + (mdr_b_determinant_integer_invariancefirsthrc)) * S ((mdr_a_determinant_integer_invariancefirsthrc) + (mdr_b_determinant_integer_invariancefirsthrc)) + ((mdr_b_determinant_integer_invariancefirsthrc) + (mdr_b_determinant_integer_invariancefirsthrc))) /\ ((mdr_e_determinant_integer_invariancefirsthrc = ((mdr_p_determinant_integer_invariancefirsth) + (mdr_n_determinant_integer_invariancefirsth)) * S ((mdr_p_determinant_integer_invariancefirsth) + (mdr_n_determinant_integer_invariancefirsth)) + ((mdr_n_determinant_integer_invariancefirsth) + (mdr_n_determinant_integer_invariancefirsth))) /\ ((mdr_f_determinant_integer_invariancefirsthrc = ((mdr_nc_determinant_integer_invariancefirsth) + (mdr_e_determinant_integer_invariancefirsthrc)) * S ((mdr_nc_determinant_integer_invariancefirsth) + (mdr_e_determinant_integer_invariancefirsthrc)) + ((mdr_e_determinant_integer_invariancefirsthrc) + (mdr_e_determinant_integer_invariancefirsthrc))) /\ ((mdr_z_determinant_integer_invariancefirsthr) = ((mdr_c_determinant_integer_invariancefirsthrc) + (mdr_f_determinant_integer_invariancefirsthrc)) * S ((mdr_c_determinant_integer_invariancefirsthrc) + (mdr_f_determinant_integer_invariancefirsthrc)) + ((mdr_f_determinant_integer_invariancefirsthrc) + (mdr_f_determinant_integer_invariancefirsthrc))))))))) /\ (((exists ff_h_mdr_determinant_integer_invariancefirsthrb. ff_h_mdr_determinant_integer_invariancefirsthrb + S (mdr_z_determinant_integer_invariancefirsthr) = S ((S (mdr_i_determinant_integer_invariancefirsth)) * mdr_c_determinant_integer_invariancefirst)) /\ exists ff_q_mdr_determinant_integer_invariancefirsthrb. mdr_b_determinant_integer_invariancefirst = ff_q_mdr_determinant_integer_invariancefirsthrb * S ((S (mdr_i_determinant_integer_invariancefirsth)) * mdr_c_determinant_integer_invariancefirst) + (mdr_z_determinant_integer_invariancefirsthr))))) /\ (((((mdr_d_determinant_integer_invariancefirsth) = 0) /\ (((mdr_p_determinant_integer_invariancefirsth) = 1) /\ ((mdr_n_determinant_integer_invariancefirsth) = 0))) \/ exists mdr_q_determinant_integer_invariancefirsths mdr_eb_determinant_integer_invariancefirsths mdr_ec_determinant_integer_invariancefirsths mdr_fb_determinant_integer_invariancefirsths mdr_fc_determinant_integer_invariancefirsths. (((mdr_d_determinant_integer_invariancefirsth) = S (mdr_q_determinant_integer_invariancefirsths)) /\ ((forall mdr_j_determinant_integer_invariancefirsthsc. (exists mdr_gap_determinant_integer_invariancefirsthscj. mdr_gap_determinant_integer_invariancefirsthscj + S (mdr_j_determinant_integer_invariancefirsthsc) = (S (mdr_q_determinant_integer_invariancefirsths))) -> exists mdr_i_determinant_integer_invariancefirsthsc mdr_up_determinant_integer_invariancefirsthsc mdr_us_determinant_integer_invariancefirsthsc mdr_un_determinant_integer_invariancefirsthsc mdr_ut_determinant_integer_invariancefirsthsc mdr_p_determinant_integer_invariancefirsthsc mdr_n_determinant_integer_invariancefirsthsc. ((exists mdr_gap_determinant_integer_invariancefirsthsci. mdr_gap_determinant_integer_invariancefirsthsci + S (mdr_i_determinant_integer_invariancefirsthsc) = (mdr_i_determinant_integer_invariancefirsth)) /\ ((exists mdr_z_determinant_integer_invariancefirsthscr. ((exists mdr_a_determinant_integer_invariancefirsthscrc mdr_b_determinant_integer_invariancefirsthscrc mdr_c_determinant_integer_invariancefirsthscrc mdr_e_determinant_integer_invariancefirsthscrc mdr_f_determinant_integer_invariancefirsthscrc. ((mdr_a_determinant_integer_invariancefirsthscrc = ((mdr_q_determinant_integer_invariancefirsths) + (mdr_up_determinant_integer_invariancefirsthsc)) * S ((mdr_q_determinant_integer_invariancefirsths) + (mdr_up_determinant_integer_invariancefirsthsc)) + ((mdr_up_determinant_integer_invariancefirsthsc) + (mdr_up_determinant_integer_invariancefirsthsc))) /\ ((mdr_b_determinant_integer_invariancefirsthscrc = ((mdr_us_determinant_integer_invariancefirsthsc) + (mdr_un_determinant_integer_invariancefirsthsc)) * S ((mdr_us_determinant_integer_invariancefirsthsc) + (mdr_un_determinant_integer_invariancefirsthsc)) + ((mdr_un_determinant_integer_invariancefirsthsc) + (mdr_un_determinant_integer_invariancefirsthsc))) /\ ((mdr_c_determinant_integer_invariancefirsthscrc = ((mdr_a_determinant_integer_invariancefirsthscrc) + (mdr_b_determinant_integer_invariancefirsthscrc)) * S ((mdr_a_determinant_integer_invariancefirsthscrc) + (mdr_b_determinant_integer_invariancefirsthscrc)) + ((mdr_b_determinant_integer_invariancefirsthscrc) + (mdr_b_determinant_integer_invariancefirsthscrc))) /\ ((mdr_e_determinant_integer_invariancefirsthscrc = ((mdr_p_determinant_integer_invariancefirsthsc) + (mdr_n_determinant_integer_invariancefirsthsc)) * S ((mdr_p_determinant_integer_invariancefirsthsc) + (mdr_n_determinant_integer_invariancefirsthsc)) + ((mdr_n_determinant_integer_invariancefirsthsc) + (mdr_n_determinant_integer_invariancefirsthsc))) /\ ((mdr_f_determinant_integer_invariancefirsthscrc = ((mdr_ut_determinant_integer_invariancefirsthsc) + (mdr_e_determinant_integer_invariancefirsthscrc)) * S ((mdr_ut_determinant_integer_invariancefirsthsc) + (mdr_e_determinant_integer_invariancefirsthscrc)) + ((mdr_e_determinant_integer_invariancefirsthscrc) + (mdr_e_determinant_integer_invariancefirsthscrc))) /\ ((mdr_z_determinant_integer_invariancefirsthscr) = ((mdr_c_determinant_integer_invariancefirsthscrc) + (mdr_f_determinant_integer_invariancefirsthscrc)) * S ((mdr_c_determinant_integer_invariancefirsthscrc) + (mdr_f_determinant_integer_invariancefirsthscrc)) + ((mdr_f_determinant_integer_invariancefirsthscrc) + (mdr_f_determinant_integer_invariancefirsthscrc))))))))) /\ (((exists ff_h_mdr_determinant_integer_invariancefirsthscrb. ff_h_mdr_determinant_integer_invariancefirsthscrb + S (mdr_z_determinant_integer_invariancefirsthscr) = S ((S (mdr_i_determinant_integer_invariancefirsthsc)) * mdr_c_determinant_integer_invariancefirst)) /\ exists ff_q_mdr_determinant_integer_invariancefirsthscrb. mdr_b_determinant_integer_invariancefirst = ff_q_mdr_determinant_integer_invariancefirsthscrb * S ((S (mdr_i_determinant_integer_invariancefirsthsc)) * mdr_c_determinant_integer_invariancefirst) + (mdr_z_determinant_integer_invariancefirsthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive. (exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_index_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) = ((mdr_q_determinant_integer_invariancefirsths) * (mdr_q_determinant_integer_invariancefirsths))) -> exists ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive. (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive = (mdr_q_determinant_integer_invariancefirsths) * ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive + ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_column_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) = (mdr_q_determinant_integer_invariancefirsths)) /\ ((exists ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell = ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell = S ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) = (mdr_j_determinant_integer_invariancefirsthsc)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell = ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_positive_cell_column_after + (mdr_j_determinant_integer_invariancefirsthsc) = (ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell = S ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_positive_cell_source. ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell) * (S (mdr_q_determinant_integer_invariancefirsths)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell))) * mdr_pc_determinant_integer_invariancefirsth)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_positive_cell_source. mdr_pb_determinant_integer_invariancefirsth = ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell) * (S (mdr_q_determinant_integer_invariancefirsths)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_positive_cell))) * mdr_pc_determinant_integer_invariancefirsth) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_positive_target. ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_positive_target + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive)) * mdr_us_determinant_integer_invariancefirsthsc)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_positive_target. mdr_up_determinant_integer_invariancefirsthsc = ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive)) * mdr_us_determinant_integer_invariancefirsthsc) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative. (exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_index_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) = ((mdr_q_determinant_integer_invariancefirsths) * (mdr_q_determinant_integer_invariancefirsths))) -> exists ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative. (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative = (mdr_q_determinant_integer_invariancefirsths) * ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative + ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_column_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) = (mdr_q_determinant_integer_invariancefirsths)) /\ ((exists ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell = ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell = S ff_row_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancefirsthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) = (mdr_j_determinant_integer_invariancefirsthsc)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell = ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_determinant_integer_invariancefirsthscm_negative_cell_column_after + (mdr_j_determinant_integer_invariancefirsthsc) = (ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell = S ff_column_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_negative_cell_source. ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell) * (S (mdr_q_determinant_integer_invariancefirsths)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell))) * mdr_nc_determinant_integer_invariancefirsth)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_negative_cell_source. mdr_nb_determinant_integer_invariancefirsth = ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell) * (S (mdr_q_determinant_integer_invariancefirsths)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancefirsthscm_negative_cell))) * mdr_nc_determinant_integer_invariancefirsth) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_negative_target. ff_h_mdm_mdr_determinant_integer_invariancefirsthscm_negative_target + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative)) * mdr_ut_determinant_integer_invariancefirsthsc)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_negative_target. mdr_un_determinant_integer_invariancefirsthsc = ff_q_mdm_mdr_determinant_integer_invariancefirsthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative)) * mdr_ut_determinant_integer_invariancefirsthsc) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancefirsthscm_negative))))))))) /\ ((((exists ff_h_mdr_determinant_integer_invariancefirsthscp. ff_h_mdr_determinant_integer_invariancefirsthscp + S (mdr_p_determinant_integer_invariancefirsthsc) = S ((S (mdr_j_determinant_integer_invariancefirsthsc)) * mdr_ec_determinant_integer_invariancefirsths)) /\ exists ff_q_mdr_determinant_integer_invariancefirsthscp. mdr_eb_determinant_integer_invariancefirsths = ff_q_mdr_determinant_integer_invariancefirsthscp * S ((S (mdr_j_determinant_integer_invariancefirsthsc)) * mdr_ec_determinant_integer_invariancefirsths) + (mdr_p_determinant_integer_invariancefirsthsc))) /\ (((exists ff_h_mdr_determinant_integer_invariancefirsthscn. ff_h_mdr_determinant_integer_invariancefirsthscn + S (mdr_n_determinant_integer_invariancefirsthsc) = S ((S (mdr_j_determinant_integer_invariancefirsthsc)) * mdr_fc_determinant_integer_invariancefirsths)) /\ exists ff_q_mdr_determinant_integer_invariancefirsthscn. mdr_fb_determinant_integer_invariancefirsths = ff_q_mdr_determinant_integer_invariancefirsthscn * S ((S (mdr_j_determinant_integer_invariancefirsthsc)) * mdr_fc_determinant_integer_invariancefirsths) + (mdr_n_determinant_integer_invariancefirsthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_determinant_integer_invariancefirsthsf ff_uc_mce_fold_mdr_determinant_integer_invariancefirsthsf ff_vb_mce_fold_mdr_determinant_integer_invariancefirsthsf ff_vc_mce_fold_mdr_determinant_integer_invariancefirsthsf. ((forall ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix. (exists ff_gap_mce_mdr_determinant_integer_invariancefirsthsf_prefix_index. ff_gap_mce_mdr_determinant_integer_invariancefirsthsf_prefix_index + S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) = (S (mdr_q_determinant_integer_invariancefirsths))) -> exists ff_ap_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix ff_an_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix ff_bp_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix ff_bn_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix ff_p_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix ff_n_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix. ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_ap. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_pc_determinant_integer_invariancefirsth)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_ap. mdr_pb_determinant_integer_invariancefirsth = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_pc_determinant_integer_invariancefirsth) + (ff_ap_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_an. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_an + S (ff_an_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_nc_determinant_integer_invariancefirsth)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_an. mdr_nb_determinant_integer_invariancefirsth = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_nc_determinant_integer_invariancefirsth) + (ff_an_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bp. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_ec_determinant_integer_invariancefirsths)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bp. mdr_eb_determinant_integer_invariancefirsths = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_ec_determinant_integer_invariancefirsths) + (ff_bp_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bn. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_fc_determinant_integer_invariancefirsths)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bn. mdr_fb_determinant_integer_invariancefirsths = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * mdr_fc_determinant_integer_invariancefirsths) + (ff_bn_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_positive. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_positive + S (ff_p_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * ff_uc_mce_fold_mdr_determinant_integer_invariancefirsthsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_positive. ff_ub_mce_fold_mdr_determinant_integer_invariancefirsthsf = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * ff_uc_mce_fold_mdr_determinant_integer_invariancefirsthsf) + (ff_p_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_negative. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_prefix_negative + S (ff_n_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * ff_vc_mce_fold_mdr_determinant_integer_invariancefirsthsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_negative. ff_vb_mce_fold_mdr_determinant_integer_invariancefirsthsf = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix)) * ff_vc_mce_fold_mdr_determinant_integer_invariancefirsthsf) + (ff_n_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_determinant_integer_invariancefirsthsf_prefix_term. ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix = 2 * ff_even_mce_term_mdr_determinant_integer_invariancefirsthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) /\ ff_n_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_determinant_integer_invariancefirsthsf_prefix_term. ff_index_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix = 2 * ff_odd_mce_term_mdr_determinant_integer_invariancefirsthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) /\ ff_n_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancefirsthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_determinant_integer_invariancefirsthsf_positive ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive. ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_start. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_start. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_positive = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_terminal. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_terminal + S (mdr_p_determinant_integer_invariancefirsth) = S ((S ((S (mdr_q_determinant_integer_invariancefirsths)))) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_terminal. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_positive = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_terminal * S ((S ((S (mdr_q_determinant_integer_invariancefirsths)))) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive) + (mdr_p_determinant_integer_invariancefirsth))) /\ forall ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive. (exists ff_lt_mce_mdr_determinant_integer_invariancefirsthsf_positive_bound. ff_lt_mce_mdr_determinant_integer_invariancefirsthsf_positive_bound + S ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive = (S (mdr_q_determinant_integer_invariancefirsths))) -> exists ff_a_mce_mdr_determinant_integer_invariancefirsthsf_positive ff_r_mce_mdr_determinant_integer_invariancefirsthsf_positive ff_s_mce_mdr_determinant_integer_invariancefirsthsf_positive. ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_summand. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_summand + S (ff_a_mce_mdr_determinant_integer_invariancefirsthsf_positive) = S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive)) * ff_uc_mce_fold_mdr_determinant_integer_invariancefirsthsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_summand. ff_ub_mce_fold_mdr_determinant_integer_invariancefirsthsf = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_summand * S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive)) * ff_uc_mce_fold_mdr_determinant_integer_invariancefirsthsf) + (ff_a_mce_mdr_determinant_integer_invariancefirsthsf_positive))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_partial. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_partial + S (ff_r_mce_mdr_determinant_integer_invariancefirsthsf_positive) = S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_partial. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_positive = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_partial * S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive) + (ff_r_mce_mdr_determinant_integer_invariancefirsthsf_positive))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_successor. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_positive_successor + S (ff_s_mce_mdr_determinant_integer_invariancefirsthsf_positive) = S ((S (S ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_successor. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_positive = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_positive_successor * S ((S (S ff_i_mce_mdr_determinant_integer_invariancefirsthsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_positive) + (ff_s_mce_mdr_determinant_integer_invariancefirsthsf_positive))) /\ ff_s_mce_mdr_determinant_integer_invariancefirsthsf_positive = ff_r_mce_mdr_determinant_integer_invariancefirsthsf_positive + ff_a_mce_mdr_determinant_integer_invariancefirsthsf_positive)))))) /\ (exists ff_u_mce_mdr_determinant_integer_invariancefirsthsf_negative ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative. ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_start. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_start. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_negative = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_terminal. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_terminal + S (mdr_n_determinant_integer_invariancefirsth) = S ((S ((S (mdr_q_determinant_integer_invariancefirsths)))) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_terminal. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_negative = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_terminal * S ((S ((S (mdr_q_determinant_integer_invariancefirsths)))) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative) + (mdr_n_determinant_integer_invariancefirsth))) /\ forall ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative. (exists ff_lt_mce_mdr_determinant_integer_invariancefirsthsf_negative_bound. ff_lt_mce_mdr_determinant_integer_invariancefirsthsf_negative_bound + S ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative = (S (mdr_q_determinant_integer_invariancefirsths))) -> exists ff_a_mce_mdr_determinant_integer_invariancefirsthsf_negative ff_r_mce_mdr_determinant_integer_invariancefirsthsf_negative ff_s_mce_mdr_determinant_integer_invariancefirsthsf_negative. ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_summand. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_summand + S (ff_a_mce_mdr_determinant_integer_invariancefirsthsf_negative) = S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative)) * ff_vc_mce_fold_mdr_determinant_integer_invariancefirsthsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_summand. ff_vb_mce_fold_mdr_determinant_integer_invariancefirsthsf = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_summand * S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative)) * ff_vc_mce_fold_mdr_determinant_integer_invariancefirsthsf) + (ff_a_mce_mdr_determinant_integer_invariancefirsthsf_negative))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_partial. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_partial + S (ff_r_mce_mdr_determinant_integer_invariancefirsthsf_negative) = S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_partial. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_negative = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_partial * S ((S (ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative) + (ff_r_mce_mdr_determinant_integer_invariancefirsthsf_negative))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_successor. ff_h_mce_mdr_determinant_integer_invariancefirsthsf_negative_successor + S (ff_s_mce_mdr_determinant_integer_invariancefirsthsf_negative) = S ((S (S ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_successor. ff_u_mce_mdr_determinant_integer_invariancefirsthsf_negative = ff_q_mce_mdr_determinant_integer_invariancefirsthsf_negative_successor * S ((S (S ff_i_mce_mdr_determinant_integer_invariancefirsthsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancefirsthsf_negative) + (ff_s_mce_mdr_determinant_integer_invariancefirsthsf_negative))) /\ ff_s_mce_mdr_determinant_integer_invariancefirsthsf_negative = ff_r_mce_mdr_determinant_integer_invariancefirsthsf_negative + ff_a_mce_mdr_determinant_integer_invariancefirsthsf_negative))))))))))))))) /\ ((exists mdr_gap_determinant_integer_invariancefirsti. mdr_gap_determinant_integer_invariancefirsti + S (mdr_i_determinant_integer_invariancefirst) = (mdr_l_determinant_integer_invariancefirst)) /\ (exists mdr_z_determinant_integer_invariancefirstr. ((exists mdr_a_determinant_integer_invariancefirstrc mdr_b_determinant_integer_invariancefirstrc mdr_c_determinant_integer_invariancefirstrc mdr_e_determinant_integer_invariancefirstrc mdr_f_determinant_integer_invariancefirstrc. ((mdr_a_determinant_integer_invariancefirstrc = ((d) + (mdr_ab_determinant_integer_invariance)) * S ((d) + (mdr_ab_determinant_integer_invariance)) + ((mdr_ab_determinant_integer_invariance) + (mdr_ab_determinant_integer_invariance))) /\ ((mdr_b_determinant_integer_invariancefirstrc = ((mdr_ac_determinant_integer_invariance) + (mdr_bb_determinant_integer_invariance)) * S ((mdr_ac_determinant_integer_invariance) + (mdr_bb_determinant_integer_invariance)) + ((mdr_bb_determinant_integer_invariance) + (mdr_bb_determinant_integer_invariance))) /\ ((mdr_c_determinant_integer_invariancefirstrc = ((mdr_a_determinant_integer_invariancefirstrc) + (mdr_b_determinant_integer_invariancefirstrc)) * S ((mdr_a_determinant_integer_invariancefirstrc) + (mdr_b_determinant_integer_invariancefirstrc)) + ((mdr_b_determinant_integer_invariancefirstrc) + (mdr_b_determinant_integer_invariancefirstrc))) /\ ((mdr_e_determinant_integer_invariancefirstrc = ((mdr_p_determinant_integer_invariance) + (mdr_n_determinant_integer_invariance)) * S ((mdr_p_determinant_integer_invariance) + (mdr_n_determinant_integer_invariance)) + ((mdr_n_determinant_integer_invariance) + (mdr_n_determinant_integer_invariance))) /\ ((mdr_f_determinant_integer_invariancefirstrc = ((mdr_bc_determinant_integer_invariance) + (mdr_e_determinant_integer_invariancefirstrc)) * S ((mdr_bc_determinant_integer_invariance) + (mdr_e_determinant_integer_invariancefirstrc)) + ((mdr_e_determinant_integer_invariancefirstrc) + (mdr_e_determinant_integer_invariancefirstrc))) /\ ((mdr_z_determinant_integer_invariancefirstr) = ((mdr_c_determinant_integer_invariancefirstrc) + (mdr_f_determinant_integer_invariancefirstrc)) * S ((mdr_c_determinant_integer_invariancefirstrc) + (mdr_f_determinant_integer_invariancefirstrc)) + ((mdr_f_determinant_integer_invariancefirstrc) + (mdr_f_determinant_integer_invariancefirstrc))))))))) /\ (((exists ff_h_mdr_determinant_integer_invariancefirstrb. ff_h_mdr_determinant_integer_invariancefirstrb + S (mdr_z_determinant_integer_invariancefirstr) = S ((S (mdr_i_determinant_integer_invariancefirst)) * mdr_c_determinant_integer_invariancefirst)) /\ exists ff_q_mdr_determinant_integer_invariancefirstrb. mdr_b_determinant_integer_invariancefirst = ff_q_mdr_determinant_integer_invariancefirstrb * S ((S (mdr_i_determinant_integer_invariancefirst)) * mdr_c_determinant_integer_invariancefirst) + (mdr_z_determinant_integer_invariancefirstr)))))))) -> (exists mdr_b_determinant_integer_invariancesecond mdr_c_determinant_integer_invariancesecond mdr_l_determinant_integer_invariancesecond mdr_i_determinant_integer_invariancesecond. ((forall mdr_i_determinant_integer_invariancesecondh. (exists mdr_gap_determinant_integer_invariancesecondhi. mdr_gap_determinant_integer_invariancesecondhi + S (mdr_i_determinant_integer_invariancesecondh) = (mdr_l_determinant_integer_invariancesecond)) -> exists mdr_d_determinant_integer_invariancesecondh mdr_pb_determinant_integer_invariancesecondh mdr_pc_determinant_integer_invariancesecondh mdr_nb_determinant_integer_invariancesecondh mdr_nc_determinant_integer_invariancesecondh mdr_p_determinant_integer_invariancesecondh mdr_n_determinant_integer_invariancesecondh. ((exists mdr_z_determinant_integer_invariancesecondhr. ((exists mdr_a_determinant_integer_invariancesecondhrc mdr_b_determinant_integer_invariancesecondhrc mdr_c_determinant_integer_invariancesecondhrc mdr_e_determinant_integer_invariancesecondhrc mdr_f_determinant_integer_invariancesecondhrc. ((mdr_a_determinant_integer_invariancesecondhrc = ((mdr_d_determinant_integer_invariancesecondh) + (mdr_pb_determinant_integer_invariancesecondh)) * S ((mdr_d_determinant_integer_invariancesecondh) + (mdr_pb_determinant_integer_invariancesecondh)) + ((mdr_pb_determinant_integer_invariancesecondh) + (mdr_pb_determinant_integer_invariancesecondh))) /\ ((mdr_b_determinant_integer_invariancesecondhrc = ((mdr_pc_determinant_integer_invariancesecondh) + (mdr_nb_determinant_integer_invariancesecondh)) * S ((mdr_pc_determinant_integer_invariancesecondh) + (mdr_nb_determinant_integer_invariancesecondh)) + ((mdr_nb_determinant_integer_invariancesecondh) + (mdr_nb_determinant_integer_invariancesecondh))) /\ ((mdr_c_determinant_integer_invariancesecondhrc = ((mdr_a_determinant_integer_invariancesecondhrc) + (mdr_b_determinant_integer_invariancesecondhrc)) * S ((mdr_a_determinant_integer_invariancesecondhrc) + (mdr_b_determinant_integer_invariancesecondhrc)) + ((mdr_b_determinant_integer_invariancesecondhrc) + (mdr_b_determinant_integer_invariancesecondhrc))) /\ ((mdr_e_determinant_integer_invariancesecondhrc = ((mdr_p_determinant_integer_invariancesecondh) + (mdr_n_determinant_integer_invariancesecondh)) * S ((mdr_p_determinant_integer_invariancesecondh) + (mdr_n_determinant_integer_invariancesecondh)) + ((mdr_n_determinant_integer_invariancesecondh) + (mdr_n_determinant_integer_invariancesecondh))) /\ ((mdr_f_determinant_integer_invariancesecondhrc = ((mdr_nc_determinant_integer_invariancesecondh) + (mdr_e_determinant_integer_invariancesecondhrc)) * S ((mdr_nc_determinant_integer_invariancesecondh) + (mdr_e_determinant_integer_invariancesecondhrc)) + ((mdr_e_determinant_integer_invariancesecondhrc) + (mdr_e_determinant_integer_invariancesecondhrc))) /\ ((mdr_z_determinant_integer_invariancesecondhr) = ((mdr_c_determinant_integer_invariancesecondhrc) + (mdr_f_determinant_integer_invariancesecondhrc)) * S ((mdr_c_determinant_integer_invariancesecondhrc) + (mdr_f_determinant_integer_invariancesecondhrc)) + ((mdr_f_determinant_integer_invariancesecondhrc) + (mdr_f_determinant_integer_invariancesecondhrc))))))))) /\ (((exists ff_h_mdr_determinant_integer_invariancesecondhrb. ff_h_mdr_determinant_integer_invariancesecondhrb + S (mdr_z_determinant_integer_invariancesecondhr) = S ((S (mdr_i_determinant_integer_invariancesecondh)) * mdr_c_determinant_integer_invariancesecond)) /\ exists ff_q_mdr_determinant_integer_invariancesecondhrb. mdr_b_determinant_integer_invariancesecond = ff_q_mdr_determinant_integer_invariancesecondhrb * S ((S (mdr_i_determinant_integer_invariancesecondh)) * mdr_c_determinant_integer_invariancesecond) + (mdr_z_determinant_integer_invariancesecondhr))))) /\ (((((mdr_d_determinant_integer_invariancesecondh) = 0) /\ (((mdr_p_determinant_integer_invariancesecondh) = 1) /\ ((mdr_n_determinant_integer_invariancesecondh) = 0))) \/ exists mdr_q_determinant_integer_invariancesecondhs mdr_eb_determinant_integer_invariancesecondhs mdr_ec_determinant_integer_invariancesecondhs mdr_fb_determinant_integer_invariancesecondhs mdr_fc_determinant_integer_invariancesecondhs. (((mdr_d_determinant_integer_invariancesecondh) = S (mdr_q_determinant_integer_invariancesecondhs)) /\ ((forall mdr_j_determinant_integer_invariancesecondhsc. (exists mdr_gap_determinant_integer_invariancesecondhscj. mdr_gap_determinant_integer_invariancesecondhscj + S (mdr_j_determinant_integer_invariancesecondhsc) = (S (mdr_q_determinant_integer_invariancesecondhs))) -> exists mdr_i_determinant_integer_invariancesecondhsc mdr_up_determinant_integer_invariancesecondhsc mdr_us_determinant_integer_invariancesecondhsc mdr_un_determinant_integer_invariancesecondhsc mdr_ut_determinant_integer_invariancesecondhsc mdr_p_determinant_integer_invariancesecondhsc mdr_n_determinant_integer_invariancesecondhsc. ((exists mdr_gap_determinant_integer_invariancesecondhsci. mdr_gap_determinant_integer_invariancesecondhsci + S (mdr_i_determinant_integer_invariancesecondhsc) = (mdr_i_determinant_integer_invariancesecondh)) /\ ((exists mdr_z_determinant_integer_invariancesecondhscr. ((exists mdr_a_determinant_integer_invariancesecondhscrc mdr_b_determinant_integer_invariancesecondhscrc mdr_c_determinant_integer_invariancesecondhscrc mdr_e_determinant_integer_invariancesecondhscrc mdr_f_determinant_integer_invariancesecondhscrc. ((mdr_a_determinant_integer_invariancesecondhscrc = ((mdr_q_determinant_integer_invariancesecondhs) + (mdr_up_determinant_integer_invariancesecondhsc)) * S ((mdr_q_determinant_integer_invariancesecondhs) + (mdr_up_determinant_integer_invariancesecondhsc)) + ((mdr_up_determinant_integer_invariancesecondhsc) + (mdr_up_determinant_integer_invariancesecondhsc))) /\ ((mdr_b_determinant_integer_invariancesecondhscrc = ((mdr_us_determinant_integer_invariancesecondhsc) + (mdr_un_determinant_integer_invariancesecondhsc)) * S ((mdr_us_determinant_integer_invariancesecondhsc) + (mdr_un_determinant_integer_invariancesecondhsc)) + ((mdr_un_determinant_integer_invariancesecondhsc) + (mdr_un_determinant_integer_invariancesecondhsc))) /\ ((mdr_c_determinant_integer_invariancesecondhscrc = ((mdr_a_determinant_integer_invariancesecondhscrc) + (mdr_b_determinant_integer_invariancesecondhscrc)) * S ((mdr_a_determinant_integer_invariancesecondhscrc) + (mdr_b_determinant_integer_invariancesecondhscrc)) + ((mdr_b_determinant_integer_invariancesecondhscrc) + (mdr_b_determinant_integer_invariancesecondhscrc))) /\ ((mdr_e_determinant_integer_invariancesecondhscrc = ((mdr_p_determinant_integer_invariancesecondhsc) + (mdr_n_determinant_integer_invariancesecondhsc)) * S ((mdr_p_determinant_integer_invariancesecondhsc) + (mdr_n_determinant_integer_invariancesecondhsc)) + ((mdr_n_determinant_integer_invariancesecondhsc) + (mdr_n_determinant_integer_invariancesecondhsc))) /\ ((mdr_f_determinant_integer_invariancesecondhscrc = ((mdr_ut_determinant_integer_invariancesecondhsc) + (mdr_e_determinant_integer_invariancesecondhscrc)) * S ((mdr_ut_determinant_integer_invariancesecondhsc) + (mdr_e_determinant_integer_invariancesecondhscrc)) + ((mdr_e_determinant_integer_invariancesecondhscrc) + (mdr_e_determinant_integer_invariancesecondhscrc))) /\ ((mdr_z_determinant_integer_invariancesecondhscr) = ((mdr_c_determinant_integer_invariancesecondhscrc) + (mdr_f_determinant_integer_invariancesecondhscrc)) * S ((mdr_c_determinant_integer_invariancesecondhscrc) + (mdr_f_determinant_integer_invariancesecondhscrc)) + ((mdr_f_determinant_integer_invariancesecondhscrc) + (mdr_f_determinant_integer_invariancesecondhscrc))))))))) /\ (((exists ff_h_mdr_determinant_integer_invariancesecondhscrb. ff_h_mdr_determinant_integer_invariancesecondhscrb + S (mdr_z_determinant_integer_invariancesecondhscr) = S ((S (mdr_i_determinant_integer_invariancesecondhsc)) * mdr_c_determinant_integer_invariancesecond)) /\ exists ff_q_mdr_determinant_integer_invariancesecondhscrb. mdr_b_determinant_integer_invariancesecond = ff_q_mdr_determinant_integer_invariancesecondhscrb * S ((S (mdr_i_determinant_integer_invariancesecondhsc)) * mdr_c_determinant_integer_invariancesecond) + (mdr_z_determinant_integer_invariancesecondhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive. (exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_index_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) = ((mdr_q_determinant_integer_invariancesecondhs) * (mdr_q_determinant_integer_invariancesecondhs))) -> exists ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive. (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive = (mdr_q_determinant_integer_invariancesecondhs) * ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive + ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_column_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) = (mdr_q_determinant_integer_invariancesecondhs)) /\ ((exists ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell = ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell = S ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) = (mdr_j_determinant_integer_invariancesecondhsc)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell = ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_positive_cell_column_after + (mdr_j_determinant_integer_invariancesecondhsc) = (ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell = S ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_positive_cell_source. ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell) * (S (mdr_q_determinant_integer_invariancesecondhs)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell))) * mdr_pc_determinant_integer_invariancesecondh)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_positive_cell_source. mdr_pb_determinant_integer_invariancesecondh = ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell) * (S (mdr_q_determinant_integer_invariancesecondhs)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_positive_cell))) * mdr_pc_determinant_integer_invariancesecondh) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_positive_target. ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_positive_target + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive)) * mdr_us_determinant_integer_invariancesecondhsc)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_positive_target. mdr_up_determinant_integer_invariancesecondhsc = ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive)) * mdr_us_determinant_integer_invariancesecondhsc) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative. (exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_index_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) = ((mdr_q_determinant_integer_invariancesecondhs) * (mdr_q_determinant_integer_invariancesecondhs))) -> exists ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative. (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative = (mdr_q_determinant_integer_invariancesecondhs) * ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative + ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_column_bound. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) = (mdr_q_determinant_integer_invariancesecondhs)) /\ ((exists ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell = ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative)) /\ ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell = S ff_row_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_determinant_integer_invariancesecondhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) = (mdr_j_determinant_integer_invariancesecondhsc)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell = ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_determinant_integer_invariancesecondhscm_negative_cell_column_after + (mdr_j_determinant_integer_invariancesecondhsc) = (ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative)) /\ ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell = S ff_column_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_negative_cell_source. ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell) * (S (mdr_q_determinant_integer_invariancesecondhs)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell))) * mdr_nc_determinant_integer_invariancesecondh)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_negative_cell_source. mdr_nb_determinant_integer_invariancesecondh = ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell) * (S (mdr_q_determinant_integer_invariancesecondhs)) + (ff_column_mdm_cell_mdr_determinant_integer_invariancesecondhscm_negative_cell))) * mdr_nc_determinant_integer_invariancesecondh) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_negative_target. ff_h_mdm_mdr_determinant_integer_invariancesecondhscm_negative_target + S (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative)) * mdr_ut_determinant_integer_invariancesecondhsc)) /\ exists ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_negative_target. mdr_un_determinant_integer_invariancesecondhsc = ff_q_mdm_mdr_determinant_integer_invariancesecondhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative)) * mdr_ut_determinant_integer_invariancesecondhsc) + (ff_value_mdm_prefix_mdr_determinant_integer_invariancesecondhscm_negative))))))))) /\ ((((exists ff_h_mdr_determinant_integer_invariancesecondhscp. ff_h_mdr_determinant_integer_invariancesecondhscp + S (mdr_p_determinant_integer_invariancesecondhsc) = S ((S (mdr_j_determinant_integer_invariancesecondhsc)) * mdr_ec_determinant_integer_invariancesecondhs)) /\ exists ff_q_mdr_determinant_integer_invariancesecondhscp. mdr_eb_determinant_integer_invariancesecondhs = ff_q_mdr_determinant_integer_invariancesecondhscp * S ((S (mdr_j_determinant_integer_invariancesecondhsc)) * mdr_ec_determinant_integer_invariancesecondhs) + (mdr_p_determinant_integer_invariancesecondhsc))) /\ (((exists ff_h_mdr_determinant_integer_invariancesecondhscn. ff_h_mdr_determinant_integer_invariancesecondhscn + S (mdr_n_determinant_integer_invariancesecondhsc) = S ((S (mdr_j_determinant_integer_invariancesecondhsc)) * mdr_fc_determinant_integer_invariancesecondhs)) /\ exists ff_q_mdr_determinant_integer_invariancesecondhscn. mdr_fb_determinant_integer_invariancesecondhs = ff_q_mdr_determinant_integer_invariancesecondhscn * S ((S (mdr_j_determinant_integer_invariancesecondhsc)) * mdr_fc_determinant_integer_invariancesecondhs) + (mdr_n_determinant_integer_invariancesecondhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_determinant_integer_invariancesecondhsf ff_uc_mce_fold_mdr_determinant_integer_invariancesecondhsf ff_vb_mce_fold_mdr_determinant_integer_invariancesecondhsf ff_vc_mce_fold_mdr_determinant_integer_invariancesecondhsf. ((forall ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix. (exists ff_gap_mce_mdr_determinant_integer_invariancesecondhsf_prefix_index. ff_gap_mce_mdr_determinant_integer_invariancesecondhsf_prefix_index + S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) = (S (mdr_q_determinant_integer_invariancesecondhs))) -> exists ff_ap_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix ff_an_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix ff_bp_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix ff_bn_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix ff_p_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix ff_n_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix. ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_ap. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_pc_determinant_integer_invariancesecondh)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_ap. mdr_pb_determinant_integer_invariancesecondh = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_pc_determinant_integer_invariancesecondh) + (ff_ap_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_an. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_an + S (ff_an_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_nc_determinant_integer_invariancesecondh)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_an. mdr_nb_determinant_integer_invariancesecondh = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_nc_determinant_integer_invariancesecondh) + (ff_an_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bp. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_ec_determinant_integer_invariancesecondhs)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bp. mdr_eb_determinant_integer_invariancesecondhs = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_ec_determinant_integer_invariancesecondhs) + (ff_bp_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bn. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_fc_determinant_integer_invariancesecondhs)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bn. mdr_fb_determinant_integer_invariancesecondhs = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * mdr_fc_determinant_integer_invariancesecondhs) + (ff_bn_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_positive. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_positive + S (ff_p_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * ff_uc_mce_fold_mdr_determinant_integer_invariancesecondhsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_positive. ff_ub_mce_fold_mdr_determinant_integer_invariancesecondhsf = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * ff_uc_mce_fold_mdr_determinant_integer_invariancesecondhsf) + (ff_p_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_negative. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_prefix_negative + S (ff_n_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * ff_vc_mce_fold_mdr_determinant_integer_invariancesecondhsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_negative. ff_vb_mce_fold_mdr_determinant_integer_invariancesecondhsf = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix)) * ff_vc_mce_fold_mdr_determinant_integer_invariancesecondhsf) + (ff_n_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_determinant_integer_invariancesecondhsf_prefix_term. ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix = 2 * ff_even_mce_term_mdr_determinant_integer_invariancesecondhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) /\ ff_n_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_determinant_integer_invariancesecondhsf_prefix_term. ff_index_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix = 2 * ff_odd_mce_term_mdr_determinant_integer_invariancesecondhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) /\ ff_n_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix = (ff_ap_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bp_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) + (ff_an_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix) * (ff_bn_mce_alternating_mdr_determinant_integer_invariancesecondhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_determinant_integer_invariancesecondhsf_positive ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive. ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_start. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_start. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_positive = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_terminal. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_terminal + S (mdr_p_determinant_integer_invariancesecondh) = S ((S ((S (mdr_q_determinant_integer_invariancesecondhs)))) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_terminal. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_positive = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_terminal * S ((S ((S (mdr_q_determinant_integer_invariancesecondhs)))) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive) + (mdr_p_determinant_integer_invariancesecondh))) /\ forall ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive. (exists ff_lt_mce_mdr_determinant_integer_invariancesecondhsf_positive_bound. ff_lt_mce_mdr_determinant_integer_invariancesecondhsf_positive_bound + S ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive = (S (mdr_q_determinant_integer_invariancesecondhs))) -> exists ff_a_mce_mdr_determinant_integer_invariancesecondhsf_positive ff_r_mce_mdr_determinant_integer_invariancesecondhsf_positive ff_s_mce_mdr_determinant_integer_invariancesecondhsf_positive. ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_summand. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_summand + S (ff_a_mce_mdr_determinant_integer_invariancesecondhsf_positive) = S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive)) * ff_uc_mce_fold_mdr_determinant_integer_invariancesecondhsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_summand. ff_ub_mce_fold_mdr_determinant_integer_invariancesecondhsf = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_summand * S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive)) * ff_uc_mce_fold_mdr_determinant_integer_invariancesecondhsf) + (ff_a_mce_mdr_determinant_integer_invariancesecondhsf_positive))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_partial. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_partial + S (ff_r_mce_mdr_determinant_integer_invariancesecondhsf_positive) = S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_partial. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_positive = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_partial * S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive) + (ff_r_mce_mdr_determinant_integer_invariancesecondhsf_positive))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_successor. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_positive_successor + S (ff_s_mce_mdr_determinant_integer_invariancesecondhsf_positive) = S ((S (S ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_successor. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_positive = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_positive_successor * S ((S (S ff_i_mce_mdr_determinant_integer_invariancesecondhsf_positive)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_positive) + (ff_s_mce_mdr_determinant_integer_invariancesecondhsf_positive))) /\ ff_s_mce_mdr_determinant_integer_invariancesecondhsf_positive = ff_r_mce_mdr_determinant_integer_invariancesecondhsf_positive + ff_a_mce_mdr_determinant_integer_invariancesecondhsf_positive)))))) /\ (exists ff_u_mce_mdr_determinant_integer_invariancesecondhsf_negative ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative. ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_start. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_start. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_negative = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_terminal. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_terminal + S (mdr_n_determinant_integer_invariancesecondh) = S ((S ((S (mdr_q_determinant_integer_invariancesecondhs)))) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_terminal. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_negative = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_terminal * S ((S ((S (mdr_q_determinant_integer_invariancesecondhs)))) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative) + (mdr_n_determinant_integer_invariancesecondh))) /\ forall ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative. (exists ff_lt_mce_mdr_determinant_integer_invariancesecondhsf_negative_bound. ff_lt_mce_mdr_determinant_integer_invariancesecondhsf_negative_bound + S ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative = (S (mdr_q_determinant_integer_invariancesecondhs))) -> exists ff_a_mce_mdr_determinant_integer_invariancesecondhsf_negative ff_r_mce_mdr_determinant_integer_invariancesecondhsf_negative ff_s_mce_mdr_determinant_integer_invariancesecondhsf_negative. ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_summand. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_summand + S (ff_a_mce_mdr_determinant_integer_invariancesecondhsf_negative) = S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative)) * ff_vc_mce_fold_mdr_determinant_integer_invariancesecondhsf)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_summand. ff_vb_mce_fold_mdr_determinant_integer_invariancesecondhsf = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_summand * S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative)) * ff_vc_mce_fold_mdr_determinant_integer_invariancesecondhsf) + (ff_a_mce_mdr_determinant_integer_invariancesecondhsf_negative))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_partial. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_partial + S (ff_r_mce_mdr_determinant_integer_invariancesecondhsf_negative) = S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_partial. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_negative = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_partial * S ((S (ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative) + (ff_r_mce_mdr_determinant_integer_invariancesecondhsf_negative))) /\ ((((exists ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_successor. ff_h_mce_mdr_determinant_integer_invariancesecondhsf_negative_successor + S (ff_s_mce_mdr_determinant_integer_invariancesecondhsf_negative) = S ((S (S ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative)) /\ exists ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_successor. ff_u_mce_mdr_determinant_integer_invariancesecondhsf_negative = ff_q_mce_mdr_determinant_integer_invariancesecondhsf_negative_successor * S ((S (S ff_i_mce_mdr_determinant_integer_invariancesecondhsf_negative)) * ff_v_mce_mdr_determinant_integer_invariancesecondhsf_negative) + (ff_s_mce_mdr_determinant_integer_invariancesecondhsf_negative))) /\ ff_s_mce_mdr_determinant_integer_invariancesecondhsf_negative = ff_r_mce_mdr_determinant_integer_invariancesecondhsf_negative + ff_a_mce_mdr_determinant_integer_invariancesecondhsf_negative))))))))))))))) /\ ((exists mdr_gap_determinant_integer_invariancesecondi. mdr_gap_determinant_integer_invariancesecondi + S (mdr_i_determinant_integer_invariancesecond) = (mdr_l_determinant_integer_invariancesecond)) /\ (exists mdr_z_determinant_integer_invariancesecondr. ((exists mdr_a_determinant_integer_invariancesecondrc mdr_b_determinant_integer_invariancesecondrc mdr_c_determinant_integer_invariancesecondrc mdr_e_determinant_integer_invariancesecondrc mdr_f_determinant_integer_invariancesecondrc. ((mdr_a_determinant_integer_invariancesecondrc = ((d) + (mdr_eb_determinant_integer_invariance)) * S ((d) + (mdr_eb_determinant_integer_invariance)) + ((mdr_eb_determinant_integer_invariance) + (mdr_eb_determinant_integer_invariance))) /\ ((mdr_b_determinant_integer_invariancesecondrc = ((mdr_ec_determinant_integer_invariance) + (mdr_fb_determinant_integer_invariance)) * S ((mdr_ec_determinant_integer_invariance) + (mdr_fb_determinant_integer_invariance)) + ((mdr_fb_determinant_integer_invariance) + (mdr_fb_determinant_integer_invariance))) /\ ((mdr_c_determinant_integer_invariancesecondrc = ((mdr_a_determinant_integer_invariancesecondrc) + (mdr_b_determinant_integer_invariancesecondrc)) * S ((mdr_a_determinant_integer_invariancesecondrc) + (mdr_b_determinant_integer_invariancesecondrc)) + ((mdr_b_determinant_integer_invariancesecondrc) + (mdr_b_determinant_integer_invariancesecondrc))) /\ ((mdr_e_determinant_integer_invariancesecondrc = ((mdr_P_determinant_integer_invariance) + (mdr_N_determinant_integer_invariance)) * S ((mdr_P_determinant_integer_invariance) + (mdr_N_determinant_integer_invariance)) + ((mdr_N_determinant_integer_invariance) + (mdr_N_determinant_integer_invariance))) /\ ((mdr_f_determinant_integer_invariancesecondrc = ((mdr_fc_determinant_integer_invariance) + (mdr_e_determinant_integer_invariancesecondrc)) * S ((mdr_fc_determinant_integer_invariance) + (mdr_e_determinant_integer_invariancesecondrc)) + ((mdr_e_determinant_integer_invariancesecondrc) + (mdr_e_determinant_integer_invariancesecondrc))) /\ ((mdr_z_determinant_integer_invariancesecondr) = ((mdr_c_determinant_integer_invariancesecondrc) + (mdr_f_determinant_integer_invariancesecondrc)) * S ((mdr_c_determinant_integer_invariancesecondrc) + (mdr_f_determinant_integer_invariancesecondrc)) + ((mdr_f_determinant_integer_invariancesecondrc) + (mdr_f_determinant_integer_invariancesecondrc))))))))) /\ (((exists ff_h_mdr_determinant_integer_invariancesecondrb. ff_h_mdr_determinant_integer_invariancesecondrb + S (mdr_z_determinant_integer_invariancesecondr) = S ((S (mdr_i_determinant_integer_invariancesecond)) * mdr_c_determinant_integer_invariancesecond)) /\ exists ff_q_mdr_determinant_integer_invariancesecondrb. mdr_b_determinant_integer_invariancesecond = ff_q_mdr_determinant_integer_invariancesecondrb * S ((S (mdr_i_determinant_integer_invariancesecond)) * mdr_c_determinant_integer_invariancesecond) + (mdr_z_determinant_integer_invariancesecondr)))))))) -> mdr_p_determinant_integer_invariance + mdr_N_determinant_integer_invariance = mdr_P_determinant_integer_invariance + mdr_n_determinant_integer_invariance)

Complete tactic proof in conservative notation

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

145 script commands · 19 reading checkpoints · 5 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 (5)

signed recursive determinant zero value signed recursive determinant successor decomposition matrix integer cofactor streams from recursion matrix integer cofactor fold balance matrix integer first row equality

01Induction on dL1–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

L1
induction d
L2
intro ab
L3
intro ac
L4
intro bb
L5
intro bc
L6
intro eb
L7
intro ec
L8
intro fb
L9
intro fc
L10
intro p

02Fix variables and assumptionsL11–16

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

L11
intro n
L12
intro P
L13
intro N
L14
intro hequal
L15
intro hfirst
L16
intro hsecond

03Establish hfirstvalueL17–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed recursive determinant zero value.

L17
have hfirstvalue : p = 1 /\ n = 0
L18
specialize signed_recursive_determinant_zero_value (ab)
L19
specialize signed_recursive_determinant_zero_value (ac)
L20
specialize signed_recursive_determinant_zero_value (bb)
L21
specialize signed_recursive_determinant_zero_value (bc)
L22
specialize signed_recursive_determinant_zero_value (p)
L23
specialize signed_recursive_determinant_zero_value (n)
L24
apply signed_recursive_determinant_zero_value
L25
exact hfirst

04Separate the logical casesL26–26

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

L26
cases hfirstvalue

05Establish hsecondvalueL27–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed recursive determinant zero value.

L27
have hsecondvalue : P = 1 /\ N = 0
L28
specialize signed_recursive_determinant_zero_value (eb)
L29
specialize signed_recursive_determinant_zero_value (ec)
L30
specialize signed_recursive_determinant_zero_value (fb)
L31
specialize signed_recursive_determinant_zero_value (fc)
L32
specialize signed_recursive_determinant_zero_value (P)
L33
specialize signed_recursive_determinant_zero_value (N)
L34
apply signed_recursive_determinant_zero_value
L35
exact hsecond

06Separate the logical casesL36–36

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

L36
cases hsecondvalue

07Calculate and transport equalitiesL37–41

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

L37
rewrite hfirstvalue_left
L38
rewrite hfirstvalue_right
L39
rewrite hsecondvalue_left
L40
rewrite hsecondvalue_right
L41
refl

08Fix variables and assumptionsL42–51

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

L42
intro ab
L43
intro ac
L44
intro bb
L45
intro bc
L46
intro eb
L47
intro ec
L48
intro fb
L49
intro fc
L50
intro p
L51
intro n

09Fix variables and assumptionsL52–56

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

L52
intro P
L53
intro N
L54
intro hequal
L55
intro hfirst
L56
intro hsecond

10Establish hfirstcofL57–66

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed recursive determinant successor decomposition.

L57
have hfirstcof : ∃ u. ∃ v. ∃ U. ∃ V. SignedEvaluatedCofactors(ab,ac,bb,bc,d,u,v,U,V) ∧ SignedAlternatingCofactorFold(ab,ac,bb,bc,u,v,U,V,S d,p,n)Definitions: SignedEvaluatedCofactors(ab,ac,bb,bc,d,u,v,U,V)SignedAlternatingCofactorFold(ab,ac,bb,bc,u,v,U,V,S d,p,n)Original native command in the exact edition
L58
specialize signed_recursive_determinant_successor_decomposition (ab)
L59
specialize signed_recursive_determinant_successor_decomposition (ac)
L60
specialize signed_recursive_determinant_successor_decomposition (bb)
L61
specialize signed_recursive_determinant_successor_decomposition (bc)
L62
specialize signed_recursive_determinant_successor_decomposition (d)
L63
specialize signed_recursive_determinant_successor_decomposition (p)
L64
specialize signed_recursive_determinant_successor_decomposition (n)
L65
apply signed_recursive_determinant_successor_decomposition
L66
exact hfirst

11Separate the logical casesL67–71

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

L67
cases hfirstcof
L68
cases hfirstcof_witness
L69
cases hfirstcof_witness_witness
L70
cases hfirstcof_witness_witness_witness
L71
cases hfirstcof_witness_witness_witness_witness

12Establish hsecondcofL72–81

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed recursive determinant successor decomposition.

L72
have hsecondcof : ∃ u. ∃ v. ∃ U. ∃ V. SignedEvaluatedCofactors(eb,ec,fb,fc,d,u,v,U,V) ∧ SignedAlternatingCofactorFold(eb,ec,fb,fc,u,v,U,V,S d,P,N)Definitions: SignedEvaluatedCofactors(eb,ec,fb,fc,d,u,v,U,V)SignedAlternatingCofactorFold(eb,ec,fb,fc,u,v,U,V,S d,P,N)Original native command in the exact edition
L73
specialize signed_recursive_determinant_successor_decomposition (eb)
L74
specialize signed_recursive_determinant_successor_decomposition (ec)
L75
specialize signed_recursive_determinant_successor_decomposition (fb)
L76
specialize signed_recursive_determinant_successor_decomposition (fc)
L77
specialize signed_recursive_determinant_successor_decomposition (d)
L78
specialize signed_recursive_determinant_successor_decomposition (P)
L79
specialize signed_recursive_determinant_successor_decomposition (N)
L80
apply signed_recursive_determinant_successor_decomposition
L81
exact hsecond

13Separate the logical casesL82–86

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

L82
cases hsecondcof
L83
cases hsecondcof_witness
L84
cases hsecondcof_witness_witness
L85
cases hsecondcof_witness_witness_witness
L86
cases hsecondcof_witness_witness_witness_witness

14Establish hcofactorsL87–96

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

L87
have hcofactors : IntegerVectorEqual(x,x1,x2,x3,x4,x5,x6,x7,S d)Definitions: IntegerVectorEqual(x,x1,x2,x3,x4,x5,x6,x7,S d)Original native command in the exact edition
L88
specialize matrix_integer_cofactor_streams_from_recursion (ab)
L89
specialize matrix_integer_cofactor_streams_from_recursion (ac)
L90
specialize matrix_integer_cofactor_streams_from_recursion (bb)
L91
specialize matrix_integer_cofactor_streams_from_recursion (bc)
L92
specialize matrix_integer_cofactor_streams_from_recursion (eb)
L93
specialize matrix_integer_cofactor_streams_from_recursion (ec)
L94
specialize matrix_integer_cofactor_streams_from_recursion (fb)
L95
specialize matrix_integer_cofactor_streams_from_recursion (fc)
L96
specialize matrix_integer_cofactor_streams_from_recursion (x)

15Use earlier factsL97–106