DL0013

signed_recursive_determinant_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every signed beta-coded square matrix has an actual finite strictly well-founded cofactor evaluation, with no bound on dimension and no assumed determinant oracle.

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.

Exact expanded first-order arithmetic statement

forall pb pc nb nc d. exists p n. (exists mdr_b_det_exists mdr_c_det_exists mdr_l_det_exists mdr_i_det_exists. ((forall mdr_i_det_existsh. (exists mdr_gap_det_existshi. mdr_gap_det_existshi + S (mdr_i_det_existsh) = (mdr_l_det_exists)) -> exists mdr_d_det_existsh mdr_pb_det_existsh mdr_pc_det_existsh mdr_nb_det_existsh mdr_nc_det_existsh mdr_p_det_existsh mdr_n_det_existsh. ((exists mdr_z_det_existshr. ((exists mdr_a_det_existshrc mdr_b_det_existshrc mdr_c_det_existshrc mdr_e_det_existshrc mdr_f_det_existshrc. ((mdr_a_det_existshrc = ((mdr_d_det_existsh) + (mdr_pb_det_existsh)) * S ((mdr_d_det_existsh) + (mdr_pb_det_existsh)) + ((mdr_pb_det_existsh) + (mdr_pb_det_existsh))) /\ ((mdr_b_det_existshrc = ((mdr_pc_det_existsh) + (mdr_nb_det_existsh)) * S ((mdr_pc_det_existsh) + (mdr_nb_det_existsh)) + ((mdr_nb_det_existsh) + (mdr_nb_det_existsh))) /\ ((mdr_c_det_existshrc = ((mdr_a_det_existshrc) + (mdr_b_det_existshrc)) * S ((mdr_a_det_existshrc) + (mdr_b_det_existshrc)) + ((mdr_b_det_existshrc) + (mdr_b_det_existshrc))) /\ ((mdr_e_det_existshrc = ((mdr_p_det_existsh) + (mdr_n_det_existsh)) * S ((mdr_p_det_existsh) + (mdr_n_det_existsh)) + ((mdr_n_det_existsh) + (mdr_n_det_existsh))) /\ ((mdr_f_det_existshrc = ((mdr_nc_det_existsh) + (mdr_e_det_existshrc)) * S ((mdr_nc_det_existsh) + (mdr_e_det_existshrc)) + ((mdr_e_det_existshrc) + (mdr_e_det_existshrc))) /\ ((mdr_z_det_existshr) = ((mdr_c_det_existshrc) + (mdr_f_det_existshrc)) * S ((mdr_c_det_existshrc) + (mdr_f_det_existshrc)) + ((mdr_f_det_existshrc) + (mdr_f_det_existshrc))))))))) /\ (((exists ff_h_mdr_det_existshrb. ff_h_mdr_det_existshrb + S (mdr_z_det_existshr) = S ((S (mdr_i_det_existsh)) * mdr_c_det_exists)) /\ exists ff_q_mdr_det_existshrb. mdr_b_det_exists = ff_q_mdr_det_existshrb * S ((S (mdr_i_det_existsh)) * mdr_c_det_exists) + (mdr_z_det_existshr))))) /\ (((((mdr_d_det_existsh) = 0) /\ (((mdr_p_det_existsh) = 1) /\ ((mdr_n_det_existsh) = 0))) \/ exists mdr_q_det_existshs mdr_eb_det_existshs mdr_ec_det_existshs mdr_fb_det_existshs mdr_fc_det_existshs. (((mdr_d_det_existsh) = S (mdr_q_det_existshs)) /\ ((forall mdr_j_det_existshsc. (exists mdr_gap_det_existshscj. mdr_gap_det_existshscj + S (mdr_j_det_existshsc) = (S (mdr_q_det_existshs))) -> exists mdr_i_det_existshsc mdr_up_det_existshsc mdr_us_det_existshsc mdr_un_det_existshsc mdr_ut_det_existshsc mdr_p_det_existshsc mdr_n_det_existshsc. ((exists mdr_gap_det_existshsci. mdr_gap_det_existshsci + S (mdr_i_det_existshsc) = (mdr_i_det_existsh)) /\ ((exists mdr_z_det_existshscr. ((exists mdr_a_det_existshscrc mdr_b_det_existshscrc mdr_c_det_existshscrc mdr_e_det_existshscrc mdr_f_det_existshscrc. ((mdr_a_det_existshscrc = ((mdr_q_det_existshs) + (mdr_up_det_existshsc)) * S ((mdr_q_det_existshs) + (mdr_up_det_existshsc)) + ((mdr_up_det_existshsc) + (mdr_up_det_existshsc))) /\ ((mdr_b_det_existshscrc = ((mdr_us_det_existshsc) + (mdr_un_det_existshsc)) * S ((mdr_us_det_existshsc) + (mdr_un_det_existshsc)) + ((mdr_un_det_existshsc) + (mdr_un_det_existshsc))) /\ ((mdr_c_det_existshscrc = ((mdr_a_det_existshscrc) + (mdr_b_det_existshscrc)) * S ((mdr_a_det_existshscrc) + (mdr_b_det_existshscrc)) + ((mdr_b_det_existshscrc) + (mdr_b_det_existshscrc))) /\ ((mdr_e_det_existshscrc = ((mdr_p_det_existshsc) + (mdr_n_det_existshsc)) * S ((mdr_p_det_existshsc) + (mdr_n_det_existshsc)) + ((mdr_n_det_existshsc) + (mdr_n_det_existshsc))) /\ ((mdr_f_det_existshscrc = ((mdr_ut_det_existshsc) + (mdr_e_det_existshscrc)) * S ((mdr_ut_det_existshsc) + (mdr_e_det_existshscrc)) + ((mdr_e_det_existshscrc) + (mdr_e_det_existshscrc))) /\ ((mdr_z_det_existshscr) = ((mdr_c_det_existshscrc) + (mdr_f_det_existshscrc)) * S ((mdr_c_det_existshscrc) + (mdr_f_det_existshscrc)) + ((mdr_f_det_existshscrc) + (mdr_f_det_existshscrc))))))))) /\ (((exists ff_h_mdr_det_existshscrb. ff_h_mdr_det_existshscrb + S (mdr_z_det_existshscr) = S ((S (mdr_i_det_existshsc)) * mdr_c_det_exists)) /\ exists ff_q_mdr_det_existshscrb. mdr_b_det_exists = ff_q_mdr_det_existshscrb * S ((S (mdr_i_det_existshsc)) * mdr_c_det_exists) + (mdr_z_det_existshscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_det_existshscm_positive. (exists ff_gap_mdm_lt_mdr_det_existshscm_positive_index_bound. ff_gap_mdm_lt_mdr_det_existshscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_det_existshscm_positive) = ((mdr_q_det_existshs) * (mdr_q_det_existshs))) -> exists ff_row_mdm_prefix_mdr_det_existshscm_positive ff_column_mdm_prefix_mdr_det_existshscm_positive ff_value_mdm_prefix_mdr_det_existshscm_positive. (ff_index_mdm_prefix_mdr_det_existshscm_positive = (mdr_q_det_existshs) * ff_row_mdm_prefix_mdr_det_existshscm_positive + ff_column_mdm_prefix_mdr_det_existshscm_positive /\ ((exists ff_gap_mdm_lt_mdr_det_existshscm_positive_column_bound. ff_gap_mdm_lt_mdr_det_existshscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_det_existshscm_positive) = (mdr_q_det_existshs)) /\ ((exists ff_row_mdm_cell_mdr_det_existshscm_positive_cell ff_column_mdm_cell_mdr_det_existshscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_det_existshscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_det_existshscm_positive_cell = ff_row_mdm_prefix_mdr_det_existshscm_positive) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_positive_cell_row_after. ff_gap_mdm_le_mdr_det_existshscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_det_existshscm_positive)) /\ ff_row_mdm_cell_mdr_det_existshscm_positive_cell = S ff_row_mdm_prefix_mdr_det_existshscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_det_existshscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_det_existshscm_positive) = (mdr_j_det_existshsc)) /\ ff_column_mdm_cell_mdr_det_existshscm_positive_cell = ff_column_mdm_prefix_mdr_det_existshscm_positive) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_positive_cell_column_after. ff_gap_mdm_le_mdr_det_existshscm_positive_cell_column_after + (mdr_j_det_existshsc) = (ff_column_mdm_prefix_mdr_det_existshscm_positive)) /\ ff_column_mdm_cell_mdr_det_existshscm_positive_cell = S ff_column_mdm_prefix_mdr_det_existshscm_positive))) /\ (((exists ff_h_mdm_mdr_det_existshscm_positive_cell_source. ff_h_mdm_mdr_det_existshscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_det_existshscm_positive) = S ((S ((ff_row_mdm_cell_mdr_det_existshscm_positive_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_positive_cell))) * mdr_pc_det_existsh)) /\ exists ff_q_mdm_mdr_det_existshscm_positive_cell_source. mdr_pb_det_existsh = ff_q_mdm_mdr_det_existshscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_det_existshscm_positive_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_positive_cell))) * mdr_pc_det_existsh) + (ff_value_mdm_prefix_mdr_det_existshscm_positive)))))) /\ (((exists ff_h_mdm_mdr_det_existshscm_positive_target. ff_h_mdm_mdr_det_existshscm_positive_target + S (ff_value_mdm_prefix_mdr_det_existshscm_positive) = S ((S (ff_index_mdm_prefix_mdr_det_existshscm_positive)) * mdr_us_det_existshsc)) /\ exists ff_q_mdm_mdr_det_existshscm_positive_target. mdr_up_det_existshsc = ff_q_mdm_mdr_det_existshscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_det_existshscm_positive)) * mdr_us_det_existshsc) + (ff_value_mdm_prefix_mdr_det_existshscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_det_existshscm_negative. (exists ff_gap_mdm_lt_mdr_det_existshscm_negative_index_bound. ff_gap_mdm_lt_mdr_det_existshscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_det_existshscm_negative) = ((mdr_q_det_existshs) * (mdr_q_det_existshs))) -> exists ff_row_mdm_prefix_mdr_det_existshscm_negative ff_column_mdm_prefix_mdr_det_existshscm_negative ff_value_mdm_prefix_mdr_det_existshscm_negative. (ff_index_mdm_prefix_mdr_det_existshscm_negative = (mdr_q_det_existshs) * ff_row_mdm_prefix_mdr_det_existshscm_negative + ff_column_mdm_prefix_mdr_det_existshscm_negative /\ ((exists ff_gap_mdm_lt_mdr_det_existshscm_negative_column_bound. ff_gap_mdm_lt_mdr_det_existshscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_det_existshscm_negative) = (mdr_q_det_existshs)) /\ ((exists ff_row_mdm_cell_mdr_det_existshscm_negative_cell ff_column_mdm_cell_mdr_det_existshscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_det_existshscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_det_existshscm_negative_cell = ff_row_mdm_prefix_mdr_det_existshscm_negative) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_negative_cell_row_after. ff_gap_mdm_le_mdr_det_existshscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_det_existshscm_negative)) /\ ff_row_mdm_cell_mdr_det_existshscm_negative_cell = S ff_row_mdm_prefix_mdr_det_existshscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_det_existshscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_det_existshscm_negative) = (mdr_j_det_existshsc)) /\ ff_column_mdm_cell_mdr_det_existshscm_negative_cell = ff_column_mdm_prefix_mdr_det_existshscm_negative) \/ ((exists ff_gap_mdm_le_mdr_det_existshscm_negative_cell_column_after. ff_gap_mdm_le_mdr_det_existshscm_negative_cell_column_after + (mdr_j_det_existshsc) = (ff_column_mdm_prefix_mdr_det_existshscm_negative)) /\ ff_column_mdm_cell_mdr_det_existshscm_negative_cell = S ff_column_mdm_prefix_mdr_det_existshscm_negative))) /\ (((exists ff_h_mdm_mdr_det_existshscm_negative_cell_source. ff_h_mdm_mdr_det_existshscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_det_existshscm_negative) = S ((S ((ff_row_mdm_cell_mdr_det_existshscm_negative_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_negative_cell))) * mdr_nc_det_existsh)) /\ exists ff_q_mdm_mdr_det_existshscm_negative_cell_source. mdr_nb_det_existsh = ff_q_mdm_mdr_det_existshscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_det_existshscm_negative_cell) * (S (mdr_q_det_existshs)) + (ff_column_mdm_cell_mdr_det_existshscm_negative_cell))) * mdr_nc_det_existsh) + (ff_value_mdm_prefix_mdr_det_existshscm_negative)))))) /\ (((exists ff_h_mdm_mdr_det_existshscm_negative_target. ff_h_mdm_mdr_det_existshscm_negative_target + S (ff_value_mdm_prefix_mdr_det_existshscm_negative) = S ((S (ff_index_mdm_prefix_mdr_det_existshscm_negative)) * mdr_ut_det_existshsc)) /\ exists ff_q_mdm_mdr_det_existshscm_negative_target. mdr_un_det_existshsc = ff_q_mdm_mdr_det_existshscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_det_existshscm_negative)) * mdr_ut_det_existshsc) + (ff_value_mdm_prefix_mdr_det_existshscm_negative))))))))) /\ ((((exists ff_h_mdr_det_existshscp. ff_h_mdr_det_existshscp + S (mdr_p_det_existshsc) = S ((S (mdr_j_det_existshsc)) * mdr_ec_det_existshs)) /\ exists ff_q_mdr_det_existshscp. mdr_eb_det_existshs = ff_q_mdr_det_existshscp * S ((S (mdr_j_det_existshsc)) * mdr_ec_det_existshs) + (mdr_p_det_existshsc))) /\ (((exists ff_h_mdr_det_existshscn. ff_h_mdr_det_existshscn + S (mdr_n_det_existshsc) = S ((S (mdr_j_det_existshsc)) * mdr_fc_det_existshs)) /\ exists ff_q_mdr_det_existshscn. mdr_fb_det_existshs = ff_q_mdr_det_existshscn * S ((S (mdr_j_det_existshsc)) * mdr_fc_det_existshs) + (mdr_n_det_existshsc)))))))) /\ (exists ff_ub_mce_fold_mdr_det_existshsf ff_uc_mce_fold_mdr_det_existshsf ff_vb_mce_fold_mdr_det_existshsf ff_vc_mce_fold_mdr_det_existshsf. ((forall ff_index_mce_alternating_mdr_det_existshsf_prefix. (exists ff_gap_mce_mdr_det_existshsf_prefix_index. ff_gap_mce_mdr_det_existshsf_prefix_index + S (ff_index_mce_alternating_mdr_det_existshsf_prefix) = (S (mdr_q_det_existshs))) -> exists ff_ap_mce_alternating_mdr_det_existshsf_prefix ff_an_mce_alternating_mdr_det_existshsf_prefix ff_bp_mce_alternating_mdr_det_existshsf_prefix ff_bn_mce_alternating_mdr_det_existshsf_prefix ff_p_mce_alternating_mdr_det_existshsf_prefix ff_n_mce_alternating_mdr_det_existshsf_prefix. ((((exists ff_h_mce_mdr_det_existshsf_prefix_ap. ff_h_mce_mdr_det_existshsf_prefix_ap + S (ff_ap_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_pc_det_existsh)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_ap. mdr_pb_det_existsh = ff_q_mce_mdr_det_existshsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_pc_det_existsh) + (ff_ap_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_an. ff_h_mce_mdr_det_existshsf_prefix_an + S (ff_an_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_nc_det_existsh)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_an. mdr_nb_det_existsh = ff_q_mce_mdr_det_existshsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_nc_det_existsh) + (ff_an_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_bp. ff_h_mce_mdr_det_existshsf_prefix_bp + S (ff_bp_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_ec_det_existshs)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_bp. mdr_eb_det_existshs = ff_q_mce_mdr_det_existshsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_ec_det_existshs) + (ff_bp_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_bn. ff_h_mce_mdr_det_existshsf_prefix_bn + S (ff_bn_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_fc_det_existshs)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_bn. mdr_fb_det_existshs = ff_q_mce_mdr_det_existshsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * mdr_fc_det_existshs) + (ff_bn_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_positive. ff_h_mce_mdr_det_existshsf_prefix_positive + S (ff_p_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_uc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_positive. ff_ub_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_uc_mce_fold_mdr_det_existshsf) + (ff_p_mce_alternating_mdr_det_existshsf_prefix))) /\ ((((exists ff_h_mce_mdr_det_existshsf_prefix_negative. ff_h_mce_mdr_det_existshsf_prefix_negative + S (ff_n_mce_alternating_mdr_det_existshsf_prefix) = S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_vc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_prefix_negative. ff_vb_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_det_existshsf_prefix)) * ff_vc_mce_fold_mdr_det_existshsf) + (ff_n_mce_alternating_mdr_det_existshsf_prefix))) /\ (((exists ff_even_mce_term_mdr_det_existshsf_prefix_term. ff_index_mce_alternating_mdr_det_existshsf_prefix = 2 * ff_even_mce_term_mdr_det_existshsf_prefix_term) /\ (ff_p_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix) /\ ff_n_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_det_existshsf_prefix_term. ff_index_mce_alternating_mdr_det_existshsf_prefix = 2 * ff_odd_mce_term_mdr_det_existshsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix) /\ ff_n_mce_alternating_mdr_det_existshsf_prefix = (ff_ap_mce_alternating_mdr_det_existshsf_prefix) * (ff_bp_mce_alternating_mdr_det_existshsf_prefix) + (ff_an_mce_alternating_mdr_det_existshsf_prefix) * (ff_bn_mce_alternating_mdr_det_existshsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_det_existshsf_positive ff_v_mce_mdr_det_existshsf_positive. ((((exists ff_h_mce_mdr_det_existshsf_positive_start. ff_h_mce_mdr_det_existshsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_start. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_start * S ((S (0)) * ff_v_mce_mdr_det_existshsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_det_existshsf_positive_terminal. ff_h_mce_mdr_det_existshsf_positive_terminal + S (mdr_p_det_existsh) = S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_terminal. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_terminal * S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_positive) + (mdr_p_det_existsh))) /\ forall ff_i_mce_mdr_det_existshsf_positive. (exists ff_lt_mce_mdr_det_existshsf_positive_bound. ff_lt_mce_mdr_det_existshsf_positive_bound + S ff_i_mce_mdr_det_existshsf_positive = (S (mdr_q_det_existshs))) -> exists ff_a_mce_mdr_det_existshsf_positive ff_r_mce_mdr_det_existshsf_positive ff_s_mce_mdr_det_existshsf_positive. ((((exists ff_h_mce_mdr_det_existshsf_positive_summand. ff_h_mce_mdr_det_existshsf_positive_summand + S (ff_a_mce_mdr_det_existshsf_positive) = S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_uc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_positive_summand. ff_ub_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_positive_summand * S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_uc_mce_fold_mdr_det_existshsf) + (ff_a_mce_mdr_det_existshsf_positive))) /\ ((((exists ff_h_mce_mdr_det_existshsf_positive_partial. ff_h_mce_mdr_det_existshsf_positive_partial + S (ff_r_mce_mdr_det_existshsf_positive) = S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_partial. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_partial * S ((S (ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive) + (ff_r_mce_mdr_det_existshsf_positive))) /\ ((((exists ff_h_mce_mdr_det_existshsf_positive_successor. ff_h_mce_mdr_det_existshsf_positive_successor + S (ff_s_mce_mdr_det_existshsf_positive) = S ((S (S ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive)) /\ exists ff_q_mce_mdr_det_existshsf_positive_successor. ff_u_mce_mdr_det_existshsf_positive = ff_q_mce_mdr_det_existshsf_positive_successor * S ((S (S ff_i_mce_mdr_det_existshsf_positive)) * ff_v_mce_mdr_det_existshsf_positive) + (ff_s_mce_mdr_det_existshsf_positive))) /\ ff_s_mce_mdr_det_existshsf_positive = ff_r_mce_mdr_det_existshsf_positive + ff_a_mce_mdr_det_existshsf_positive)))))) /\ (exists ff_u_mce_mdr_det_existshsf_negative ff_v_mce_mdr_det_existshsf_negative. ((((exists ff_h_mce_mdr_det_existshsf_negative_start. ff_h_mce_mdr_det_existshsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_start. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_start * S ((S (0)) * ff_v_mce_mdr_det_existshsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_det_existshsf_negative_terminal. ff_h_mce_mdr_det_existshsf_negative_terminal + S (mdr_n_det_existsh) = S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_terminal. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_terminal * S ((S ((S (mdr_q_det_existshs)))) * ff_v_mce_mdr_det_existshsf_negative) + (mdr_n_det_existsh))) /\ forall ff_i_mce_mdr_det_existshsf_negative. (exists ff_lt_mce_mdr_det_existshsf_negative_bound. ff_lt_mce_mdr_det_existshsf_negative_bound + S ff_i_mce_mdr_det_existshsf_negative = (S (mdr_q_det_existshs))) -> exists ff_a_mce_mdr_det_existshsf_negative ff_r_mce_mdr_det_existshsf_negative ff_s_mce_mdr_det_existshsf_negative. ((((exists ff_h_mce_mdr_det_existshsf_negative_summand. ff_h_mce_mdr_det_existshsf_negative_summand + S (ff_a_mce_mdr_det_existshsf_negative) = S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_vc_mce_fold_mdr_det_existshsf)) /\ exists ff_q_mce_mdr_det_existshsf_negative_summand. ff_vb_mce_fold_mdr_det_existshsf = ff_q_mce_mdr_det_existshsf_negative_summand * S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_vc_mce_fold_mdr_det_existshsf) + (ff_a_mce_mdr_det_existshsf_negative))) /\ ((((exists ff_h_mce_mdr_det_existshsf_negative_partial. ff_h_mce_mdr_det_existshsf_negative_partial + S (ff_r_mce_mdr_det_existshsf_negative) = S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_partial. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_partial * S ((S (ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative) + (ff_r_mce_mdr_det_existshsf_negative))) /\ ((((exists ff_h_mce_mdr_det_existshsf_negative_successor. ff_h_mce_mdr_det_existshsf_negative_successor + S (ff_s_mce_mdr_det_existshsf_negative) = S ((S (S ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative)) /\ exists ff_q_mce_mdr_det_existshsf_negative_successor. ff_u_mce_mdr_det_existshsf_negative = ff_q_mce_mdr_det_existshsf_negative_successor * S ((S (S ff_i_mce_mdr_det_existshsf_negative)) * ff_v_mce_mdr_det_existshsf_negative) + (ff_s_mce_mdr_det_existshsf_negative))) /\ ff_s_mce_mdr_det_existshsf_negative = ff_r_mce_mdr_det_existshsf_negative + ff_a_mce_mdr_det_existshsf_negative))))))))))))))) /\ ((exists mdr_gap_det_existsi. mdr_gap_det_existsi + S (mdr_i_det_exists) = (mdr_l_det_exists)) /\ (exists mdr_z_det_existsr. ((exists mdr_a_det_existsrc mdr_b_det_existsrc mdr_c_det_existsrc mdr_e_det_existsrc mdr_f_det_existsrc. ((mdr_a_det_existsrc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_det_existsrc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_det_existsrc = ((mdr_a_det_existsrc) + (mdr_b_det_existsrc)) * S ((mdr_a_det_existsrc) + (mdr_b_det_existsrc)) + ((mdr_b_det_existsrc) + (mdr_b_det_existsrc))) /\ ((mdr_e_det_existsrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_det_existsrc = ((nc) + (mdr_e_det_existsrc)) * S ((nc) + (mdr_e_det_existsrc)) + ((mdr_e_det_existsrc) + (mdr_e_det_existsrc))) /\ ((mdr_z_det_existsr) = ((mdr_c_det_existsrc) + (mdr_f_det_existsrc)) * S ((mdr_c_det_existsrc) + (mdr_f_det_existsrc)) + ((mdr_f_det_existsrc) + (mdr_f_det_existsrc))))))))) /\ (((exists ff_h_mdr_det_existsrb. ff_h_mdr_det_existsrb + S (mdr_z_det_existsr) = S ((S (mdr_i_det_exists)) * mdr_c_det_exists)) /\ exists ff_q_mdr_det_existsrb. mdr_b_det_exists = ff_q_mdr_det_existsrb * S ((S (mdr_i_det_exists)) * mdr_c_det_exists) + (mdr_z_det_existsr))))))))

