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
∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ w. ∀ rb. ∀ rc. ∀ cb. ∀ cc. ∀ q. ∀ Rb. ∀ Rc. ∀ Cb. ∀ Cc. ∀ p. ∀ n. (∀ x. ∀ y. Lt(x,q) → BetaAt(rb,rc,x,y) → BetaAt(Rb,Rc,x,y)) → (∀ x. ∀ y. Lt(x,q) → BetaAt(cb,cc,x,y) → BetaAt(Cb,Cc,x,y)) → SignedSelectedDeterminant(pb,pc,nb,nc,w,rb,rc,cb,cc,q,p,n) → SignedSelectedDeterminant(pb,pc,nb,nc,w,Rb,Rc,Cb,Cc,q,p,n)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall pb pc nb nc w rb rc cb cc q Rb Rc Cb Cc p n. (forall mdr_i_det_rows mdr_a_det_rows. (exists mdr_gap_det_rowsb. mdr_gap_det_rowsb + S (mdr_i_det_rows) = (q)) -> (((exists ff_h_mdr_det_rowso. ff_h_mdr_det_rowso + S (mdr_a_det_rows) = S ((S (mdr_i_det_rows)) * rc)) /\ exists ff_q_mdr_det_rowso. rb = ff_q_mdr_det_rowso * S ((S (mdr_i_det_rows)) * rc) + (mdr_a_det_rows))) -> (((exists ff_h_mdr_det_rowsn. ff_h_mdr_det_rowsn + S (mdr_a_det_rows) = S ((S (mdr_i_det_rows)) * Rc)) /\ exists ff_q_mdr_det_rowsn. Rb = ff_q_mdr_det_rowsn * S ((S (mdr_i_det_rows)) * Rc) + (mdr_a_det_rows)))) -> (forall mdr_i_det_columns mdr_a_det_columns. (exists mdr_gap_det_columnsb. mdr_gap_det_columnsb + S (mdr_i_det_columns) = (q)) -> (((exists ff_h_mdr_det_columnso. ff_h_mdr_det_columnso + S (mdr_a_det_columns) = S ((S (mdr_i_det_columns)) * cc)) /\ exists ff_q_mdr_det_columnso. cb = ff_q_mdr_det_columnso * S ((S (mdr_i_det_columns)) * cc) + (mdr_a_det_columns))) -> (((exists ff_h_mdr_det_columnsn. ff_h_mdr_det_columnsn + S (mdr_a_det_columns) = S ((S (mdr_i_det_columns)) * Cc)) /\ exists ff_q_mdr_det_columnsn. Cb = ff_q_mdr_det_columnsn * S ((S (mdr_i_det_columns)) * Cc) + (mdr_a_det_columns)))) -> (exists mdr_ub_selected_det_source mdr_uc_selected_det_source mdr_vb_selected_det_source mdr_vc_selected_det_source. ((((forall mdr_i_selected_det_sourcematrixpositive. (exists mdr_gap_selected_det_sourcematrixpositivebound. mdr_gap_selected_det_sourcematrixpositivebound + S (mdr_i_selected_det_sourcematrixpositive) = ((q) * (q))) -> exists mdr_a_selected_det_sourcematrixpositive. (((exists mdr_r_selected_det_sourcematrixpositivepoint mdr_s_selected_det_sourcematrixpositivepoint mdr_u_selected_det_sourcematrixpositivepoint mdr_v_selected_det_sourcematrixpositivepoint. ((mdr_i_selected_det_sourcematrixpositive = (q) * mdr_r_selected_det_sourcematrixpositivepoint + mdr_s_selected_det_sourcematrixpositivepoint) /\ ((exists mdr_gap_selected_det_sourcematrixpositivepointcolumn. mdr_gap_selected_det_sourcematrixpositivepointcolumn + S (mdr_s_selected_det_sourcematrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_sourcematrixpositivepointrow_index. ff_h_mdr_selected_det_sourcematrixpositivepointrow_index + S (mdr_u_selected_det_sourcematrixpositivepoint) = S ((S (mdr_r_selected_det_sourcematrixpositivepoint)) * rc)) /\ exists ff_q_mdr_selected_det_sourcematrixpositivepointrow_index. rb = ff_q_mdr_selected_det_sourcematrixpositivepointrow_index * S ((S (mdr_r_selected_det_sourcematrixpositivepoint)) * rc) + (mdr_u_selected_det_sourcematrixpositivepoint))) /\ ((((exists ff_h_mdr_selected_det_sourcematrixpositivepointcolumn_index. ff_h_mdr_selected_det_sourcematrixpositivepointcolumn_index + S (mdr_v_selected_det_sourcematrixpositivepoint) = S ((S (mdr_s_selected_det_sourcematrixpositivepoint)) * cc)) /\ exists ff_q_mdr_selected_det_sourcematrixpositivepointcolumn_index. cb = ff_q_mdr_selected_det_sourcematrixpositivepointcolumn_index * S ((S (mdr_s_selected_det_sourcematrixpositivepoint)) * cc) + (mdr_v_selected_det_sourcematrixpositivepoint))) /\ (((exists ff_h_mdr_selected_det_sourcematrixpositivepointsource. ff_h_mdr_selected_det_sourcematrixpositivepointsource + S (mdr_a_selected_det_sourcematrixpositive) = S ((S ((mdr_u_selected_det_sourcematrixpositivepoint) * (w) + (mdr_v_selected_det_sourcematrixpositivepoint))) * pc)) /\ exists ff_q_mdr_selected_det_sourcematrixpositivepointsource. pb = ff_q_mdr_selected_det_sourcematrixpositivepointsource * S ((S ((mdr_u_selected_det_sourcematrixpositivepoint) * (w) + (mdr_v_selected_det_sourcematrixpositivepoint))) * pc) + (mdr_a_selected_det_sourcematrixpositive)))))))) /\ (((exists ff_h_mdr_selected_det_sourcematrixpositiveoutput. ff_h_mdr_selected_det_sourcematrixpositiveoutput + S (mdr_a_selected_det_sourcematrixpositive) = S ((S (mdr_i_selected_det_sourcematrixpositive)) * mdr_uc_selected_det_source)) /\ exists ff_q_mdr_selected_det_sourcematrixpositiveoutput. mdr_ub_selected_det_source = ff_q_mdr_selected_det_sourcematrixpositiveoutput * S ((S (mdr_i_selected_det_sourcematrixpositive)) * mdr_uc_selected_det_source) + (mdr_a_selected_det_sourcematrixpositive)))))) /\ (forall mdr_i_selected_det_sourcematrixnegative. (exists mdr_gap_selected_det_sourcematrixnegativebound. mdr_gap_selected_det_sourcematrixnegativebound + S (mdr_i_selected_det_sourcematrixnegative) = ((q) * (q))) -> exists mdr_a_selected_det_sourcematrixnegative. (((exists mdr_r_selected_det_sourcematrixnegativepoint mdr_s_selected_det_sourcematrixnegativepoint mdr_u_selected_det_sourcematrixnegativepoint mdr_v_selected_det_sourcematrixnegativepoint. ((mdr_i_selected_det_sourcematrixnegative = (q) * mdr_r_selected_det_sourcematrixnegativepoint + mdr_s_selected_det_sourcematrixnegativepoint) /\ ((exists mdr_gap_selected_det_sourcematrixnegativepointcolumn. mdr_gap_selected_det_sourcematrixnegativepointcolumn + S (mdr_s_selected_det_sourcematrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_sourcematrixnegativepointrow_index. ff_h_mdr_selected_det_sourcematrixnegativepointrow_index + S (mdr_u_selected_det_sourcematrixnegativepoint) = S ((S (mdr_r_selected_det_sourcematrixnegativepoint)) * rc)) /\ exists ff_q_mdr_selected_det_sourcematrixnegativepointrow_index. rb = ff_q_mdr_selected_det_sourcematrixnegativepointrow_index * S ((S (mdr_r_selected_det_sourcematrixnegativepoint)) * rc) + (mdr_u_selected_det_sourcematrixnegativepoint))) /\ ((((exists ff_h_mdr_selected_det_sourcematrixnegativepointcolumn_index. ff_h_mdr_selected_det_sourcematrixnegativepointcolumn_index + S (mdr_v_selected_det_sourcematrixnegativepoint) = S ((S (mdr_s_selected_det_sourcematrixnegativepoint)) * cc)) /\ exists ff_q_mdr_selected_det_sourcematrixnegativepointcolumn_index. cb = ff_q_mdr_selected_det_sourcematrixnegativepointcolumn_index * S ((S (mdr_s_selected_det_sourcematrixnegativepoint)) * cc) + (mdr_v_selected_det_sourcematrixnegativepoint))) /\ (((exists ff_h_mdr_selected_det_sourcematrixnegativepointsource. ff_h_mdr_selected_det_sourcematrixnegativepointsource + S (mdr_a_selected_det_sourcematrixnegative) = S ((S ((mdr_u_selected_det_sourcematrixnegativepoint) * (w) + (mdr_v_selected_det_sourcematrixnegativepoint))) * nc)) /\ exists ff_q_mdr_selected_det_sourcematrixnegativepointsource. nb = ff_q_mdr_selected_det_sourcematrixnegativepointsource * S ((S ((mdr_u_selected_det_sourcematrixnegativepoint) * (w) + (mdr_v_selected_det_sourcematrixnegativepoint))) * nc) + (mdr_a_selected_det_sourcematrixnegative)))))))) /\ (((exists ff_h_mdr_selected_det_sourcematrixnegativeoutput. ff_h_mdr_selected_det_sourcematrixnegativeoutput + S (mdr_a_selected_det_sourcematrixnegative) = S ((S (mdr_i_selected_det_sourcematrixnegative)) * mdr_vc_selected_det_source)) /\ exists ff_q_mdr_selected_det_sourcematrixnegativeoutput. mdr_vb_selected_det_source = ff_q_mdr_selected_det_sourcematrixnegativeoutput * S ((S (mdr_i_selected_det_sourcematrixnegative)) * mdr_vc_selected_det_source) + (mdr_a_selected_det_sourcematrixnegative)))))))) /\ (exists mdr_b_selected_det_sourcedeterminant mdr_c_selected_det_sourcedeterminant mdr_l_selected_det_sourcedeterminant mdr_i_selected_det_sourcedeterminant. ((forall mdr_i_selected_det_sourcedeterminanth. (exists mdr_gap_selected_det_sourcedeterminanthi. mdr_gap_selected_det_sourcedeterminanthi + S (mdr_i_selected_det_sourcedeterminanth) = (mdr_l_selected_det_sourcedeterminant)) -> exists mdr_d_selected_det_sourcedeterminanth mdr_pb_selected_det_sourcedeterminanth mdr_pc_selected_det_sourcedeterminanth mdr_nb_selected_det_sourcedeterminanth mdr_nc_selected_det_sourcedeterminanth mdr_p_selected_det_sourcedeterminanth mdr_n_selected_det_sourcedeterminanth. ((exists mdr_z_selected_det_sourcedeterminanthr. ((exists mdr_a_selected_det_sourcedeterminanthrc mdr_b_selected_det_sourcedeterminanthrc mdr_c_selected_det_sourcedeterminanthrc mdr_e_selected_det_sourcedeterminanthrc mdr_f_selected_det_sourcedeterminanthrc. ((mdr_a_selected_det_sourcedeterminanthrc = ((mdr_d_selected_det_sourcedeterminanth) + (mdr_pb_selected_det_sourcedeterminanth)) * S ((mdr_d_selected_det_sourcedeterminanth) + (mdr_pb_selected_det_sourcedeterminanth)) + ((mdr_pb_selected_det_sourcedeterminanth) + (mdr_pb_selected_det_sourcedeterminanth))) /\ ((mdr_b_selected_det_sourcedeterminanthrc = ((mdr_pc_selected_det_sourcedeterminanth) + (mdr_nb_selected_det_sourcedeterminanth)) * S ((mdr_pc_selected_det_sourcedeterminanth) + (mdr_nb_selected_det_sourcedeterminanth)) + ((mdr_nb_selected_det_sourcedeterminanth) + (mdr_nb_selected_det_sourcedeterminanth))) /\ ((mdr_c_selected_det_sourcedeterminanthrc = ((mdr_a_selected_det_sourcedeterminanthrc) + (mdr_b_selected_det_sourcedeterminanthrc)) * S ((mdr_a_selected_det_sourcedeterminanthrc) + (mdr_b_selected_det_sourcedeterminanthrc)) + ((mdr_b_selected_det_sourcedeterminanthrc) + (mdr_b_selected_det_sourcedeterminanthrc))) /\ ((mdr_e_selected_det_sourcedeterminanthrc = ((mdr_p_selected_det_sourcedeterminanth) + (mdr_n_selected_det_sourcedeterminanth)) * S ((mdr_p_selected_det_sourcedeterminanth) + (mdr_n_selected_det_sourcedeterminanth)) + ((mdr_n_selected_det_sourcedeterminanth) + (mdr_n_selected_det_sourcedeterminanth))) /\ ((mdr_f_selected_det_sourcedeterminanthrc = ((mdr_nc_selected_det_sourcedeterminanth) + (mdr_e_selected_det_sourcedeterminanthrc)) * S ((mdr_nc_selected_det_sourcedeterminanth) + (mdr_e_selected_det_sourcedeterminanthrc)) + ((mdr_e_selected_det_sourcedeterminanthrc) + (mdr_e_selected_det_sourcedeterminanthrc))) /\ ((mdr_z_selected_det_sourcedeterminanthr) = ((mdr_c_selected_det_sourcedeterminanthrc) + (mdr_f_selected_det_sourcedeterminanthrc)) * S ((mdr_c_selected_det_sourcedeterminanthrc) + (mdr_f_selected_det_sourcedeterminanthrc)) + ((mdr_f_selected_det_sourcedeterminanthrc) + (mdr_f_selected_det_sourcedeterminanthrc))))))))) /\ (((exists ff_h_mdr_selected_det_sourcedeterminanthrb. ff_h_mdr_selected_det_sourcedeterminanthrb + S (mdr_z_selected_det_sourcedeterminanthr) = S ((S (mdr_i_selected_det_sourcedeterminanth)) * mdr_c_selected_det_sourcedeterminant)) /\ exists ff_q_mdr_selected_det_sourcedeterminanthrb. mdr_b_selected_det_sourcedeterminant = ff_q_mdr_selected_det_sourcedeterminanthrb * S ((S (mdr_i_selected_det_sourcedeterminanth)) * mdr_c_selected_det_sourcedeterminant) + (mdr_z_selected_det_sourcedeterminanthr))))) /\ (((((mdr_d_selected_det_sourcedeterminanth) = 0) /\ (((mdr_p_selected_det_sourcedeterminanth) = 1) /\ ((mdr_n_selected_det_sourcedeterminanth) = 0))) \/ exists mdr_q_selected_det_sourcedeterminanths mdr_eb_selected_det_sourcedeterminanths mdr_ec_selected_det_sourcedeterminanths mdr_fb_selected_det_sourcedeterminanths mdr_fc_selected_det_sourcedeterminanths. (((mdr_d_selected_det_sourcedeterminanth) = S (mdr_q_selected_det_sourcedeterminanths)) /\ ((forall mdr_j_selected_det_sourcedeterminanthsc. (exists mdr_gap_selected_det_sourcedeterminanthscj. mdr_gap_selected_det_sourcedeterminanthscj + S (mdr_j_selected_det_sourcedeterminanthsc) = (S (mdr_q_selected_det_sourcedeterminanths))) -> exists mdr_i_selected_det_sourcedeterminanthsc mdr_up_selected_det_sourcedeterminanthsc mdr_us_selected_det_sourcedeterminanthsc mdr_un_selected_det_sourcedeterminanthsc mdr_ut_selected_det_sourcedeterminanthsc mdr_p_selected_det_sourcedeterminanthsc mdr_n_selected_det_sourcedeterminanthsc. ((exists mdr_gap_selected_det_sourcedeterminanthsci. mdr_gap_selected_det_sourcedeterminanthsci + S (mdr_i_selected_det_sourcedeterminanthsc) = (mdr_i_selected_det_sourcedeterminanth)) /\ ((exists mdr_z_selected_det_sourcedeterminanthscr. ((exists mdr_a_selected_det_sourcedeterminanthscrc mdr_b_selected_det_sourcedeterminanthscrc mdr_c_selected_det_sourcedeterminanthscrc mdr_e_selected_det_sourcedeterminanthscrc mdr_f_selected_det_sourcedeterminanthscrc. ((mdr_a_selected_det_sourcedeterminanthscrc = ((mdr_q_selected_det_sourcedeterminanths) + (mdr_up_selected_det_sourcedeterminanthsc)) * S ((mdr_q_selected_det_sourcedeterminanths) + (mdr_up_selected_det_sourcedeterminanthsc)) + ((mdr_up_selected_det_sourcedeterminanthsc) + (mdr_up_selected_det_sourcedeterminanthsc))) /\ ((mdr_b_selected_det_sourcedeterminanthscrc = ((mdr_us_selected_det_sourcedeterminanthsc) + (mdr_un_selected_det_sourcedeterminanthsc)) * S ((mdr_us_selected_det_sourcedeterminanthsc) + (mdr_un_selected_det_sourcedeterminanthsc)) + ((mdr_un_selected_det_sourcedeterminanthsc) + (mdr_un_selected_det_sourcedeterminanthsc))) /\ ((mdr_c_selected_det_sourcedeterminanthscrc = ((mdr_a_selected_det_sourcedeterminanthscrc) + (mdr_b_selected_det_sourcedeterminanthscrc)) * S ((mdr_a_selected_det_sourcedeterminanthscrc) + (mdr_b_selected_det_sourcedeterminanthscrc)) + ((mdr_b_selected_det_sourcedeterminanthscrc) + (mdr_b_selected_det_sourcedeterminanthscrc))) /\ ((mdr_e_selected_det_sourcedeterminanthscrc = ((mdr_p_selected_det_sourcedeterminanthsc) + (mdr_n_selected_det_sourcedeterminanthsc)) * S ((mdr_p_selected_det_sourcedeterminanthsc) + (mdr_n_selected_det_sourcedeterminanthsc)) + ((mdr_n_selected_det_sourcedeterminanthsc) + (mdr_n_selected_det_sourcedeterminanthsc))) /\ ((mdr_f_selected_det_sourcedeterminanthscrc = ((mdr_ut_selected_det_sourcedeterminanthsc) + (mdr_e_selected_det_sourcedeterminanthscrc)) * S ((mdr_ut_selected_det_sourcedeterminanthsc) + (mdr_e_selected_det_sourcedeterminanthscrc)) + ((mdr_e_selected_det_sourcedeterminanthscrc) + (mdr_e_selected_det_sourcedeterminanthscrc))) /\ ((mdr_z_selected_det_sourcedeterminanthscr) = ((mdr_c_selected_det_sourcedeterminanthscrc) + (mdr_f_selected_det_sourcedeterminanthscrc)) * S ((mdr_c_selected_det_sourcedeterminanthscrc) + (mdr_f_selected_det_sourcedeterminanthscrc)) + ((mdr_f_selected_det_sourcedeterminanthscrc) + (mdr_f_selected_det_sourcedeterminanthscrc))))))))) /\ (((exists ff_h_mdr_selected_det_sourcedeterminanthscrb. ff_h_mdr_selected_det_sourcedeterminanthscrb + S (mdr_z_selected_det_sourcedeterminanthscr) = S ((S (mdr_i_selected_det_sourcedeterminanthsc)) * mdr_c_selected_det_sourcedeterminant)) /\ exists ff_q_mdr_selected_det_sourcedeterminanthscrb. mdr_b_selected_det_sourcedeterminant = ff_q_mdr_selected_det_sourcedeterminanthscrb * S ((S (mdr_i_selected_det_sourcedeterminanthsc)) * mdr_c_selected_det_sourcedeterminant) + (mdr_z_selected_det_sourcedeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) = ((mdr_q_selected_det_sourcedeterminanths) * (mdr_q_selected_det_sourcedeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive. (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive = (mdr_q_selected_det_sourcedeterminanths) * ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive + ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) = (mdr_q_selected_det_sourcedeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) = (mdr_j_selected_det_sourcedeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_positive_cell_column_after + (mdr_j_selected_det_sourcedeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_positive_cell_source. ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell) * (S (mdr_q_selected_det_sourcedeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell))) * mdr_pc_selected_det_sourcedeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_positive_cell_source. mdr_pb_selected_det_sourcedeterminanth = ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell) * (S (mdr_q_selected_det_sourcedeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_positive_cell))) * mdr_pc_selected_det_sourcedeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_positive_target. ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive)) * mdr_us_selected_det_sourcedeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_positive_target. mdr_up_selected_det_sourcedeterminanthsc = ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive)) * mdr_us_selected_det_sourcedeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) = ((mdr_q_selected_det_sourcedeterminanths) * (mdr_q_selected_det_sourcedeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative. (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative = (mdr_q_selected_det_sourcedeterminanths) * ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative + ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) = (mdr_q_selected_det_sourcedeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_sourcedeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) = (mdr_j_selected_det_sourcedeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_selected_det_sourcedeterminanthscm_negative_cell_column_after + (mdr_j_selected_det_sourcedeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_negative_cell_source. ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell) * (S (mdr_q_selected_det_sourcedeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell))) * mdr_nc_selected_det_sourcedeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_negative_cell_source. mdr_nb_selected_det_sourcedeterminanth = ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell) * (S (mdr_q_selected_det_sourcedeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_sourcedeterminanthscm_negative_cell))) * mdr_nc_selected_det_sourcedeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_negative_target. ff_h_mdm_mdr_selected_det_sourcedeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative)) * mdr_ut_selected_det_sourcedeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_negative_target. mdr_un_selected_det_sourcedeterminanthsc = ff_q_mdm_mdr_selected_det_sourcedeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative)) * mdr_ut_selected_det_sourcedeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_sourcedeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_selected_det_sourcedeterminanthscp. ff_h_mdr_selected_det_sourcedeterminanthscp + S (mdr_p_selected_det_sourcedeterminanthsc) = S ((S (mdr_j_selected_det_sourcedeterminanthsc)) * mdr_ec_selected_det_sourcedeterminanths)) /\ exists ff_q_mdr_selected_det_sourcedeterminanthscp. mdr_eb_selected_det_sourcedeterminanths = ff_q_mdr_selected_det_sourcedeterminanthscp * S ((S (mdr_j_selected_det_sourcedeterminanthsc)) * mdr_ec_selected_det_sourcedeterminanths) + (mdr_p_selected_det_sourcedeterminanthsc))) /\ (((exists ff_h_mdr_selected_det_sourcedeterminanthscn. ff_h_mdr_selected_det_sourcedeterminanthscn + S (mdr_n_selected_det_sourcedeterminanthsc) = S ((S (mdr_j_selected_det_sourcedeterminanthsc)) * mdr_fc_selected_det_sourcedeterminanths)) /\ exists ff_q_mdr_selected_det_sourcedeterminanthscn. mdr_fb_selected_det_sourcedeterminanths = ff_q_mdr_selected_det_sourcedeterminanthscn * S ((S (mdr_j_selected_det_sourcedeterminanthsc)) * mdr_fc_selected_det_sourcedeterminanths) + (mdr_n_selected_det_sourcedeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_selected_det_sourcedeterminanthsf ff_uc_mce_fold_mdr_selected_det_sourcedeterminanthsf ff_vb_mce_fold_mdr_selected_det_sourcedeterminanthsf ff_vc_mce_fold_mdr_selected_det_sourcedeterminanthsf. ((forall ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix. (exists ff_gap_mce_mdr_selected_det_sourcedeterminanthsf_prefix_index. ff_gap_mce_mdr_selected_det_sourcedeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) = (S (mdr_q_selected_det_sourcedeterminanths))) -> exists ff_ap_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix ff_an_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix ff_bp_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix ff_bn_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix ff_p_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix ff_n_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix. ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_ap. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_pc_selected_det_sourcedeterminanth)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_ap. mdr_pb_selected_det_sourcedeterminanth = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_pc_selected_det_sourcedeterminanth) + (ff_ap_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_an. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_nc_selected_det_sourcedeterminanth)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_an. mdr_nb_selected_det_sourcedeterminanth = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_nc_selected_det_sourcedeterminanth) + (ff_an_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bp. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_ec_selected_det_sourcedeterminanths)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bp. mdr_eb_selected_det_sourcedeterminanths = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_ec_selected_det_sourcedeterminanths) + (ff_bp_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bn. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_fc_selected_det_sourcedeterminanths)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bn. mdr_fb_selected_det_sourcedeterminanths = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * mdr_fc_selected_det_sourcedeterminanths) + (ff_bn_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_positive. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_sourcedeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_selected_det_sourcedeterminanthsf = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_sourcedeterminanthsf) + (ff_p_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_negative. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_sourcedeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_selected_det_sourcedeterminanthsf = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_sourcedeterminanthsf) + (ff_n_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_selected_det_sourcedeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_selected_det_sourcedeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_selected_det_sourcedeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_selected_det_sourcedeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_sourcedeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_selected_det_sourcedeterminanthsf_positive ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_start. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_start. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_positive = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_terminal. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_terminal + S (mdr_p_selected_det_sourcedeterminanth) = S ((S ((S (mdr_q_selected_det_sourcedeterminanths)))) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_terminal. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_positive = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_terminal * S ((S ((S (mdr_q_selected_det_sourcedeterminanths)))) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive) + (mdr_p_selected_det_sourcedeterminanth))) /\ forall ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive. (exists ff_lt_mce_mdr_selected_det_sourcedeterminanthsf_positive_bound. ff_lt_mce_mdr_selected_det_sourcedeterminanthsf_positive_bound + S ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive = (S (mdr_q_selected_det_sourcedeterminanths))) -> exists ff_a_mce_mdr_selected_det_sourcedeterminanthsf_positive ff_r_mce_mdr_selected_det_sourcedeterminanthsf_positive ff_s_mce_mdr_selected_det_sourcedeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_summand. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_summand + S (ff_a_mce_mdr_selected_det_sourcedeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_sourcedeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_selected_det_sourcedeterminanthsf = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_sourcedeterminanthsf) + (ff_a_mce_mdr_selected_det_sourcedeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_partial. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_partial + S (ff_r_mce_mdr_selected_det_sourcedeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_partial. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_positive = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive) + (ff_r_mce_mdr_selected_det_sourcedeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_successor. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_positive_successor + S (ff_s_mce_mdr_selected_det_sourcedeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_successor. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_positive = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_selected_det_sourcedeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_positive) + (ff_s_mce_mdr_selected_det_sourcedeterminanthsf_positive))) /\ ff_s_mce_mdr_selected_det_sourcedeterminanthsf_positive = ff_r_mce_mdr_selected_det_sourcedeterminanthsf_positive + ff_a_mce_mdr_selected_det_sourcedeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_selected_det_sourcedeterminanthsf_negative ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_start. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_start. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_negative = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_terminal. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_terminal + S (mdr_n_selected_det_sourcedeterminanth) = S ((S ((S (mdr_q_selected_det_sourcedeterminanths)))) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_terminal. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_negative = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_terminal * S ((S ((S (mdr_q_selected_det_sourcedeterminanths)))) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative) + (mdr_n_selected_det_sourcedeterminanth))) /\ forall ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative. (exists ff_lt_mce_mdr_selected_det_sourcedeterminanthsf_negative_bound. ff_lt_mce_mdr_selected_det_sourcedeterminanthsf_negative_bound + S ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative = (S (mdr_q_selected_det_sourcedeterminanths))) -> exists ff_a_mce_mdr_selected_det_sourcedeterminanthsf_negative ff_r_mce_mdr_selected_det_sourcedeterminanthsf_negative ff_s_mce_mdr_selected_det_sourcedeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_summand. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_summand + S (ff_a_mce_mdr_selected_det_sourcedeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_sourcedeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_selected_det_sourcedeterminanthsf = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_sourcedeterminanthsf) + (ff_a_mce_mdr_selected_det_sourcedeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_partial. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_partial + S (ff_r_mce_mdr_selected_det_sourcedeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_partial. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_negative = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative) + (ff_r_mce_mdr_selected_det_sourcedeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_successor. ff_h_mce_mdr_selected_det_sourcedeterminanthsf_negative_successor + S (ff_s_mce_mdr_selected_det_sourcedeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_successor. ff_u_mce_mdr_selected_det_sourcedeterminanthsf_negative = ff_q_mce_mdr_selected_det_sourcedeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_selected_det_sourcedeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_sourcedeterminanthsf_negative) + (ff_s_mce_mdr_selected_det_sourcedeterminanthsf_negative))) /\ ff_s_mce_mdr_selected_det_sourcedeterminanthsf_negative = ff_r_mce_mdr_selected_det_sourcedeterminanthsf_negative + ff_a_mce_mdr_selected_det_sourcedeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_selected_det_sourcedeterminanti. mdr_gap_selected_det_sourcedeterminanti + S (mdr_i_selected_det_sourcedeterminant) = (mdr_l_selected_det_sourcedeterminant)) /\ (exists mdr_z_selected_det_sourcedeterminantr. ((exists mdr_a_selected_det_sourcedeterminantrc mdr_b_selected_det_sourcedeterminantrc mdr_c_selected_det_sourcedeterminantrc mdr_e_selected_det_sourcedeterminantrc mdr_f_selected_det_sourcedeterminantrc. ((mdr_a_selected_det_sourcedeterminantrc = ((q) + (mdr_ub_selected_det_source)) * S ((q) + (mdr_ub_selected_det_source)) + ((mdr_ub_selected_det_source) + (mdr_ub_selected_det_source))) /\ ((mdr_b_selected_det_sourcedeterminantrc = ((mdr_uc_selected_det_source) + (mdr_vb_selected_det_source)) * S ((mdr_uc_selected_det_source) + (mdr_vb_selected_det_source)) + ((mdr_vb_selected_det_source) + (mdr_vb_selected_det_source))) /\ ((mdr_c_selected_det_sourcedeterminantrc = ((mdr_a_selected_det_sourcedeterminantrc) + (mdr_b_selected_det_sourcedeterminantrc)) * S ((mdr_a_selected_det_sourcedeterminantrc) + (mdr_b_selected_det_sourcedeterminantrc)) + ((mdr_b_selected_det_sourcedeterminantrc) + (mdr_b_selected_det_sourcedeterminantrc))) /\ ((mdr_e_selected_det_sourcedeterminantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_selected_det_sourcedeterminantrc = ((mdr_vc_selected_det_source) + (mdr_e_selected_det_sourcedeterminantrc)) * S ((mdr_vc_selected_det_source) + (mdr_e_selected_det_sourcedeterminantrc)) + ((mdr_e_selected_det_sourcedeterminantrc) + (mdr_e_selected_det_sourcedeterminantrc))) /\ ((mdr_z_selected_det_sourcedeterminantr) = ((mdr_c_selected_det_sourcedeterminantrc) + (mdr_f_selected_det_sourcedeterminantrc)) * S ((mdr_c_selected_det_sourcedeterminantrc) + (mdr_f_selected_det_sourcedeterminantrc)) + ((mdr_f_selected_det_sourcedeterminantrc) + (mdr_f_selected_det_sourcedeterminantrc))))))))) /\ (((exists ff_h_mdr_selected_det_sourcedeterminantrb. ff_h_mdr_selected_det_sourcedeterminantrb + S (mdr_z_selected_det_sourcedeterminantr) = S ((S (mdr_i_selected_det_sourcedeterminant)) * mdr_c_selected_det_sourcedeterminant)) /\ exists ff_q_mdr_selected_det_sourcedeterminantrb. mdr_b_selected_det_sourcedeterminant = ff_q_mdr_selected_det_sourcedeterminantrb * S ((S (mdr_i_selected_det_sourcedeterminant)) * mdr_c_selected_det_sourcedeterminant) + (mdr_z_selected_det_sourcedeterminantr)))))))))) -> (exists mdr_ub_selected_det_target mdr_uc_selected_det_target mdr_vb_selected_det_target mdr_vc_selected_det_target. ((((forall mdr_i_selected_det_targetmatrixpositive. (exists mdr_gap_selected_det_targetmatrixpositivebound. mdr_gap_selected_det_targetmatrixpositivebound + S (mdr_i_selected_det_targetmatrixpositive) = ((q) * (q))) -> exists mdr_a_selected_det_targetmatrixpositive. (((exists mdr_r_selected_det_targetmatrixpositivepoint mdr_s_selected_det_targetmatrixpositivepoint mdr_u_selected_det_targetmatrixpositivepoint mdr_v_selected_det_targetmatrixpositivepoint. ((mdr_i_selected_det_targetmatrixpositive = (q) * mdr_r_selected_det_targetmatrixpositivepoint + mdr_s_selected_det_targetmatrixpositivepoint) /\ ((exists mdr_gap_selected_det_targetmatrixpositivepointcolumn. mdr_gap_selected_det_targetmatrixpositivepointcolumn + S (mdr_s_selected_det_targetmatrixpositivepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_targetmatrixpositivepointrow_index. ff_h_mdr_selected_det_targetmatrixpositivepointrow_index + S (mdr_u_selected_det_targetmatrixpositivepoint) = S ((S (mdr_r_selected_det_targetmatrixpositivepoint)) * Rc)) /\ exists ff_q_mdr_selected_det_targetmatrixpositivepointrow_index. Rb = ff_q_mdr_selected_det_targetmatrixpositivepointrow_index * S ((S (mdr_r_selected_det_targetmatrixpositivepoint)) * Rc) + (mdr_u_selected_det_targetmatrixpositivepoint))) /\ ((((exists ff_h_mdr_selected_det_targetmatrixpositivepointcolumn_index. ff_h_mdr_selected_det_targetmatrixpositivepointcolumn_index + S (mdr_v_selected_det_targetmatrixpositivepoint) = S ((S (mdr_s_selected_det_targetmatrixpositivepoint)) * Cc)) /\ exists ff_q_mdr_selected_det_targetmatrixpositivepointcolumn_index. Cb = ff_q_mdr_selected_det_targetmatrixpositivepointcolumn_index * S ((S (mdr_s_selected_det_targetmatrixpositivepoint)) * Cc) + (mdr_v_selected_det_targetmatrixpositivepoint))) /\ (((exists ff_h_mdr_selected_det_targetmatrixpositivepointsource. ff_h_mdr_selected_det_targetmatrixpositivepointsource + S (mdr_a_selected_det_targetmatrixpositive) = S ((S ((mdr_u_selected_det_targetmatrixpositivepoint) * (w) + (mdr_v_selected_det_targetmatrixpositivepoint))) * pc)) /\ exists ff_q_mdr_selected_det_targetmatrixpositivepointsource. pb = ff_q_mdr_selected_det_targetmatrixpositivepointsource * S ((S ((mdr_u_selected_det_targetmatrixpositivepoint) * (w) + (mdr_v_selected_det_targetmatrixpositivepoint))) * pc) + (mdr_a_selected_det_targetmatrixpositive)))))))) /\ (((exists ff_h_mdr_selected_det_targetmatrixpositiveoutput. ff_h_mdr_selected_det_targetmatrixpositiveoutput + S (mdr_a_selected_det_targetmatrixpositive) = S ((S (mdr_i_selected_det_targetmatrixpositive)) * mdr_uc_selected_det_target)) /\ exists ff_q_mdr_selected_det_targetmatrixpositiveoutput. mdr_ub_selected_det_target = ff_q_mdr_selected_det_targetmatrixpositiveoutput * S ((S (mdr_i_selected_det_targetmatrixpositive)) * mdr_uc_selected_det_target) + (mdr_a_selected_det_targetmatrixpositive)))))) /\ (forall mdr_i_selected_det_targetmatrixnegative. (exists mdr_gap_selected_det_targetmatrixnegativebound. mdr_gap_selected_det_targetmatrixnegativebound + S (mdr_i_selected_det_targetmatrixnegative) = ((q) * (q))) -> exists mdr_a_selected_det_targetmatrixnegative. (((exists mdr_r_selected_det_targetmatrixnegativepoint mdr_s_selected_det_targetmatrixnegativepoint mdr_u_selected_det_targetmatrixnegativepoint mdr_v_selected_det_targetmatrixnegativepoint. ((mdr_i_selected_det_targetmatrixnegative = (q) * mdr_r_selected_det_targetmatrixnegativepoint + mdr_s_selected_det_targetmatrixnegativepoint) /\ ((exists mdr_gap_selected_det_targetmatrixnegativepointcolumn. mdr_gap_selected_det_targetmatrixnegativepointcolumn + S (mdr_s_selected_det_targetmatrixnegativepoint) = (q)) /\ ((((exists ff_h_mdr_selected_det_targetmatrixnegativepointrow_index. ff_h_mdr_selected_det_targetmatrixnegativepointrow_index + S (mdr_u_selected_det_targetmatrixnegativepoint) = S ((S (mdr_r_selected_det_targetmatrixnegativepoint)) * Rc)) /\ exists ff_q_mdr_selected_det_targetmatrixnegativepointrow_index. Rb = ff_q_mdr_selected_det_targetmatrixnegativepointrow_index * S ((S (mdr_r_selected_det_targetmatrixnegativepoint)) * Rc) + (mdr_u_selected_det_targetmatrixnegativepoint))) /\ ((((exists ff_h_mdr_selected_det_targetmatrixnegativepointcolumn_index. ff_h_mdr_selected_det_targetmatrixnegativepointcolumn_index + S (mdr_v_selected_det_targetmatrixnegativepoint) = S ((S (mdr_s_selected_det_targetmatrixnegativepoint)) * Cc)) /\ exists ff_q_mdr_selected_det_targetmatrixnegativepointcolumn_index. Cb = ff_q_mdr_selected_det_targetmatrixnegativepointcolumn_index * S ((S (mdr_s_selected_det_targetmatrixnegativepoint)) * Cc) + (mdr_v_selected_det_targetmatrixnegativepoint))) /\ (((exists ff_h_mdr_selected_det_targetmatrixnegativepointsource. ff_h_mdr_selected_det_targetmatrixnegativepointsource + S (mdr_a_selected_det_targetmatrixnegative) = S ((S ((mdr_u_selected_det_targetmatrixnegativepoint) * (w) + (mdr_v_selected_det_targetmatrixnegativepoint))) * nc)) /\ exists ff_q_mdr_selected_det_targetmatrixnegativepointsource. nb = ff_q_mdr_selected_det_targetmatrixnegativepointsource * S ((S ((mdr_u_selected_det_targetmatrixnegativepoint) * (w) + (mdr_v_selected_det_targetmatrixnegativepoint))) * nc) + (mdr_a_selected_det_targetmatrixnegative)))))))) /\ (((exists ff_h_mdr_selected_det_targetmatrixnegativeoutput. ff_h_mdr_selected_det_targetmatrixnegativeoutput + S (mdr_a_selected_det_targetmatrixnegative) = S ((S (mdr_i_selected_det_targetmatrixnegative)) * mdr_vc_selected_det_target)) /\ exists ff_q_mdr_selected_det_targetmatrixnegativeoutput. mdr_vb_selected_det_target = ff_q_mdr_selected_det_targetmatrixnegativeoutput * S ((S (mdr_i_selected_det_targetmatrixnegative)) * mdr_vc_selected_det_target) + (mdr_a_selected_det_targetmatrixnegative)))))))) /\ (exists mdr_b_selected_det_targetdeterminant mdr_c_selected_det_targetdeterminant mdr_l_selected_det_targetdeterminant mdr_i_selected_det_targetdeterminant. ((forall mdr_i_selected_det_targetdeterminanth. (exists mdr_gap_selected_det_targetdeterminanthi. mdr_gap_selected_det_targetdeterminanthi + S (mdr_i_selected_det_targetdeterminanth) = (mdr_l_selected_det_targetdeterminant)) -> exists mdr_d_selected_det_targetdeterminanth mdr_pb_selected_det_targetdeterminanth mdr_pc_selected_det_targetdeterminanth mdr_nb_selected_det_targetdeterminanth mdr_nc_selected_det_targetdeterminanth mdr_p_selected_det_targetdeterminanth mdr_n_selected_det_targetdeterminanth. ((exists mdr_z_selected_det_targetdeterminanthr. ((exists mdr_a_selected_det_targetdeterminanthrc mdr_b_selected_det_targetdeterminanthrc mdr_c_selected_det_targetdeterminanthrc mdr_e_selected_det_targetdeterminanthrc mdr_f_selected_det_targetdeterminanthrc. ((mdr_a_selected_det_targetdeterminanthrc = ((mdr_d_selected_det_targetdeterminanth) + (mdr_pb_selected_det_targetdeterminanth)) * S ((mdr_d_selected_det_targetdeterminanth) + (mdr_pb_selected_det_targetdeterminanth)) + ((mdr_pb_selected_det_targetdeterminanth) + (mdr_pb_selected_det_targetdeterminanth))) /\ ((mdr_b_selected_det_targetdeterminanthrc = ((mdr_pc_selected_det_targetdeterminanth) + (mdr_nb_selected_det_targetdeterminanth)) * S ((mdr_pc_selected_det_targetdeterminanth) + (mdr_nb_selected_det_targetdeterminanth)) + ((mdr_nb_selected_det_targetdeterminanth) + (mdr_nb_selected_det_targetdeterminanth))) /\ ((mdr_c_selected_det_targetdeterminanthrc = ((mdr_a_selected_det_targetdeterminanthrc) + (mdr_b_selected_det_targetdeterminanthrc)) * S ((mdr_a_selected_det_targetdeterminanthrc) + (mdr_b_selected_det_targetdeterminanthrc)) + ((mdr_b_selected_det_targetdeterminanthrc) + (mdr_b_selected_det_targetdeterminanthrc))) /\ ((mdr_e_selected_det_targetdeterminanthrc = ((mdr_p_selected_det_targetdeterminanth) + (mdr_n_selected_det_targetdeterminanth)) * S ((mdr_p_selected_det_targetdeterminanth) + (mdr_n_selected_det_targetdeterminanth)) + ((mdr_n_selected_det_targetdeterminanth) + (mdr_n_selected_det_targetdeterminanth))) /\ ((mdr_f_selected_det_targetdeterminanthrc = ((mdr_nc_selected_det_targetdeterminanth) + (mdr_e_selected_det_targetdeterminanthrc)) * S ((mdr_nc_selected_det_targetdeterminanth) + (mdr_e_selected_det_targetdeterminanthrc)) + ((mdr_e_selected_det_targetdeterminanthrc) + (mdr_e_selected_det_targetdeterminanthrc))) /\ ((mdr_z_selected_det_targetdeterminanthr) = ((mdr_c_selected_det_targetdeterminanthrc) + (mdr_f_selected_det_targetdeterminanthrc)) * S ((mdr_c_selected_det_targetdeterminanthrc) + (mdr_f_selected_det_targetdeterminanthrc)) + ((mdr_f_selected_det_targetdeterminanthrc) + (mdr_f_selected_det_targetdeterminanthrc))))))))) /\ (((exists ff_h_mdr_selected_det_targetdeterminanthrb. ff_h_mdr_selected_det_targetdeterminanthrb + S (mdr_z_selected_det_targetdeterminanthr) = S ((S (mdr_i_selected_det_targetdeterminanth)) * mdr_c_selected_det_targetdeterminant)) /\ exists ff_q_mdr_selected_det_targetdeterminanthrb. mdr_b_selected_det_targetdeterminant = ff_q_mdr_selected_det_targetdeterminanthrb * S ((S (mdr_i_selected_det_targetdeterminanth)) * mdr_c_selected_det_targetdeterminant) + (mdr_z_selected_det_targetdeterminanthr))))) /\ (((((mdr_d_selected_det_targetdeterminanth) = 0) /\ (((mdr_p_selected_det_targetdeterminanth) = 1) /\ ((mdr_n_selected_det_targetdeterminanth) = 0))) \/ exists mdr_q_selected_det_targetdeterminanths mdr_eb_selected_det_targetdeterminanths mdr_ec_selected_det_targetdeterminanths mdr_fb_selected_det_targetdeterminanths mdr_fc_selected_det_targetdeterminanths. (((mdr_d_selected_det_targetdeterminanth) = S (mdr_q_selected_det_targetdeterminanths)) /\ ((forall mdr_j_selected_det_targetdeterminanthsc. (exists mdr_gap_selected_det_targetdeterminanthscj. mdr_gap_selected_det_targetdeterminanthscj + S (mdr_j_selected_det_targetdeterminanthsc) = (S (mdr_q_selected_det_targetdeterminanths))) -> exists mdr_i_selected_det_targetdeterminanthsc mdr_up_selected_det_targetdeterminanthsc mdr_us_selected_det_targetdeterminanthsc mdr_un_selected_det_targetdeterminanthsc mdr_ut_selected_det_targetdeterminanthsc mdr_p_selected_det_targetdeterminanthsc mdr_n_selected_det_targetdeterminanthsc. ((exists mdr_gap_selected_det_targetdeterminanthsci. mdr_gap_selected_det_targetdeterminanthsci + S (mdr_i_selected_det_targetdeterminanthsc) = (mdr_i_selected_det_targetdeterminanth)) /\ ((exists mdr_z_selected_det_targetdeterminanthscr. ((exists mdr_a_selected_det_targetdeterminanthscrc mdr_b_selected_det_targetdeterminanthscrc mdr_c_selected_det_targetdeterminanthscrc mdr_e_selected_det_targetdeterminanthscrc mdr_f_selected_det_targetdeterminanthscrc. ((mdr_a_selected_det_targetdeterminanthscrc = ((mdr_q_selected_det_targetdeterminanths) + (mdr_up_selected_det_targetdeterminanthsc)) * S ((mdr_q_selected_det_targetdeterminanths) + (mdr_up_selected_det_targetdeterminanthsc)) + ((mdr_up_selected_det_targetdeterminanthsc) + (mdr_up_selected_det_targetdeterminanthsc))) /\ ((mdr_b_selected_det_targetdeterminanthscrc = ((mdr_us_selected_det_targetdeterminanthsc) + (mdr_un_selected_det_targetdeterminanthsc)) * S ((mdr_us_selected_det_targetdeterminanthsc) + (mdr_un_selected_det_targetdeterminanthsc)) + ((mdr_un_selected_det_targetdeterminanthsc) + (mdr_un_selected_det_targetdeterminanthsc))) /\ ((mdr_c_selected_det_targetdeterminanthscrc = ((mdr_a_selected_det_targetdeterminanthscrc) + (mdr_b_selected_det_targetdeterminanthscrc)) * S ((mdr_a_selected_det_targetdeterminanthscrc) + (mdr_b_selected_det_targetdeterminanthscrc)) + ((mdr_b_selected_det_targetdeterminanthscrc) + (mdr_b_selected_det_targetdeterminanthscrc))) /\ ((mdr_e_selected_det_targetdeterminanthscrc = ((mdr_p_selected_det_targetdeterminanthsc) + (mdr_n_selected_det_targetdeterminanthsc)) * S ((mdr_p_selected_det_targetdeterminanthsc) + (mdr_n_selected_det_targetdeterminanthsc)) + ((mdr_n_selected_det_targetdeterminanthsc) + (mdr_n_selected_det_targetdeterminanthsc))) /\ ((mdr_f_selected_det_targetdeterminanthscrc = ((mdr_ut_selected_det_targetdeterminanthsc) + (mdr_e_selected_det_targetdeterminanthscrc)) * S ((mdr_ut_selected_det_targetdeterminanthsc) + (mdr_e_selected_det_targetdeterminanthscrc)) + ((mdr_e_selected_det_targetdeterminanthscrc) + (mdr_e_selected_det_targetdeterminanthscrc))) /\ ((mdr_z_selected_det_targetdeterminanthscr) = ((mdr_c_selected_det_targetdeterminanthscrc) + (mdr_f_selected_det_targetdeterminanthscrc)) * S ((mdr_c_selected_det_targetdeterminanthscrc) + (mdr_f_selected_det_targetdeterminanthscrc)) + ((mdr_f_selected_det_targetdeterminanthscrc) + (mdr_f_selected_det_targetdeterminanthscrc))))))))) /\ (((exists ff_h_mdr_selected_det_targetdeterminanthscrb. ff_h_mdr_selected_det_targetdeterminanthscrb + S (mdr_z_selected_det_targetdeterminanthscr) = S ((S (mdr_i_selected_det_targetdeterminanthsc)) * mdr_c_selected_det_targetdeterminant)) /\ exists ff_q_mdr_selected_det_targetdeterminanthscrb. mdr_b_selected_det_targetdeterminant = ff_q_mdr_selected_det_targetdeterminanthscrb * S ((S (mdr_i_selected_det_targetdeterminanthsc)) * mdr_c_selected_det_targetdeterminant) + (mdr_z_selected_det_targetdeterminanthscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive. (exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_index_bound. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) = ((mdr_q_selected_det_targetdeterminanths) * (mdr_q_selected_det_targetdeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive. (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive = (mdr_q_selected_det_targetdeterminanths) * ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive + ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive /\ ((exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_column_bound. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) = (mdr_q_selected_det_targetdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell = ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_positive_cell_row_after. ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive)) /\ ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell = S ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) = (mdr_j_selected_det_targetdeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell = ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) \/ ((exists ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_positive_cell_column_after. ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_positive_cell_column_after + (mdr_j_selected_det_targetdeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive)) /\ ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell = S ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive))) /\ (((exists ff_h_mdm_mdr_selected_det_targetdeterminanthscm_positive_cell_source. ff_h_mdm_mdr_selected_det_targetdeterminanthscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) = S ((S ((ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell) * (S (mdr_q_selected_det_targetdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell))) * mdr_pc_selected_det_targetdeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_targetdeterminanthscm_positive_cell_source. mdr_pb_selected_det_targetdeterminanth = ff_q_mdm_mdr_selected_det_targetdeterminanthscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell) * (S (mdr_q_selected_det_targetdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_positive_cell))) * mdr_pc_selected_det_targetdeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive)))))) /\ (((exists ff_h_mdm_mdr_selected_det_targetdeterminanthscm_positive_target. ff_h_mdm_mdr_selected_det_targetdeterminanthscm_positive_target + S (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive) = S ((S (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive)) * mdr_us_selected_det_targetdeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_targetdeterminanthscm_positive_target. mdr_up_selected_det_targetdeterminanthsc = ff_q_mdm_mdr_selected_det_targetdeterminanthscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive)) * mdr_us_selected_det_targetdeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative. (exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_index_bound. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) = ((mdr_q_selected_det_targetdeterminanths) * (mdr_q_selected_det_targetdeterminanths))) -> exists ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative. (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative = (mdr_q_selected_det_targetdeterminanths) * ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative + ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative /\ ((exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_column_bound. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) = (mdr_q_selected_det_targetdeterminanths)) /\ ((exists ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell = ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_negative_cell_row_after. ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative)) /\ ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell = S ff_row_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_selected_det_targetdeterminanthscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) = (mdr_j_selected_det_targetdeterminanthsc)) /\ ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell = ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) \/ ((exists ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_negative_cell_column_after. ff_gap_mdm_le_mdr_selected_det_targetdeterminanthscm_negative_cell_column_after + (mdr_j_selected_det_targetdeterminanthsc) = (ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative)) /\ ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell = S ff_column_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative))) /\ (((exists ff_h_mdm_mdr_selected_det_targetdeterminanthscm_negative_cell_source. ff_h_mdm_mdr_selected_det_targetdeterminanthscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) = S ((S ((ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell) * (S (mdr_q_selected_det_targetdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell))) * mdr_nc_selected_det_targetdeterminanth)) /\ exists ff_q_mdm_mdr_selected_det_targetdeterminanthscm_negative_cell_source. mdr_nb_selected_det_targetdeterminanth = ff_q_mdm_mdr_selected_det_targetdeterminanthscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell) * (S (mdr_q_selected_det_targetdeterminanths)) + (ff_column_mdm_cell_mdr_selected_det_targetdeterminanthscm_negative_cell))) * mdr_nc_selected_det_targetdeterminanth) + (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative)))))) /\ (((exists ff_h_mdm_mdr_selected_det_targetdeterminanthscm_negative_target. ff_h_mdm_mdr_selected_det_targetdeterminanthscm_negative_target + S (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative) = S ((S (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative)) * mdr_ut_selected_det_targetdeterminanthsc)) /\ exists ff_q_mdm_mdr_selected_det_targetdeterminanthscm_negative_target. mdr_un_selected_det_targetdeterminanthsc = ff_q_mdm_mdr_selected_det_targetdeterminanthscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative)) * mdr_ut_selected_det_targetdeterminanthsc) + (ff_value_mdm_prefix_mdr_selected_det_targetdeterminanthscm_negative))))))))) /\ ((((exists ff_h_mdr_selected_det_targetdeterminanthscp. ff_h_mdr_selected_det_targetdeterminanthscp + S (mdr_p_selected_det_targetdeterminanthsc) = S ((S (mdr_j_selected_det_targetdeterminanthsc)) * mdr_ec_selected_det_targetdeterminanths)) /\ exists ff_q_mdr_selected_det_targetdeterminanthscp. mdr_eb_selected_det_targetdeterminanths = ff_q_mdr_selected_det_targetdeterminanthscp * S ((S (mdr_j_selected_det_targetdeterminanthsc)) * mdr_ec_selected_det_targetdeterminanths) + (mdr_p_selected_det_targetdeterminanthsc))) /\ (((exists ff_h_mdr_selected_det_targetdeterminanthscn. ff_h_mdr_selected_det_targetdeterminanthscn + S (mdr_n_selected_det_targetdeterminanthsc) = S ((S (mdr_j_selected_det_targetdeterminanthsc)) * mdr_fc_selected_det_targetdeterminanths)) /\ exists ff_q_mdr_selected_det_targetdeterminanthscn. mdr_fb_selected_det_targetdeterminanths = ff_q_mdr_selected_det_targetdeterminanthscn * S ((S (mdr_j_selected_det_targetdeterminanthsc)) * mdr_fc_selected_det_targetdeterminanths) + (mdr_n_selected_det_targetdeterminanthsc)))))))) /\ (exists ff_ub_mce_fold_mdr_selected_det_targetdeterminanthsf ff_uc_mce_fold_mdr_selected_det_targetdeterminanthsf ff_vb_mce_fold_mdr_selected_det_targetdeterminanthsf ff_vc_mce_fold_mdr_selected_det_targetdeterminanthsf. ((forall ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix. (exists ff_gap_mce_mdr_selected_det_targetdeterminanthsf_prefix_index. ff_gap_mce_mdr_selected_det_targetdeterminanthsf_prefix_index + S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) = (S (mdr_q_selected_det_targetdeterminanths))) -> exists ff_ap_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix ff_an_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix ff_bp_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix ff_bn_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix ff_p_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix ff_n_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix. ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_ap. ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_ap + S (ff_ap_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_pc_selected_det_targetdeterminanth)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_ap. mdr_pb_selected_det_targetdeterminanth = ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_pc_selected_det_targetdeterminanth) + (ff_ap_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_an. ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_an + S (ff_an_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_nc_selected_det_targetdeterminanth)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_an. mdr_nb_selected_det_targetdeterminanth = ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_nc_selected_det_targetdeterminanth) + (ff_an_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_bp. ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_bp + S (ff_bp_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_ec_selected_det_targetdeterminanths)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_bp. mdr_eb_selected_det_targetdeterminanths = ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_ec_selected_det_targetdeterminanths) + (ff_bp_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_bn. ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_bn + S (ff_bn_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_fc_selected_det_targetdeterminanths)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_bn. mdr_fb_selected_det_targetdeterminanths = ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * mdr_fc_selected_det_targetdeterminanths) + (ff_bn_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_positive. ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_positive + S (ff_p_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_targetdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_positive. ff_ub_mce_fold_mdr_selected_det_targetdeterminanthsf = ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * ff_uc_mce_fold_mdr_selected_det_targetdeterminanthsf) + (ff_p_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_negative. ff_h_mce_mdr_selected_det_targetdeterminanthsf_prefix_negative + S (ff_n_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) = S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_targetdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_negative. ff_vb_mce_fold_mdr_selected_det_targetdeterminanthsf = ff_q_mce_mdr_selected_det_targetdeterminanthsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix)) * ff_vc_mce_fold_mdr_selected_det_targetdeterminanthsf) + (ff_n_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))) /\ (((exists ff_even_mce_term_mdr_selected_det_targetdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix = 2 * ff_even_mce_term_mdr_selected_det_targetdeterminanthsf_prefix_term) /\ (ff_p_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_selected_det_targetdeterminanthsf_prefix_term. ff_index_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix = 2 * ff_odd_mce_term_mdr_selected_det_targetdeterminanthsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) /\ ff_n_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix = (ff_ap_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bp_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) + (ff_an_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix) * (ff_bn_mce_alternating_mdr_selected_det_targetdeterminanthsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_selected_det_targetdeterminanthsf_positive ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_start. ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_start. ff_u_mce_mdr_selected_det_targetdeterminanthsf_positive = ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_start * S ((S (0)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_terminal. ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_terminal + S (mdr_p_selected_det_targetdeterminanth) = S ((S ((S (mdr_q_selected_det_targetdeterminanths)))) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_terminal. ff_u_mce_mdr_selected_det_targetdeterminanthsf_positive = ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_terminal * S ((S ((S (mdr_q_selected_det_targetdeterminanths)))) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive) + (mdr_p_selected_det_targetdeterminanth))) /\ forall ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive. (exists ff_lt_mce_mdr_selected_det_targetdeterminanthsf_positive_bound. ff_lt_mce_mdr_selected_det_targetdeterminanthsf_positive_bound + S ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive = (S (mdr_q_selected_det_targetdeterminanths))) -> exists ff_a_mce_mdr_selected_det_targetdeterminanthsf_positive ff_r_mce_mdr_selected_det_targetdeterminanthsf_positive ff_s_mce_mdr_selected_det_targetdeterminanthsf_positive. ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_summand. ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_summand + S (ff_a_mce_mdr_selected_det_targetdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_targetdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_summand. ff_ub_mce_fold_mdr_selected_det_targetdeterminanthsf = ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_summand * S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive)) * ff_uc_mce_fold_mdr_selected_det_targetdeterminanthsf) + (ff_a_mce_mdr_selected_det_targetdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_partial. ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_partial + S (ff_r_mce_mdr_selected_det_targetdeterminanthsf_positive) = S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_partial. ff_u_mce_mdr_selected_det_targetdeterminanthsf_positive = ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_partial * S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive) + (ff_r_mce_mdr_selected_det_targetdeterminanthsf_positive))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_successor. ff_h_mce_mdr_selected_det_targetdeterminanthsf_positive_successor + S (ff_s_mce_mdr_selected_det_targetdeterminanthsf_positive) = S ((S (S ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_successor. ff_u_mce_mdr_selected_det_targetdeterminanthsf_positive = ff_q_mce_mdr_selected_det_targetdeterminanthsf_positive_successor * S ((S (S ff_i_mce_mdr_selected_det_targetdeterminanthsf_positive)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_positive) + (ff_s_mce_mdr_selected_det_targetdeterminanthsf_positive))) /\ ff_s_mce_mdr_selected_det_targetdeterminanthsf_positive = ff_r_mce_mdr_selected_det_targetdeterminanthsf_positive + ff_a_mce_mdr_selected_det_targetdeterminanthsf_positive)))))) /\ (exists ff_u_mce_mdr_selected_det_targetdeterminanthsf_negative ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_start. ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_start. ff_u_mce_mdr_selected_det_targetdeterminanthsf_negative = ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_start * S ((S (0)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_terminal. ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_terminal + S (mdr_n_selected_det_targetdeterminanth) = S ((S ((S (mdr_q_selected_det_targetdeterminanths)))) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_terminal. ff_u_mce_mdr_selected_det_targetdeterminanthsf_negative = ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_terminal * S ((S ((S (mdr_q_selected_det_targetdeterminanths)))) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative) + (mdr_n_selected_det_targetdeterminanth))) /\ forall ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative. (exists ff_lt_mce_mdr_selected_det_targetdeterminanthsf_negative_bound. ff_lt_mce_mdr_selected_det_targetdeterminanthsf_negative_bound + S ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative = (S (mdr_q_selected_det_targetdeterminanths))) -> exists ff_a_mce_mdr_selected_det_targetdeterminanthsf_negative ff_r_mce_mdr_selected_det_targetdeterminanthsf_negative ff_s_mce_mdr_selected_det_targetdeterminanthsf_negative. ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_summand. ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_summand + S (ff_a_mce_mdr_selected_det_targetdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_targetdeterminanthsf)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_summand. ff_vb_mce_fold_mdr_selected_det_targetdeterminanthsf = ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_summand * S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative)) * ff_vc_mce_fold_mdr_selected_det_targetdeterminanthsf) + (ff_a_mce_mdr_selected_det_targetdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_partial. ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_partial + S (ff_r_mce_mdr_selected_det_targetdeterminanthsf_negative) = S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_partial. ff_u_mce_mdr_selected_det_targetdeterminanthsf_negative = ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_partial * S ((S (ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative) + (ff_r_mce_mdr_selected_det_targetdeterminanthsf_negative))) /\ ((((exists ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_successor. ff_h_mce_mdr_selected_det_targetdeterminanthsf_negative_successor + S (ff_s_mce_mdr_selected_det_targetdeterminanthsf_negative) = S ((S (S ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative)) /\ exists ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_successor. ff_u_mce_mdr_selected_det_targetdeterminanthsf_negative = ff_q_mce_mdr_selected_det_targetdeterminanthsf_negative_successor * S ((S (S ff_i_mce_mdr_selected_det_targetdeterminanthsf_negative)) * ff_v_mce_mdr_selected_det_targetdeterminanthsf_negative) + (ff_s_mce_mdr_selected_det_targetdeterminanthsf_negative))) /\ ff_s_mce_mdr_selected_det_targetdeterminanthsf_negative = ff_r_mce_mdr_selected_det_targetdeterminanthsf_negative + ff_a_mce_mdr_selected_det_targetdeterminanthsf_negative))))))))))))))) /\ ((exists mdr_gap_selected_det_targetdeterminanti. mdr_gap_selected_det_targetdeterminanti + S (mdr_i_selected_det_targetdeterminant) = (mdr_l_selected_det_targetdeterminant)) /\ (exists mdr_z_selected_det_targetdeterminantr. ((exists mdr_a_selected_det_targetdeterminantrc mdr_b_selected_det_targetdeterminantrc mdr_c_selected_det_targetdeterminantrc mdr_e_selected_det_targetdeterminantrc mdr_f_selected_det_targetdeterminantrc. ((mdr_a_selected_det_targetdeterminantrc = ((q) + (mdr_ub_selected_det_target)) * S ((q) + (mdr_ub_selected_det_target)) + ((mdr_ub_selected_det_target) + (mdr_ub_selected_det_target))) /\ ((mdr_b_selected_det_targetdeterminantrc = ((mdr_uc_selected_det_target) + (mdr_vb_selected_det_target)) * S ((mdr_uc_selected_det_target) + (mdr_vb_selected_det_target)) + ((mdr_vb_selected_det_target) + (mdr_vb_selected_det_target))) /\ ((mdr_c_selected_det_targetdeterminantrc = ((mdr_a_selected_det_targetdeterminantrc) + (mdr_b_selected_det_targetdeterminantrc)) * S ((mdr_a_selected_det_targetdeterminantrc) + (mdr_b_selected_det_targetdeterminantrc)) + ((mdr_b_selected_det_targetdeterminantrc) + (mdr_b_selected_det_targetdeterminantrc))) /\ ((mdr_e_selected_det_targetdeterminantrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_selected_det_targetdeterminantrc = ((mdr_vc_selected_det_target) + (mdr_e_selected_det_targetdeterminantrc)) * S ((mdr_vc_selected_det_target) + (mdr_e_selected_det_targetdeterminantrc)) + ((mdr_e_selected_det_targetdeterminantrc) + (mdr_e_selected_det_targetdeterminantrc))) /\ ((mdr_z_selected_det_targetdeterminantr) = ((mdr_c_selected_det_targetdeterminantrc) + (mdr_f_selected_det_targetdeterminantrc)) * S ((mdr_c_selected_det_targetdeterminantrc) + (mdr_f_selected_det_targetdeterminantrc)) + ((mdr_f_selected_det_targetdeterminantrc) + (mdr_f_selected_det_targetdeterminantrc))))))))) /\ (((exists ff_h_mdr_selected_det_targetdeterminantrb. ff_h_mdr_selected_det_targetdeterminantrb + S (mdr_z_selected_det_targetdeterminantr) = S ((S (mdr_i_selected_det_targetdeterminant)) * mdr_c_selected_det_targetdeterminant)) /\ exists ff_q_mdr_selected_det_targetdeterminantrb. mdr_b_selected_det_targetdeterminant = ff_q_mdr_selected_det_targetdeterminantrb * S ((S (mdr_i_selected_det_targetdeterminant)) * mdr_c_selected_det_targetdeterminant) + (mdr_z_selected_det_targetdeterminantr))))))))))Complete tactic proof in conservative notation
All 52 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
52 script commands · 8 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–19
03Separate the logical casesL20–24
04Construct an explicit witnessL25–28
05Separate the logical casesL29–29
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L29
split
06Use earlier factsL30–39
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
specialize matrix_rank_signed_selected_selector_transport (pb) - L31
specialize matrix_rank_signed_selected_selector_transport (pc) - L32
specialize matrix_rank_signed_selected_selector_transport (nb) - L33
specialize matrix_rank_signed_selected_selector_transport (nc) - L34
specialize matrix_rank_signed_selected_selector_transport (w) - L35
specialize matrix_rank_signed_selected_selector_transport (rb) - L36
specialize matrix_rank_signed_selected_selector_transport (rc) - L37
specialize matrix_rank_signed_selected_selector_transport (cb) - L38
specialize matrix_rank_signed_selected_selector_transport (cc) - L39
specialize matrix_rank_signed_selected_selector_transport (q)
07Use earlier factsL40–49
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L40
specialize matrix_rank_signed_selected_selector_transport (Rb) - L41
specialize matrix_rank_signed_selected_selector_transport (Rc) - L42
specialize matrix_rank_signed_selected_selector_transport (Cb) - L43
specialize matrix_rank_signed_selected_selector_transport (Cc) - L44
specialize matrix_rank_signed_selected_selector_transport (x) - L45
specialize matrix_rank_signed_selected_selector_transport (x1) - L46
specialize matrix_rank_signed_selected_selector_transport (x2) - L47
specialize matrix_rank_signed_selected_selector_transport (x3) - L48
apply matrix_rank_signed_selected_selector_transport - L49
exact hrows
Original defined command ledger · 52 lines
- 0001
intro pb - 0002
intro pc - 0003
intro nb - 0004
intro nc - 0005
intro w - 0006
intro rb - 0007
intro rc - 0008
intro cb - 0009
intro cc - 0010
intro q - 0011
intro Rb - 0012
intro Rc - 0013
intro Cb - 0014
intro Cc - 0015
intro p - 0016
intro n - 0017
intro hrows - 0018
intro hcolumns - 0019
intro hdet - 0020
cases hdet - 0021
cases hdet_witness - 0022
cases hdet_witness_witness - 0023
cases hdet_witness_witness_witness - 0024
cases hdet_witness_witness_witness_witness - 0025
exists x - 0026
exists x1 - 0027
exists x2 - 0028
exists x3 - 0029
split - 0030
specialize matrix_rank_signed_selected_selector_transport (pb) - 0031
specialize matrix_rank_signed_selected_selector_transport (pc) - 0032
specialize matrix_rank_signed_selected_selector_transport (nb) - 0033
specialize matrix_rank_signed_selected_selector_transport (nc) - 0034
specialize matrix_rank_signed_selected_selector_transport (w) - 0035
specialize matrix_rank_signed_selected_selector_transport (rb) - 0036
specialize matrix_rank_signed_selected_selector_transport (rc) - 0037
specialize matrix_rank_signed_selected_selector_transport (cb) - 0038
specialize matrix_rank_signed_selected_selector_transport (cc) - 0039
specialize matrix_rank_signed_selected_selector_transport (q) - 0040
specialize matrix_rank_signed_selected_selector_transport (Rb) - 0041
specialize matrix_rank_signed_selected_selector_transport (Rc) - 0042
specialize matrix_rank_signed_selected_selector_transport (Cb) - 0043
specialize matrix_rank_signed_selected_selector_transport (Cc) - 0044
specialize matrix_rank_signed_selected_selector_transport (x) - 0045
specialize matrix_rank_signed_selected_selector_transport (x1) - 0046
specialize matrix_rank_signed_selected_selector_transport (x2) - 0047
specialize matrix_rank_signed_selected_selector_transport (x3) - 0048
apply matrix_rank_signed_selected_selector_transport - 0049
exact hrows - 0050
exact hcolumns - 0051
exact hdet_witness_witness_witness_witness_left - 0052
exact hdet_witness_witness_witness_witness_right