signed_recursive_determinant_integer_invariant

Exact expanded first-order arithmetic 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)