Constructive proof overview

Generated structural guide

Every signed beta-coded square matrix has an actual finite strictly well-founded cofactor evaluation, with no bound on dimension and no assumed determinant oracle.

The unchanged tactic script uses 3 declared prerequisites and contains 37 exact native proof lines.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

le_refl Stable theorem; checked-use authorized DL0007 matrix_recursive_empty_history DL0012 matrix_recursive_all_extensions

Direct dependents

DL0028 signed_recursive_determinant_exists_unique DL0029 signed_recursive_determinant_from_evaluated_cofactors DL0049 matrix_rank_selected_determinant_exists DL00A7 absolute_recursive_determinant_exists DL00A9 absolute_recursive_determinant_integer_transport

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

37 script commands · 9 reading checkpoints · 1 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.

Named ingredients (2)
matrix recursive empty historymatrix recursive all extensions

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro pb
  2. L2
    intro pc
  3. L3
    intro nb
  4. L4
    intro nc
  5. L5
    intro d
02Establish hevaluationL6–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix recursive all extensions.

  1. L6
    have hevaluation : ∃ u. ∃ v. ∃ t. ∃ p. ∃ n. (∀ x. ∀ y. Lt(x,0) → BetaAt(0,0,x,y) → BetaAt(u,v,x,y)) ∧ (Le(0,t) ∧ (SignedDeterminantHistory(u,v,S t) ∧ SignedDeterminantNodeAt(u,v,t,d,pb,pc,nb,nc,p,n)))Definitions: SignedDeterminantNodeAtSignedDeterminantHistoryLeLtBetaAt
  2. L7
    specialize matrix_recursive_all_extensions (d)
  3. L8
    specialize matrix_recursive_all_extensions (pb)
  4. L9
    specialize matrix_recursive_all_extensions (pc)
  5. L10
    specialize matrix_recursive_all_extensions (nb)
  6. L11
    specialize matrix_recursive_all_extensions (nc)
  7. L12
    specialize matrix_recursive_all_extensions (0)
  8. L13
    specialize matrix_recursive_all_extensions (0)
  9. L14
    specialize matrix_recursive_all_extensions (0)
  10. L15
    apply matrix_recursive_all_extensions
03Use earlier factsL16–18

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

  1. L16
    specialize matrix_recursive_empty_history (0)
  2. L17
    specialize matrix_recursive_empty_history (0)
  3. L18
    apply matrix_recursive_empty_history
04Separate the logical casesL19–26

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

  1. L19
    cases hevaluation
  2. L20
    cases hevaluation_witness
  3. L21
    cases hevaluation_witness_witness
  4. L22
    cases hevaluation_witness_witness_witness
  5. L23
    cases hevaluation_witness_witness_witness_witness
  6. L24
    cases hevaluation_witness_witness_witness_witness_witness
  7. L25
    cases hevaluation_witness_witness_witness_witness_witness_right
  8. L26
    cases hevaluation_witness_witness_witness_witness_witness_right_right
05Construct an explicit witnessL27–32

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists x3
  2. L28
    exists x4
  3. L29
    exists x
  4. L30
    exists x1
  5. L31
    exists S x2
  6. L32
    exists x2
06Separate the logical casesL33–33

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

  1. L33
    split
07Use earlier factsL34–34

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

  1. L34
    exact hevaluation_witness_witness_witness_witness_witness_right_right_left
08Separate the logical casesL35–35

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

  1. L35
    split
09Use earlier factsL36–37

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

  1. L36
    apply le_refl
  2. L37
    exact hevaluation_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 37 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro d
  6. 0006have hevaluation : exists u v t p n. (((forall mdr_i_existence_evalp mdr_a_existence_evalp. (exists mdr_gap_existence_evalpb. mdr_gap_existence_evalpb + S (mdr_i_existence_evalp) = (0)) -> (((exists ff_h_mdr_existence_evalpo. ff_h_mdr_existence_evalpo + S (mdr_a_existence_evalp) = S ((S (mdr_i_existence_evalp)) * 0)) /\ exists ff_q_mdr_existence_evalpo. 0 = ff_q_mdr_existence_evalpo * S ((S (mdr_i_existence_evalp)) * 0) + (mdr_a_existence_evalp))) -> (((exists ff_h_mdr_existence_evalpn. ff_h_mdr_existence_evalpn + S (mdr_a_existence_evalp) = S ((S (mdr_i_existence_evalp)) * v)) /\ exists ff_q_mdr_existence_evalpn. u = ff_q_mdr_existence_evalpn * S ((S (mdr_i_existence_evalp)) * v) + (mdr_a_existence_evalp)))) /\ ((exists mdr_gap_existence_evall. mdr_gap_existence_evall + (0) = (t)) /\ ((forall mdr_i_existence_evalh. (exists mdr_gap_existence_evalhi. mdr_gap_existence_evalhi + S (mdr_i_existence_evalh) = (S (t))) -> exists mdr_d_existence_evalh mdr_pb_existence_evalh mdr_pc_existence_evalh mdr_nb_existence_evalh mdr_nc_existence_evalh mdr_p_existence_evalh mdr_n_existence_evalh. ((exists mdr_z_existence_evalhr. ((exists mdr_a_existence_evalhrc mdr_b_existence_evalhrc mdr_c_existence_evalhrc mdr_e_existence_evalhrc mdr_f_existence_evalhrc. ((mdr_a_existence_evalhrc = ((mdr_d_existence_evalh) + (mdr_pb_existence_evalh)) * S ((mdr_d_existence_evalh) + (mdr_pb_existence_evalh)) + ((mdr_pb_existence_evalh) + (mdr_pb_existence_evalh))) /\ ((mdr_b_existence_evalhrc = ((mdr_pc_existence_evalh) + (mdr_nb_existence_evalh)) * S ((mdr_pc_existence_evalh) + (mdr_nb_existence_evalh)) + ((mdr_nb_existence_evalh) + (mdr_nb_existence_evalh))) /\ ((mdr_c_existence_evalhrc = ((mdr_a_existence_evalhrc) + (mdr_b_existence_evalhrc)) * S ((mdr_a_existence_evalhrc) + (mdr_b_existence_evalhrc)) + ((mdr_b_existence_evalhrc) + (mdr_b_existence_evalhrc))) /\ ((mdr_e_existence_evalhrc = ((mdr_p_existence_evalh) + (mdr_n_existence_evalh)) * S ((mdr_p_existence_evalh) + (mdr_n_existence_evalh)) + ((mdr_n_existence_evalh) + (mdr_n_existence_evalh))) /\ ((mdr_f_existence_evalhrc = ((mdr_nc_existence_evalh) + (mdr_e_existence_evalhrc)) * S ((mdr_nc_existence_evalh) + (mdr_e_existence_evalhrc)) + ((mdr_e_existence_evalhrc) + (mdr_e_existence_evalhrc))) /\ ((mdr_z_existence_evalhr) = ((mdr_c_existence_evalhrc) + (mdr_f_existence_evalhrc)) * S ((mdr_c_existence_evalhrc) + (mdr_f_existence_evalhrc)) + ((mdr_f_existence_evalhrc) + (mdr_f_existence_evalhrc))))))))) /\ (((exists ff_h_mdr_existence_evalhrb. ff_h_mdr_existence_evalhrb + S (mdr_z_existence_evalhr) = S ((S (mdr_i_existence_evalh)) * v)) /\ exists ff_q_mdr_existence_evalhrb. u = ff_q_mdr_existence_evalhrb * S ((S (mdr_i_existence_evalh)) * v) + (mdr_z_existence_evalhr))))) /\ (((((mdr_d_existence_evalh) = 0) /\ (((mdr_p_existence_evalh) = 1) /\ ((mdr_n_existence_evalh) = 0))) \/ exists mdr_q_existence_evalhs mdr_eb_existence_evalhs mdr_ec_existence_evalhs mdr_fb_existence_evalhs mdr_fc_existence_evalhs. (((mdr_d_existence_evalh) = S (mdr_q_existence_evalhs)) /\ ((forall mdr_j_existence_evalhsc. (exists mdr_gap_existence_evalhscj. mdr_gap_existence_evalhscj + S (mdr_j_existence_evalhsc) = (S (mdr_q_existence_evalhs))) -> exists mdr_i_existence_evalhsc mdr_up_existence_evalhsc mdr_us_existence_evalhsc mdr_un_existence_evalhsc mdr_ut_existence_evalhsc mdr_p_existence_evalhsc mdr_n_existence_evalhsc. ((exists mdr_gap_existence_evalhsci. mdr_gap_existence_evalhsci + S (mdr_i_existence_evalhsc) = (mdr_i_existence_evalh)) /\ ((exists mdr_z_existence_evalhscr. ((exists mdr_a_existence_evalhscrc mdr_b_existence_evalhscrc mdr_c_existence_evalhscrc mdr_e_existence_evalhscrc mdr_f_existence_evalhscrc. ((mdr_a_existence_evalhscrc = ((mdr_q_existence_evalhs) + (mdr_up_existence_evalhsc)) * S ((mdr_q_existence_evalhs) + (mdr_up_existence_evalhsc)) + ((mdr_up_existence_evalhsc) + (mdr_up_existence_evalhsc))) /\ ((mdr_b_existence_evalhscrc = ((mdr_us_existence_evalhsc) + (mdr_un_existence_evalhsc)) * S ((mdr_us_existence_evalhsc) + (mdr_un_existence_evalhsc)) + ((mdr_un_existence_evalhsc) + (mdr_un_existence_evalhsc))) /\ ((mdr_c_existence_evalhscrc = ((mdr_a_existence_evalhscrc) + (mdr_b_existence_evalhscrc)) * S ((mdr_a_existence_evalhscrc) + (mdr_b_existence_evalhscrc)) + ((mdr_b_existence_evalhscrc) + (mdr_b_existence_evalhscrc))) /\ ((mdr_e_existence_evalhscrc = ((mdr_p_existence_evalhsc) + (mdr_n_existence_evalhsc)) * S ((mdr_p_existence_evalhsc) + (mdr_n_existence_evalhsc)) + ((mdr_n_existence_evalhsc) + (mdr_n_existence_evalhsc))) /\ ((mdr_f_existence_evalhscrc = ((mdr_ut_existence_evalhsc) + (mdr_e_existence_evalhscrc)) * S ((mdr_ut_existence_evalhsc) + (mdr_e_existence_evalhscrc)) + ((mdr_e_existence_evalhscrc) + (mdr_e_existence_evalhscrc))) /\ ((mdr_z_existence_evalhscr) = ((mdr_c_existence_evalhscrc) + (mdr_f_existence_evalhscrc)) * S ((mdr_c_existence_evalhscrc) + (mdr_f_existence_evalhscrc)) + ((mdr_f_existence_evalhscrc) + (mdr_f_existence_evalhscrc))))))))) /\ (((exists ff_h_mdr_existence_evalhscrb. ff_h_mdr_existence_evalhscrb + S (mdr_z_existence_evalhscr) = S ((S (mdr_i_existence_evalhsc)) * v)) /\ exists ff_q_mdr_existence_evalhscrb. u = ff_q_mdr_existence_evalhscrb * S ((S (mdr_i_existence_evalhsc)) * v) + (mdr_z_existence_evalhscr))))) /\ ((((forall ff_index_mdm_prefix_mdr_existence_evalhscm_positive. (exists ff_gap_mdm_lt_mdr_existence_evalhscm_positive_index_bound. ff_gap_mdm_lt_mdr_existence_evalhscm_positive_index_bound + S (ff_index_mdm_prefix_mdr_existence_evalhscm_positive) = ((mdr_q_existence_evalhs) * (mdr_q_existence_evalhs))) -> exists ff_row_mdm_prefix_mdr_existence_evalhscm_positive ff_column_mdm_prefix_mdr_existence_evalhscm_positive ff_value_mdm_prefix_mdr_existence_evalhscm_positive. (ff_index_mdm_prefix_mdr_existence_evalhscm_positive = (mdr_q_existence_evalhs) * ff_row_mdm_prefix_mdr_existence_evalhscm_positive + ff_column_mdm_prefix_mdr_existence_evalhscm_positive /\ ((exists ff_gap_mdm_lt_mdr_existence_evalhscm_positive_column_bound. ff_gap_mdm_lt_mdr_existence_evalhscm_positive_column_bound + S (ff_column_mdm_prefix_mdr_existence_evalhscm_positive) = (mdr_q_existence_evalhs)) /\ ((exists ff_row_mdm_cell_mdr_existence_evalhscm_positive_cell ff_column_mdm_cell_mdr_existence_evalhscm_positive_cell. (((((exists ff_gap_mdm_lt_mdr_existence_evalhscm_positive_cell_row_before. ff_gap_mdm_lt_mdr_existence_evalhscm_positive_cell_row_before + S (ff_row_mdm_prefix_mdr_existence_evalhscm_positive) = (0)) /\ ff_row_mdm_cell_mdr_existence_evalhscm_positive_cell = ff_row_mdm_prefix_mdr_existence_evalhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_existence_evalhscm_positive_cell_row_after. ff_gap_mdm_le_mdr_existence_evalhscm_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_existence_evalhscm_positive)) /\ ff_row_mdm_cell_mdr_existence_evalhscm_positive_cell = S ff_row_mdm_prefix_mdr_existence_evalhscm_positive))) /\ (((((exists ff_gap_mdm_lt_mdr_existence_evalhscm_positive_cell_column_before. ff_gap_mdm_lt_mdr_existence_evalhscm_positive_cell_column_before + S (ff_column_mdm_prefix_mdr_existence_evalhscm_positive) = (mdr_j_existence_evalhsc)) /\ ff_column_mdm_cell_mdr_existence_evalhscm_positive_cell = ff_column_mdm_prefix_mdr_existence_evalhscm_positive) \/ ((exists ff_gap_mdm_le_mdr_existence_evalhscm_positive_cell_column_after. ff_gap_mdm_le_mdr_existence_evalhscm_positive_cell_column_after + (mdr_j_existence_evalhsc) = (ff_column_mdm_prefix_mdr_existence_evalhscm_positive)) /\ ff_column_mdm_cell_mdr_existence_evalhscm_positive_cell = S ff_column_mdm_prefix_mdr_existence_evalhscm_positive))) /\ (((exists ff_h_mdm_mdr_existence_evalhscm_positive_cell_source. ff_h_mdm_mdr_existence_evalhscm_positive_cell_source + S (ff_value_mdm_prefix_mdr_existence_evalhscm_positive) = S ((S ((ff_row_mdm_cell_mdr_existence_evalhscm_positive_cell) * (S (mdr_q_existence_evalhs)) + (ff_column_mdm_cell_mdr_existence_evalhscm_positive_cell))) * mdr_pc_existence_evalh)) /\ exists ff_q_mdm_mdr_existence_evalhscm_positive_cell_source. mdr_pb_existence_evalh = ff_q_mdm_mdr_existence_evalhscm_positive_cell_source * S ((S ((ff_row_mdm_cell_mdr_existence_evalhscm_positive_cell) * (S (mdr_q_existence_evalhs)) + (ff_column_mdm_cell_mdr_existence_evalhscm_positive_cell))) * mdr_pc_existence_evalh) + (ff_value_mdm_prefix_mdr_existence_evalhscm_positive)))))) /\ (((exists ff_h_mdm_mdr_existence_evalhscm_positive_target. ff_h_mdm_mdr_existence_evalhscm_positive_target + S (ff_value_mdm_prefix_mdr_existence_evalhscm_positive) = S ((S (ff_index_mdm_prefix_mdr_existence_evalhscm_positive)) * mdr_us_existence_evalhsc)) /\ exists ff_q_mdm_mdr_existence_evalhscm_positive_target. mdr_up_existence_evalhsc = ff_q_mdm_mdr_existence_evalhscm_positive_target * S ((S (ff_index_mdm_prefix_mdr_existence_evalhscm_positive)) * mdr_us_existence_evalhsc) + (ff_value_mdm_prefix_mdr_existence_evalhscm_positive))))))) /\ (forall ff_index_mdm_prefix_mdr_existence_evalhscm_negative. (exists ff_gap_mdm_lt_mdr_existence_evalhscm_negative_index_bound. ff_gap_mdm_lt_mdr_existence_evalhscm_negative_index_bound + S (ff_index_mdm_prefix_mdr_existence_evalhscm_negative) = ((mdr_q_existence_evalhs) * (mdr_q_existence_evalhs))) -> exists ff_row_mdm_prefix_mdr_existence_evalhscm_negative ff_column_mdm_prefix_mdr_existence_evalhscm_negative ff_value_mdm_prefix_mdr_existence_evalhscm_negative. (ff_index_mdm_prefix_mdr_existence_evalhscm_negative = (mdr_q_existence_evalhs) * ff_row_mdm_prefix_mdr_existence_evalhscm_negative + ff_column_mdm_prefix_mdr_existence_evalhscm_negative /\ ((exists ff_gap_mdm_lt_mdr_existence_evalhscm_negative_column_bound. ff_gap_mdm_lt_mdr_existence_evalhscm_negative_column_bound + S (ff_column_mdm_prefix_mdr_existence_evalhscm_negative) = (mdr_q_existence_evalhs)) /\ ((exists ff_row_mdm_cell_mdr_existence_evalhscm_negative_cell ff_column_mdm_cell_mdr_existence_evalhscm_negative_cell. (((((exists ff_gap_mdm_lt_mdr_existence_evalhscm_negative_cell_row_before. ff_gap_mdm_lt_mdr_existence_evalhscm_negative_cell_row_before + S (ff_row_mdm_prefix_mdr_existence_evalhscm_negative) = (0)) /\ ff_row_mdm_cell_mdr_existence_evalhscm_negative_cell = ff_row_mdm_prefix_mdr_existence_evalhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_existence_evalhscm_negative_cell_row_after. ff_gap_mdm_le_mdr_existence_evalhscm_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mdr_existence_evalhscm_negative)) /\ ff_row_mdm_cell_mdr_existence_evalhscm_negative_cell = S ff_row_mdm_prefix_mdr_existence_evalhscm_negative))) /\ (((((exists ff_gap_mdm_lt_mdr_existence_evalhscm_negative_cell_column_before. ff_gap_mdm_lt_mdr_existence_evalhscm_negative_cell_column_before + S (ff_column_mdm_prefix_mdr_existence_evalhscm_negative) = (mdr_j_existence_evalhsc)) /\ ff_column_mdm_cell_mdr_existence_evalhscm_negative_cell = ff_column_mdm_prefix_mdr_existence_evalhscm_negative) \/ ((exists ff_gap_mdm_le_mdr_existence_evalhscm_negative_cell_column_after. ff_gap_mdm_le_mdr_existence_evalhscm_negative_cell_column_after + (mdr_j_existence_evalhsc) = (ff_column_mdm_prefix_mdr_existence_evalhscm_negative)) /\ ff_column_mdm_cell_mdr_existence_evalhscm_negative_cell = S ff_column_mdm_prefix_mdr_existence_evalhscm_negative))) /\ (((exists ff_h_mdm_mdr_existence_evalhscm_negative_cell_source. ff_h_mdm_mdr_existence_evalhscm_negative_cell_source + S (ff_value_mdm_prefix_mdr_existence_evalhscm_negative) = S ((S ((ff_row_mdm_cell_mdr_existence_evalhscm_negative_cell) * (S (mdr_q_existence_evalhs)) + (ff_column_mdm_cell_mdr_existence_evalhscm_negative_cell))) * mdr_nc_existence_evalh)) /\ exists ff_q_mdm_mdr_existence_evalhscm_negative_cell_source. mdr_nb_existence_evalh = ff_q_mdm_mdr_existence_evalhscm_negative_cell_source * S ((S ((ff_row_mdm_cell_mdr_existence_evalhscm_negative_cell) * (S (mdr_q_existence_evalhs)) + (ff_column_mdm_cell_mdr_existence_evalhscm_negative_cell))) * mdr_nc_existence_evalh) + (ff_value_mdm_prefix_mdr_existence_evalhscm_negative)))))) /\ (((exists ff_h_mdm_mdr_existence_evalhscm_negative_target. ff_h_mdm_mdr_existence_evalhscm_negative_target + S (ff_value_mdm_prefix_mdr_existence_evalhscm_negative) = S ((S (ff_index_mdm_prefix_mdr_existence_evalhscm_negative)) * mdr_ut_existence_evalhsc)) /\ exists ff_q_mdm_mdr_existence_evalhscm_negative_target. mdr_un_existence_evalhsc = ff_q_mdm_mdr_existence_evalhscm_negative_target * S ((S (ff_index_mdm_prefix_mdr_existence_evalhscm_negative)) * mdr_ut_existence_evalhsc) + (ff_value_mdm_prefix_mdr_existence_evalhscm_negative))))))))) /\ ((((exists ff_h_mdr_existence_evalhscp. ff_h_mdr_existence_evalhscp + S (mdr_p_existence_evalhsc) = S ((S (mdr_j_existence_evalhsc)) * mdr_ec_existence_evalhs)) /\ exists ff_q_mdr_existence_evalhscp. mdr_eb_existence_evalhs = ff_q_mdr_existence_evalhscp * S ((S (mdr_j_existence_evalhsc)) * mdr_ec_existence_evalhs) + (mdr_p_existence_evalhsc))) /\ (((exists ff_h_mdr_existence_evalhscn. ff_h_mdr_existence_evalhscn + S (mdr_n_existence_evalhsc) = S ((S (mdr_j_existence_evalhsc)) * mdr_fc_existence_evalhs)) /\ exists ff_q_mdr_existence_evalhscn. mdr_fb_existence_evalhs = ff_q_mdr_existence_evalhscn * S ((S (mdr_j_existence_evalhsc)) * mdr_fc_existence_evalhs) + (mdr_n_existence_evalhsc)))))))) /\ (exists ff_ub_mce_fold_mdr_existence_evalhsf ff_uc_mce_fold_mdr_existence_evalhsf ff_vb_mce_fold_mdr_existence_evalhsf ff_vc_mce_fold_mdr_existence_evalhsf. ((forall ff_index_mce_alternating_mdr_existence_evalhsf_prefix. (exists ff_gap_mce_mdr_existence_evalhsf_prefix_index. ff_gap_mce_mdr_existence_evalhsf_prefix_index + S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix) = (S (mdr_q_existence_evalhs))) -> exists ff_ap_mce_alternating_mdr_existence_evalhsf_prefix ff_an_mce_alternating_mdr_existence_evalhsf_prefix ff_bp_mce_alternating_mdr_existence_evalhsf_prefix ff_bn_mce_alternating_mdr_existence_evalhsf_prefix ff_p_mce_alternating_mdr_existence_evalhsf_prefix ff_n_mce_alternating_mdr_existence_evalhsf_prefix. ((((exists ff_h_mce_mdr_existence_evalhsf_prefix_ap. ff_h_mce_mdr_existence_evalhsf_prefix_ap + S (ff_ap_mce_alternating_mdr_existence_evalhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_pc_existence_evalh)) /\ exists ff_q_mce_mdr_existence_evalhsf_prefix_ap. mdr_pb_existence_evalh = ff_q_mce_mdr_existence_evalhsf_prefix_ap * S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_pc_existence_evalh) + (ff_ap_mce_alternating_mdr_existence_evalhsf_prefix))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_prefix_an. ff_h_mce_mdr_existence_evalhsf_prefix_an + S (ff_an_mce_alternating_mdr_existence_evalhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_nc_existence_evalh)) /\ exists ff_q_mce_mdr_existence_evalhsf_prefix_an. mdr_nb_existence_evalh = ff_q_mce_mdr_existence_evalhsf_prefix_an * S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_nc_existence_evalh) + (ff_an_mce_alternating_mdr_existence_evalhsf_prefix))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_prefix_bp. ff_h_mce_mdr_existence_evalhsf_prefix_bp + S (ff_bp_mce_alternating_mdr_existence_evalhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_ec_existence_evalhs)) /\ exists ff_q_mce_mdr_existence_evalhsf_prefix_bp. mdr_eb_existence_evalhs = ff_q_mce_mdr_existence_evalhsf_prefix_bp * S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_ec_existence_evalhs) + (ff_bp_mce_alternating_mdr_existence_evalhsf_prefix))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_prefix_bn. ff_h_mce_mdr_existence_evalhsf_prefix_bn + S (ff_bn_mce_alternating_mdr_existence_evalhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_fc_existence_evalhs)) /\ exists ff_q_mce_mdr_existence_evalhsf_prefix_bn. mdr_fb_existence_evalhs = ff_q_mce_mdr_existence_evalhsf_prefix_bn * S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * mdr_fc_existence_evalhs) + (ff_bn_mce_alternating_mdr_existence_evalhsf_prefix))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_prefix_positive. ff_h_mce_mdr_existence_evalhsf_prefix_positive + S (ff_p_mce_alternating_mdr_existence_evalhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * ff_uc_mce_fold_mdr_existence_evalhsf)) /\ exists ff_q_mce_mdr_existence_evalhsf_prefix_positive. ff_ub_mce_fold_mdr_existence_evalhsf = ff_q_mce_mdr_existence_evalhsf_prefix_positive * S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * ff_uc_mce_fold_mdr_existence_evalhsf) + (ff_p_mce_alternating_mdr_existence_evalhsf_prefix))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_prefix_negative. ff_h_mce_mdr_existence_evalhsf_prefix_negative + S (ff_n_mce_alternating_mdr_existence_evalhsf_prefix) = S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * ff_vc_mce_fold_mdr_existence_evalhsf)) /\ exists ff_q_mce_mdr_existence_evalhsf_prefix_negative. ff_vb_mce_fold_mdr_existence_evalhsf = ff_q_mce_mdr_existence_evalhsf_prefix_negative * S ((S (ff_index_mce_alternating_mdr_existence_evalhsf_prefix)) * ff_vc_mce_fold_mdr_existence_evalhsf) + (ff_n_mce_alternating_mdr_existence_evalhsf_prefix))) /\ (((exists ff_even_mce_term_mdr_existence_evalhsf_prefix_term. ff_index_mce_alternating_mdr_existence_evalhsf_prefix = 2 * ff_even_mce_term_mdr_existence_evalhsf_prefix_term) /\ (ff_p_mce_alternating_mdr_existence_evalhsf_prefix = (ff_ap_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bp_mce_alternating_mdr_existence_evalhsf_prefix) + (ff_an_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bn_mce_alternating_mdr_existence_evalhsf_prefix) /\ ff_n_mce_alternating_mdr_existence_evalhsf_prefix = (ff_ap_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bn_mce_alternating_mdr_existence_evalhsf_prefix) + (ff_an_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bp_mce_alternating_mdr_existence_evalhsf_prefix))) \/ ((exists ff_odd_mce_term_mdr_existence_evalhsf_prefix_term. ff_index_mce_alternating_mdr_existence_evalhsf_prefix = 2 * ff_odd_mce_term_mdr_existence_evalhsf_prefix_term + 1) /\ (ff_p_mce_alternating_mdr_existence_evalhsf_prefix = (ff_ap_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bn_mce_alternating_mdr_existence_evalhsf_prefix) + (ff_an_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bp_mce_alternating_mdr_existence_evalhsf_prefix) /\ ff_n_mce_alternating_mdr_existence_evalhsf_prefix = (ff_ap_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bp_mce_alternating_mdr_existence_evalhsf_prefix) + (ff_an_mce_alternating_mdr_existence_evalhsf_prefix) * (ff_bn_mce_alternating_mdr_existence_evalhsf_prefix))))))))))) /\ ((exists ff_u_mce_mdr_existence_evalhsf_positive ff_v_mce_mdr_existence_evalhsf_positive. ((((exists ff_h_mce_mdr_existence_evalhsf_positive_start. ff_h_mce_mdr_existence_evalhsf_positive_start + S (0) = S ((S (0)) * ff_v_mce_mdr_existence_evalhsf_positive)) /\ exists ff_q_mce_mdr_existence_evalhsf_positive_start. ff_u_mce_mdr_existence_evalhsf_positive = ff_q_mce_mdr_existence_evalhsf_positive_start * S ((S (0)) * ff_v_mce_mdr_existence_evalhsf_positive) + (0))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_positive_terminal. ff_h_mce_mdr_existence_evalhsf_positive_terminal + S (mdr_p_existence_evalh) = S ((S ((S (mdr_q_existence_evalhs)))) * ff_v_mce_mdr_existence_evalhsf_positive)) /\ exists ff_q_mce_mdr_existence_evalhsf_positive_terminal. ff_u_mce_mdr_existence_evalhsf_positive = ff_q_mce_mdr_existence_evalhsf_positive_terminal * S ((S ((S (mdr_q_existence_evalhs)))) * ff_v_mce_mdr_existence_evalhsf_positive) + (mdr_p_existence_evalh))) /\ forall ff_i_mce_mdr_existence_evalhsf_positive. (exists ff_lt_mce_mdr_existence_evalhsf_positive_bound. ff_lt_mce_mdr_existence_evalhsf_positive_bound + S ff_i_mce_mdr_existence_evalhsf_positive = (S (mdr_q_existence_evalhs))) -> exists ff_a_mce_mdr_existence_evalhsf_positive ff_r_mce_mdr_existence_evalhsf_positive ff_s_mce_mdr_existence_evalhsf_positive. ((((exists ff_h_mce_mdr_existence_evalhsf_positive_summand. ff_h_mce_mdr_existence_evalhsf_positive_summand + S (ff_a_mce_mdr_existence_evalhsf_positive) = S ((S (ff_i_mce_mdr_existence_evalhsf_positive)) * ff_uc_mce_fold_mdr_existence_evalhsf)) /\ exists ff_q_mce_mdr_existence_evalhsf_positive_summand. ff_ub_mce_fold_mdr_existence_evalhsf = ff_q_mce_mdr_existence_evalhsf_positive_summand * S ((S (ff_i_mce_mdr_existence_evalhsf_positive)) * ff_uc_mce_fold_mdr_existence_evalhsf) + (ff_a_mce_mdr_existence_evalhsf_positive))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_positive_partial. ff_h_mce_mdr_existence_evalhsf_positive_partial + S (ff_r_mce_mdr_existence_evalhsf_positive) = S ((S (ff_i_mce_mdr_existence_evalhsf_positive)) * ff_v_mce_mdr_existence_evalhsf_positive)) /\ exists ff_q_mce_mdr_existence_evalhsf_positive_partial. ff_u_mce_mdr_existence_evalhsf_positive = ff_q_mce_mdr_existence_evalhsf_positive_partial * S ((S (ff_i_mce_mdr_existence_evalhsf_positive)) * ff_v_mce_mdr_existence_evalhsf_positive) + (ff_r_mce_mdr_existence_evalhsf_positive))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_positive_successor. ff_h_mce_mdr_existence_evalhsf_positive_successor + S (ff_s_mce_mdr_existence_evalhsf_positive) = S ((S (S ff_i_mce_mdr_existence_evalhsf_positive)) * ff_v_mce_mdr_existence_evalhsf_positive)) /\ exists ff_q_mce_mdr_existence_evalhsf_positive_successor. ff_u_mce_mdr_existence_evalhsf_positive = ff_q_mce_mdr_existence_evalhsf_positive_successor * S ((S (S ff_i_mce_mdr_existence_evalhsf_positive)) * ff_v_mce_mdr_existence_evalhsf_positive) + (ff_s_mce_mdr_existence_evalhsf_positive))) /\ ff_s_mce_mdr_existence_evalhsf_positive = ff_r_mce_mdr_existence_evalhsf_positive + ff_a_mce_mdr_existence_evalhsf_positive)))))) /\ (exists ff_u_mce_mdr_existence_evalhsf_negative ff_v_mce_mdr_existence_evalhsf_negative. ((((exists ff_h_mce_mdr_existence_evalhsf_negative_start. ff_h_mce_mdr_existence_evalhsf_negative_start + S (0) = S ((S (0)) * ff_v_mce_mdr_existence_evalhsf_negative)) /\ exists ff_q_mce_mdr_existence_evalhsf_negative_start. ff_u_mce_mdr_existence_evalhsf_negative = ff_q_mce_mdr_existence_evalhsf_negative_start * S ((S (0)) * ff_v_mce_mdr_existence_evalhsf_negative) + (0))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_negative_terminal. ff_h_mce_mdr_existence_evalhsf_negative_terminal + S (mdr_n_existence_evalh) = S ((S ((S (mdr_q_existence_evalhs)))) * ff_v_mce_mdr_existence_evalhsf_negative)) /\ exists ff_q_mce_mdr_existence_evalhsf_negative_terminal. ff_u_mce_mdr_existence_evalhsf_negative = ff_q_mce_mdr_existence_evalhsf_negative_terminal * S ((S ((S (mdr_q_existence_evalhs)))) * ff_v_mce_mdr_existence_evalhsf_negative) + (mdr_n_existence_evalh))) /\ forall ff_i_mce_mdr_existence_evalhsf_negative. (exists ff_lt_mce_mdr_existence_evalhsf_negative_bound. ff_lt_mce_mdr_existence_evalhsf_negative_bound + S ff_i_mce_mdr_existence_evalhsf_negative = (S (mdr_q_existence_evalhs))) -> exists ff_a_mce_mdr_existence_evalhsf_negative ff_r_mce_mdr_existence_evalhsf_negative ff_s_mce_mdr_existence_evalhsf_negative. ((((exists ff_h_mce_mdr_existence_evalhsf_negative_summand. ff_h_mce_mdr_existence_evalhsf_negative_summand + S (ff_a_mce_mdr_existence_evalhsf_negative) = S ((S (ff_i_mce_mdr_existence_evalhsf_negative)) * ff_vc_mce_fold_mdr_existence_evalhsf)) /\ exists ff_q_mce_mdr_existence_evalhsf_negative_summand. ff_vb_mce_fold_mdr_existence_evalhsf = ff_q_mce_mdr_existence_evalhsf_negative_summand * S ((S (ff_i_mce_mdr_existence_evalhsf_negative)) * ff_vc_mce_fold_mdr_existence_evalhsf) + (ff_a_mce_mdr_existence_evalhsf_negative))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_negative_partial. ff_h_mce_mdr_existence_evalhsf_negative_partial + S (ff_r_mce_mdr_existence_evalhsf_negative) = S ((S (ff_i_mce_mdr_existence_evalhsf_negative)) * ff_v_mce_mdr_existence_evalhsf_negative)) /\ exists ff_q_mce_mdr_existence_evalhsf_negative_partial. ff_u_mce_mdr_existence_evalhsf_negative = ff_q_mce_mdr_existence_evalhsf_negative_partial * S ((S (ff_i_mce_mdr_existence_evalhsf_negative)) * ff_v_mce_mdr_existence_evalhsf_negative) + (ff_r_mce_mdr_existence_evalhsf_negative))) /\ ((((exists ff_h_mce_mdr_existence_evalhsf_negative_successor. ff_h_mce_mdr_existence_evalhsf_negative_successor + S (ff_s_mce_mdr_existence_evalhsf_negative) = S ((S (S ff_i_mce_mdr_existence_evalhsf_negative)) * ff_v_mce_mdr_existence_evalhsf_negative)) /\ exists ff_q_mce_mdr_existence_evalhsf_negative_successor. ff_u_mce_mdr_existence_evalhsf_negative = ff_q_mce_mdr_existence_evalhsf_negative_successor * S ((S (S ff_i_mce_mdr_existence_evalhsf_negative)) * ff_v_mce_mdr_existence_evalhsf_negative) + (ff_s_mce_mdr_existence_evalhsf_negative))) /\ ff_s_mce_mdr_existence_evalhsf_negative = ff_r_mce_mdr_existence_evalhsf_negative + ff_a_mce_mdr_existence_evalhsf_negative))))))))))))))) /\ (exists mdr_z_existence_evalr. ((exists mdr_a_existence_evalrc mdr_b_existence_evalrc mdr_c_existence_evalrc mdr_e_existence_evalrc mdr_f_existence_evalrc. ((mdr_a_existence_evalrc = ((d) + (pb)) * S ((d) + (pb)) + ((pb) + (pb))) /\ ((mdr_b_existence_evalrc = ((pc) + (nb)) * S ((pc) + (nb)) + ((nb) + (nb))) /\ ((mdr_c_existence_evalrc = ((mdr_a_existence_evalrc) + (mdr_b_existence_evalrc)) * S ((mdr_a_existence_evalrc) + (mdr_b_existence_evalrc)) + ((mdr_b_existence_evalrc) + (mdr_b_existence_evalrc))) /\ ((mdr_e_existence_evalrc = ((p) + (n)) * S ((p) + (n)) + ((n) + (n))) /\ ((mdr_f_existence_evalrc = ((nc) + (mdr_e_existence_evalrc)) * S ((nc) + (mdr_e_existence_evalrc)) + ((mdr_e_existence_evalrc) + (mdr_e_existence_evalrc))) /\ ((mdr_z_existence_evalr) = ((mdr_c_existence_evalrc) + (mdr_f_existence_evalrc)) * S ((mdr_c_existence_evalrc) + (mdr_f_existence_evalrc)) + ((mdr_f_existence_evalrc) + (mdr_f_existence_evalrc))))))))) /\ (((exists ff_h_mdr_existence_evalrb. ff_h_mdr_existence_evalrb + S (mdr_z_existence_evalr) = S ((S (t)) * v)) /\ exists ff_q_mdr_existence_evalrb. u = ff_q_mdr_existence_evalrb * S ((S (t)) * v) + (mdr_z_existence_evalr)))))))))
  7. 0007specialize matrix_recursive_all_extensions (d)
  8. 0008specialize matrix_recursive_all_extensions (pb)
  9. 0009specialize matrix_recursive_all_extensions (pc)
  10. 0010specialize matrix_recursive_all_extensions (nb)
  11. 0011specialize matrix_recursive_all_extensions (nc)
  12. 0012specialize matrix_recursive_all_extensions (0)
  13. 0013specialize matrix_recursive_all_extensions (0)
  14. 0014specialize matrix_recursive_all_extensions (0)
  15. 0015apply matrix_recursive_all_extensions
  16. 0016specialize matrix_recursive_empty_history (0)
  17. 0017specialize matrix_recursive_empty_history (0)
  18. 0018apply matrix_recursive_empty_history
  19. 0019cases hevaluation
  20. 0020cases hevaluation_witness
  21. 0021cases hevaluation_witness_witness
  22. 0022cases hevaluation_witness_witness_witness
  23. 0023cases hevaluation_witness_witness_witness_witness
  24. 0024cases hevaluation_witness_witness_witness_witness_witness
  25. 0025cases hevaluation_witness_witness_witness_witness_witness_right
  26. 0026cases hevaluation_witness_witness_witness_witness_witness_right_right
  27. 0027exists x3
  28. 0028exists x4
  29. 0029exists x
  30. 0030exists x1
  31. 0031exists S x2
  32. 0032exists x2
  33. 0033split
  34. 0034exact hevaluation_witness_witness_witness_witness_witness_right_right_left
  35. 0035split
  36. 0036apply le_refl
  37. 0037exact hevaluation_witness_witness_witness_witness_witness_right_right_right