CE001D

signed_matrix_cofactor_family_and_fold_exists

Every arbitrary signed square matrix simultaneously has ALL genuine first-row signed minors and the exact alternating fold of its ACTUAL first row against separately supplied signed cofactor values.

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

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.

Historical partial components only: this chapter proves genuine signed first-row minors and unique alternating folds, with supplied cofactor values. T13 is now closed in the separate Alpha-v27 integer-linear-algebra branch with actual arbitrary determinant data, rank, and integer column spans; lattice index and normal forms are not claimed. Full T13 proof · Alpha v27

Exact theorem in conservative defined notation

∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ q. ∀ eb. ∀ ec. ∀ fb. ∀ fc. ∃ u. ∃ v. ∃ p. ∃ n. SignedCofactorMinorPrefix(pb,pc,nb,nc,q,u,v,S q) ∧ SignedFirstRowCofactorFold(pb,pc,nb,nc,q,eb,ec,fb,fc,p,n)

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

Definition DAG

SignedCofactorMinorPrefix(pb,pc,nb,nc,q,b,c,l) · 1SignedFirstRowCofactorFold(pb,pc,nb,nc,q,eb,ec,fb,fc,p,n) · 1

Actual proof prerequisites

signed_cofactor_minor_family_existssigned_first_row_cofactor_fold_exists
Original expanded first-order statement 
forall pb pc nb nc q eb ec fb fc. exists u v p n. ((forall ff_index_mce_family_full. (exists ff_gap_mce_full_index. ff_gap_mce_full_index + S (ff_index_mce_family_full) = (S q)) -> exists ff_value_mce_family_full. ((((exists ff_h_mce_full_entry. ff_h_mce_full_entry + S (ff_value_mce_family_full) = S ((S (ff_index_mce_family_full)) * v)) /\ exists ff_q_mce_full_entry. u = ff_q_mce_full_entry * S ((S (ff_index_mce_family_full)) * v) + (ff_value_mce_family_full))) /\ (exists ff_up_mce_record_full_record ff_us_mce_record_full_record ff_un_mce_record_full_record ff_ut_mce_record_full_record. ((ff_value_mce_family_full = ((((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) * S ((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) + ((ff_us_mce_record_full_record) + (ff_us_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record)))) * S ((((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) * S ((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) + ((ff_us_mce_record_full_record) + (ff_us_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record)))) + ((((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record))))) /\ (((forall ff_index_mdm_prefix_mce_full_record_minor_positive. (exists ff_gap_mdm_lt_mce_full_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_full_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_full_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_full_record_minor_positive ff_column_mdm_prefix_mce_full_record_minor_positive ff_value_mdm_prefix_mce_full_record_minor_positive. (ff_index_mdm_prefix_mce_full_record_minor_positive = (q) * ff_row_mdm_prefix_mce_full_record_minor_positive + ff_column_mdm_prefix_mce_full_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_full_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_full_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_full_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_full_record_minor_positive_cell ff_column_mdm_cell_mce_full_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_full_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_full_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_full_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_full_record_minor_positive_cell = ff_row_mdm_prefix_mce_full_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_full_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_full_record_minor_positive)) /\ ff_row_mdm_cell_mce_full_record_minor_positive_cell = S ff_row_mdm_prefix_mce_full_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_full_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_full_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_full_record_minor_positive) = (ff_index_mce_family_full)) /\ ff_column_mdm_cell_mce_full_record_minor_positive_cell = ff_column_mdm_prefix_mce_full_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_full_record_minor_positive_cell_column_after + (ff_index_mce_family_full) = (ff_column_mdm_prefix_mce_full_record_minor_positive)) /\ ff_column_mdm_cell_mce_full_record_minor_positive_cell = S ff_column_mdm_prefix_mce_full_record_minor_positive))) /\ (((exists ff_h_mdm_mce_full_record_minor_positive_cell_source. ff_h_mdm_mce_full_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_full_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_full_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_full_record_minor_positive_cell_source. pb = ff_q_mdm_mce_full_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_full_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_full_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_full_record_minor_positive_target. ff_h_mdm_mce_full_record_minor_positive_target + S (ff_value_mdm_prefix_mce_full_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_full_record_minor_positive)) * ff_us_mce_record_full_record)) /\ exists ff_q_mdm_mce_full_record_minor_positive_target. ff_up_mce_record_full_record = ff_q_mdm_mce_full_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_full_record_minor_positive)) * ff_us_mce_record_full_record) + (ff_value_mdm_prefix_mce_full_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_full_record_minor_negative. (exists ff_gap_mdm_lt_mce_full_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_full_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_full_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_full_record_minor_negative ff_column_mdm_prefix_mce_full_record_minor_negative ff_value_mdm_prefix_mce_full_record_minor_negative. (ff_index_mdm_prefix_mce_full_record_minor_negative = (q) * ff_row_mdm_prefix_mce_full_record_minor_negative + ff_column_mdm_prefix_mce_full_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_full_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_full_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_full_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_full_record_minor_negative_cell ff_column_mdm_cell_mce_full_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_full_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_full_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_full_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_full_record_minor_negative_cell = ff_row_mdm_prefix_mce_full_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_full_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_full_record_minor_negative)) /\ ff_row_mdm_cell_mce_full_record_minor_negative_cell = S ff_row_mdm_prefix_mce_full_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_full_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_full_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_full_record_minor_negative) = (ff_index_mce_family_full)) /\ ff_column_mdm_cell_mce_full_record_minor_negative_cell = ff_column_mdm_prefix_mce_full_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_full_record_minor_negative_cell_column_after + (ff_index_mce_family_full) = (ff_column_mdm_prefix_mce_full_record_minor_negative)) /\ ff_column_mdm_cell_mce_full_record_minor_negative_cell = S ff_column_mdm_prefix_mce_full_record_minor_negative))) /\ (((exists ff_h_mdm_mce_full_record_minor_negative_cell_source. ff_h_mdm_mce_full_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_full_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_full_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_full_record_minor_negative_cell_source. nb = ff_q_mdm_mce_full_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_full_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_full_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_full_record_minor_negative_target. ff_h_mdm_mce_full_record_minor_negative_target + S (ff_value_mdm_prefix_mce_full_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_full_record_minor_negative)) * ff_ut_mce_record_full_record)) /\ exists ff_q_mdm_mce_full_record_minor_negative_target. ff_un_mce_record_full_record = ff_q_mdm_mce_full_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_full_record_minor_negative)) * ff_ut_mce_record_full_record) + (ff_value_mdm_prefix_mce_full_record_minor_negative))))))))))))) /\ (exists ff_ab_mce_row_result ff_ac_mce_row_result ff_db_mce_row_result ff_dc_mce_row_result. ((forall ff_index_mcp_mce_result_positive ff_source_mcp_mce_result_positive ff_target_mcp_mce_result_positive. (exists mcp_gap_mce_result_positive_bound. mcp_gap_mce_result_positive_bound + S (ff_index_mcp_mce_result_positive) = (S (q))) -> (((exists fs_h_mcp_mce_result_positive_source. fs_h_mcp_mce_result_positive_source + S (ff_source_mcp_mce_result_positive) = S ((S ((0) + (1) * ff_index_mcp_mce_result_positive)) * pc)) /\ exists fs_q_mcp_mce_result_positive_source. pb = fs_q_mcp_mce_result_positive_source * S ((S ((0) + (1) * ff_index_mcp_mce_result_positive)) * pc) + (ff_source_mcp_mce_result_positive))) -> (((exists fs_h_mcp_mce_result_positive_target. fs_h_mcp_mce_result_positive_target + S (ff_target_mcp_mce_result_positive) = S ((S (ff_index_mcp_mce_result_positive)) * ff_ac_mce_row_result)) /\ exists fs_q_mcp_mce_result_positive_target. ff_ab_mce_row_result = fs_q_mcp_mce_result_positive_target * S ((S (ff_index_mcp_mce_result_positive)) * ff_ac_mce_row_result) + (ff_target_mcp_mce_result_positive))) -> ff_target_mcp_mce_result_positive = ff_source_mcp_mce_result_positive) /\ ((forall ff_index_mcp_mce_result_negative ff_source_mcp_mce_result_negative ff_target_mcp_mce_result_negative. (exists mcp_gap_mce_result_negative_bound. mcp_gap_mce_result_negative_bound + S (ff_index_mcp_mce_result_negative) = (S (q))) -> (((exists fs_h_mcp_mce_result_negative_source. fs_h_mcp_mce_result_negative_source + S (ff_source_mcp_mce_result_negative) = S ((S ((0) + (1) * ff_index_mcp_mce_result_negative)) * nc)) /\ exists fs_q_mcp_mce_result_negative_source. nb = fs_q_mcp_mce_result_negative_source * S ((S ((0) + (1) * ff_index_mcp_mce_result_negative)) * nc) + (ff_source_mcp_mce_result_negative))) -> (((exists fs_h_mcp_mce_result_negative_target. fs_h_mcp_mce_result_negative_target + S (ff_target_mcp_mce_result_negative) = S ((S (ff_index_mcp_mce_result_negative)) * ff_dc_mce_row_result)) /\ exists fs_q_mcp_mce_result_negative_target. ff_db_mce_row_result = fs_q_mcp_mce_result_negative_target * S ((S (ff_index_mcp_mce_result_negative)) * ff_dc_mce_row_result) + (ff_target_mcp_mce_result_negative))) -> ff_target_mcp_mce_result_negative = ff_source_mcp_mce_result_negative) /\ (exists ff_ub_mce_fold_result_fold ff_uc_mce_fold_result_fold ff_vb_mce_fold_result_fold ff_vc_mce_fold_result_fold. ((forall ff_index_mce_alternating_result_fold_prefix. (exists ff_gap_mce_result_fold_prefix_index. ff_gap_mce_result_fold_prefix_index + S (ff_index_mce_alternating_result_fold_prefix) = (S (q))) -> exists ff_ap_mce_alternating_result_fold_prefix ff_an_mce_alternating_result_fold_prefix ff_bp_mce_alternating_result_fold_prefix ff_bn_mce_alternating_result_fold_prefix ff_p_mce_alternating_result_fold_prefix ff_n_mce_alternating_result_fold_prefix. ((((exists ff_h_mce_result_fold_prefix_ap. ff_h_mce_result_fold_prefix_ap + S (ff_ap_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_ac_mce_row_result)) /\ exists ff_q_mce_result_fold_prefix_ap. ff_ab_mce_row_result = ff_q_mce_result_fold_prefix_ap * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_ac_mce_row_result) + (ff_ap_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_an. ff_h_mce_result_fold_prefix_an + S (ff_an_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_dc_mce_row_result)) /\ exists ff_q_mce_result_fold_prefix_an. ff_db_mce_row_result = ff_q_mce_result_fold_prefix_an * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_dc_mce_row_result) + (ff_an_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_bp. ff_h_mce_result_fold_prefix_bp + S (ff_bp_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ec)) /\ exists ff_q_mce_result_fold_prefix_bp. eb = ff_q_mce_result_fold_prefix_bp * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ec) + (ff_bp_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_bn. ff_h_mce_result_fold_prefix_bn + S (ff_bn_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * fc)) /\ exists ff_q_mce_result_fold_prefix_bn. fb = ff_q_mce_result_fold_prefix_bn * S ((S (ff_index_mce_alternating_result_fold_prefix)) * fc) + (ff_bn_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_positive. ff_h_mce_result_fold_prefix_positive + S (ff_p_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_uc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_prefix_positive. ff_ub_mce_fold_result_fold = ff_q_mce_result_fold_prefix_positive * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_uc_mce_fold_result_fold) + (ff_p_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_negative. ff_h_mce_result_fold_prefix_negative + S (ff_n_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_vc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_prefix_negative. ff_vb_mce_fold_result_fold = ff_q_mce_result_fold_prefix_negative * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_vc_mce_fold_result_fold) + (ff_n_mce_alternating_result_fold_prefix))) /\ (((exists ff_even_mce_term_result_fold_prefix_term. ff_index_mce_alternating_result_fold_prefix = 2 * ff_even_mce_term_result_fold_prefix_term) /\ (ff_p_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) /\ ff_n_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix))) \/ ((exists ff_odd_mce_term_result_fold_prefix_term. ff_index_mce_alternating_result_fold_prefix = 2 * ff_odd_mce_term_result_fold_prefix_term + 1) /\ (ff_p_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) /\ ff_n_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix))))))))))) /\ ((exists ff_u_mce_result_fold_positive ff_v_mce_result_fold_positive. ((((exists ff_h_mce_result_fold_positive_start. ff_h_mce_result_fold_positive_start + S (0) = S ((S (0)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_start. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_start * S ((S (0)) * ff_v_mce_result_fold_positive) + (0))) /\ ((((exists ff_h_mce_result_fold_positive_terminal. ff_h_mce_result_fold_positive_terminal + S (p) = S ((S ((S (q)))) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_terminal. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_terminal * S ((S ((S (q)))) * ff_v_mce_result_fold_positive) + (p))) /\ forall ff_i_mce_result_fold_positive. (exists ff_lt_mce_result_fold_positive_bound. ff_lt_mce_result_fold_positive_bound + S ff_i_mce_result_fold_positive = (S (q))) -> exists ff_a_mce_result_fold_positive ff_r_mce_result_fold_positive ff_s_mce_result_fold_positive. ((((exists ff_h_mce_result_fold_positive_summand. ff_h_mce_result_fold_positive_summand + S (ff_a_mce_result_fold_positive) = S ((S (ff_i_mce_result_fold_positive)) * ff_uc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_positive_summand. ff_ub_mce_fold_result_fold = ff_q_mce_result_fold_positive_summand * S ((S (ff_i_mce_result_fold_positive)) * ff_uc_mce_fold_result_fold) + (ff_a_mce_result_fold_positive))) /\ ((((exists ff_h_mce_result_fold_positive_partial. ff_h_mce_result_fold_positive_partial + S (ff_r_mce_result_fold_positive) = S ((S (ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_partial. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_partial * S ((S (ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive) + (ff_r_mce_result_fold_positive))) /\ ((((exists ff_h_mce_result_fold_positive_successor. ff_h_mce_result_fold_positive_successor + S (ff_s_mce_result_fold_positive) = S ((S (S ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_successor. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_successor * S ((S (S ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive) + (ff_s_mce_result_fold_positive))) /\ ff_s_mce_result_fold_positive = ff_r_mce_result_fold_positive + ff_a_mce_result_fold_positive)))))) /\ (exists ff_u_mce_result_fold_negative ff_v_mce_result_fold_negative. ((((exists ff_h_mce_result_fold_negative_start. ff_h_mce_result_fold_negative_start + S (0) = S ((S (0)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_start. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_start * S ((S (0)) * ff_v_mce_result_fold_negative) + (0))) /\ ((((exists ff_h_mce_result_fold_negative_terminal. ff_h_mce_result_fold_negative_terminal + S (n) = S ((S ((S (q)))) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_terminal. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_terminal * S ((S ((S (q)))) * ff_v_mce_result_fold_negative) + (n))) /\ forall ff_i_mce_result_fold_negative. (exists ff_lt_mce_result_fold_negative_bound. ff_lt_mce_result_fold_negative_bound + S ff_i_mce_result_fold_negative = (S (q))) -> exists ff_a_mce_result_fold_negative ff_r_mce_result_fold_negative ff_s_mce_result_fold_negative. ((((exists ff_h_mce_result_fold_negative_summand. ff_h_mce_result_fold_negative_summand + S (ff_a_mce_result_fold_negative) = S ((S (ff_i_mce_result_fold_negative)) * ff_vc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_negative_summand. ff_vb_mce_fold_result_fold = ff_q_mce_result_fold_negative_summand * S ((S (ff_i_mce_result_fold_negative)) * ff_vc_mce_fold_result_fold) + (ff_a_mce_result_fold_negative))) /\ ((((exists ff_h_mce_result_fold_negative_partial. ff_h_mce_result_fold_negative_partial + S (ff_r_mce_result_fold_negative) = S ((S (ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_partial. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_partial * S ((S (ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative) + (ff_r_mce_result_fold_negative))) /\ ((((exists ff_h_mce_result_fold_negative_successor. ff_h_mce_result_fold_negative_successor + S (ff_s_mce_result_fold_negative) = S ((S (S ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_successor. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_successor * S ((S (S ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative) + (ff_s_mce_result_fold_negative))) /\ ff_s_mce_result_fold_negative = ff_r_mce_result_fold_negative + ff_a_mce_result_fold_negative)))))))))))))

Complete unchanged native tactic proof

All 38 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

38 script commands · 9 reading checkpoints · 2 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 (2)
signed cofactor minor family existssigned first row cofactor fold exists

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–9

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 q
  6. L6
    intro eb
  7. L7
    intro ec
  8. L8
    intro fb
  9. L9
    intro fc
02Establish hfamilyL10–16

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

  1. L10
    have hfamily : ∃ u. ∃ v. SignedCofactorMinorPrefix(pb,pc,nb,nc,q,u,v,S q)Definitions: SignedCofactorMinorPrefixOriginal native command in the exact edition
  2. L11
    specialize signed_cofactor_minor_family_exists pb
  3. L12
    specialize signed_cofactor_minor_family_exists pc
  4. L13
    specialize signed_cofactor_minor_family_exists nb
  5. L14
    specialize signed_cofactor_minor_family_exists nc
  6. L15
    specialize signed_cofactor_minor_family_exists q
  7. L16
    exact signed_cofactor_minor_family_exists
03Separate the logical casesL17–18

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

  1. L17
    cases hfamily
  2. L18
    cases hfamily_witness
04Establish hfoldL19–28

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

  1. L19
    have hfold : ∃ p. ∃ n. SignedFirstRowCofactorFold(pb,pc,nb,nc,q,eb,ec,fb,fc,p,n)Definitions: SignedFirstRowCofactorFoldOriginal native command in the exact edition
  2. L20
    specialize signed_first_row_cofactor_fold_exists pb
  3. L21
    specialize signed_first_row_cofactor_fold_exists pc
  4. L22
    specialize signed_first_row_cofactor_fold_exists nb
  5. L23
    specialize signed_first_row_cofactor_fold_exists nc
  6. L24
    specialize signed_first_row_cofactor_fold_exists q
  7. L25
    specialize signed_first_row_cofactor_fold_exists eb
  8. L26
    specialize signed_first_row_cofactor_fold_exists ec
  9. L27
    specialize signed_first_row_cofactor_fold_exists fb
  10. L28
    specialize signed_first_row_cofactor_fold_exists fc
05Use earlier factsL29–29

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

  1. L29
    exact signed_first_row_cofactor_fold_exists
06Separate the logical casesL30–31

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

  1. L30
    cases hfold
  2. L31
    cases hfold_witness
07Construct an explicit witnessL32–35

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

  1. L32
    exists x
  2. L33
    exists x1
  3. L34
    exists x2
  4. L35
    exists x3
08Separate the logical casesL36–36

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

  1. L36
    split
09Use earlier factsL37–38

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

  1. L37
    exact hfamily_witness_witness
  2. L38
    exact hfold_witness_witness

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro q
  6. 0006intro eb
  7. 0007intro ec
  8. 0008intro fb
  9. 0009intro fc
  10. 0010have hfamily : exists u v. (forall ff_index_mce_family_full. (exists ff_gap_mce_full_index. ff_gap_mce_full_index + S (ff_index_mce_family_full) = (S q)) -> exists ff_value_mce_family_full. ((((exists ff_h_mce_full_entry. ff_h_mce_full_entry + S (ff_value_mce_family_full) = S ((S (ff_index_mce_family_full)) * v)) /\ exists ff_q_mce_full_entry. u = ff_q_mce_full_entry * S ((S (ff_index_mce_family_full)) * v) + (ff_value_mce_family_full))) /\ (exists ff_up_mce_record_full_record ff_us_mce_record_full_record ff_un_mce_record_full_record ff_ut_mce_record_full_record. ((ff_value_mce_family_full = ((((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) * S ((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) + ((ff_us_mce_record_full_record) + (ff_us_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record)))) * S ((((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) * S ((ff_up_mce_record_full_record) + (ff_us_mce_record_full_record)) + ((ff_us_mce_record_full_record) + (ff_us_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record)))) + ((((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record))) + (((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) * S ((ff_un_mce_record_full_record) + (ff_ut_mce_record_full_record)) + ((ff_ut_mce_record_full_record) + (ff_ut_mce_record_full_record))))) /\ (((forall ff_index_mdm_prefix_mce_full_record_minor_positive. (exists ff_gap_mdm_lt_mce_full_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_full_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_full_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_full_record_minor_positive ff_column_mdm_prefix_mce_full_record_minor_positive ff_value_mdm_prefix_mce_full_record_minor_positive. (ff_index_mdm_prefix_mce_full_record_minor_positive = (q) * ff_row_mdm_prefix_mce_full_record_minor_positive + ff_column_mdm_prefix_mce_full_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_full_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_full_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_full_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_full_record_minor_positive_cell ff_column_mdm_cell_mce_full_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_full_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_full_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_full_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_full_record_minor_positive_cell = ff_row_mdm_prefix_mce_full_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_full_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_full_record_minor_positive)) /\ ff_row_mdm_cell_mce_full_record_minor_positive_cell = S ff_row_mdm_prefix_mce_full_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_full_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_full_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_full_record_minor_positive) = (ff_index_mce_family_full)) /\ ff_column_mdm_cell_mce_full_record_minor_positive_cell = ff_column_mdm_prefix_mce_full_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_full_record_minor_positive_cell_column_after + (ff_index_mce_family_full) = (ff_column_mdm_prefix_mce_full_record_minor_positive)) /\ ff_column_mdm_cell_mce_full_record_minor_positive_cell = S ff_column_mdm_prefix_mce_full_record_minor_positive))) /\ (((exists ff_h_mdm_mce_full_record_minor_positive_cell_source. ff_h_mdm_mce_full_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_full_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_full_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_full_record_minor_positive_cell_source. pb = ff_q_mdm_mce_full_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_full_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_full_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_full_record_minor_positive_target. ff_h_mdm_mce_full_record_minor_positive_target + S (ff_value_mdm_prefix_mce_full_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_full_record_minor_positive)) * ff_us_mce_record_full_record)) /\ exists ff_q_mdm_mce_full_record_minor_positive_target. ff_up_mce_record_full_record = ff_q_mdm_mce_full_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_full_record_minor_positive)) * ff_us_mce_record_full_record) + (ff_value_mdm_prefix_mce_full_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_full_record_minor_negative. (exists ff_gap_mdm_lt_mce_full_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_full_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_full_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_full_record_minor_negative ff_column_mdm_prefix_mce_full_record_minor_negative ff_value_mdm_prefix_mce_full_record_minor_negative. (ff_index_mdm_prefix_mce_full_record_minor_negative = (q) * ff_row_mdm_prefix_mce_full_record_minor_negative + ff_column_mdm_prefix_mce_full_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_full_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_full_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_full_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_full_record_minor_negative_cell ff_column_mdm_cell_mce_full_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_full_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_full_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_full_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_full_record_minor_negative_cell = ff_row_mdm_prefix_mce_full_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_full_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_full_record_minor_negative)) /\ ff_row_mdm_cell_mce_full_record_minor_negative_cell = S ff_row_mdm_prefix_mce_full_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_full_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_full_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_full_record_minor_negative) = (ff_index_mce_family_full)) /\ ff_column_mdm_cell_mce_full_record_minor_negative_cell = ff_column_mdm_prefix_mce_full_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_full_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_full_record_minor_negative_cell_column_after + (ff_index_mce_family_full) = (ff_column_mdm_prefix_mce_full_record_minor_negative)) /\ ff_column_mdm_cell_mce_full_record_minor_negative_cell = S ff_column_mdm_prefix_mce_full_record_minor_negative))) /\ (((exists ff_h_mdm_mce_full_record_minor_negative_cell_source. ff_h_mdm_mce_full_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_full_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_full_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_full_record_minor_negative_cell_source. nb = ff_q_mdm_mce_full_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_full_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_full_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_full_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_full_record_minor_negative_target. ff_h_mdm_mce_full_record_minor_negative_target + S (ff_value_mdm_prefix_mce_full_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_full_record_minor_negative)) * ff_ut_mce_record_full_record)) /\ exists ff_q_mdm_mce_full_record_minor_negative_target. ff_un_mce_record_full_record = ff_q_mdm_mce_full_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_full_record_minor_negative)) * ff_ut_mce_record_full_record) + (ff_value_mdm_prefix_mce_full_record_minor_negative)))))))))))))
  11. 0011specialize signed_cofactor_minor_family_exists pb
  12. 0012specialize signed_cofactor_minor_family_exists pc
  13. 0013specialize signed_cofactor_minor_family_exists nb
  14. 0014specialize signed_cofactor_minor_family_exists nc
  15. 0015specialize signed_cofactor_minor_family_exists q
  16. 0016exact signed_cofactor_minor_family_exists
  17. 0017cases hfamily
  18. 0018cases hfamily_witness
  19. 0019have hfold : exists p n. (exists ff_ab_mce_row_result ff_ac_mce_row_result ff_db_mce_row_result ff_dc_mce_row_result. ((forall ff_index_mcp_mce_result_positive ff_source_mcp_mce_result_positive ff_target_mcp_mce_result_positive. (exists mcp_gap_mce_result_positive_bound. mcp_gap_mce_result_positive_bound + S (ff_index_mcp_mce_result_positive) = (S (q))) -> (((exists fs_h_mcp_mce_result_positive_source. fs_h_mcp_mce_result_positive_source + S (ff_source_mcp_mce_result_positive) = S ((S ((0) + (1) * ff_index_mcp_mce_result_positive)) * pc)) /\ exists fs_q_mcp_mce_result_positive_source. pb = fs_q_mcp_mce_result_positive_source * S ((S ((0) + (1) * ff_index_mcp_mce_result_positive)) * pc) + (ff_source_mcp_mce_result_positive))) -> (((exists fs_h_mcp_mce_result_positive_target. fs_h_mcp_mce_result_positive_target + S (ff_target_mcp_mce_result_positive) = S ((S (ff_index_mcp_mce_result_positive)) * ff_ac_mce_row_result)) /\ exists fs_q_mcp_mce_result_positive_target. ff_ab_mce_row_result = fs_q_mcp_mce_result_positive_target * S ((S (ff_index_mcp_mce_result_positive)) * ff_ac_mce_row_result) + (ff_target_mcp_mce_result_positive))) -> ff_target_mcp_mce_result_positive = ff_source_mcp_mce_result_positive) /\ ((forall ff_index_mcp_mce_result_negative ff_source_mcp_mce_result_negative ff_target_mcp_mce_result_negative. (exists mcp_gap_mce_result_negative_bound. mcp_gap_mce_result_negative_bound + S (ff_index_mcp_mce_result_negative) = (S (q))) -> (((exists fs_h_mcp_mce_result_negative_source. fs_h_mcp_mce_result_negative_source + S (ff_source_mcp_mce_result_negative) = S ((S ((0) + (1) * ff_index_mcp_mce_result_negative)) * nc)) /\ exists fs_q_mcp_mce_result_negative_source. nb = fs_q_mcp_mce_result_negative_source * S ((S ((0) + (1) * ff_index_mcp_mce_result_negative)) * nc) + (ff_source_mcp_mce_result_negative))) -> (((exists fs_h_mcp_mce_result_negative_target. fs_h_mcp_mce_result_negative_target + S (ff_target_mcp_mce_result_negative) = S ((S (ff_index_mcp_mce_result_negative)) * ff_dc_mce_row_result)) /\ exists fs_q_mcp_mce_result_negative_target. ff_db_mce_row_result = fs_q_mcp_mce_result_negative_target * S ((S (ff_index_mcp_mce_result_negative)) * ff_dc_mce_row_result) + (ff_target_mcp_mce_result_negative))) -> ff_target_mcp_mce_result_negative = ff_source_mcp_mce_result_negative) /\ (exists ff_ub_mce_fold_result_fold ff_uc_mce_fold_result_fold ff_vb_mce_fold_result_fold ff_vc_mce_fold_result_fold. ((forall ff_index_mce_alternating_result_fold_prefix. (exists ff_gap_mce_result_fold_prefix_index. ff_gap_mce_result_fold_prefix_index + S (ff_index_mce_alternating_result_fold_prefix) = (S (q))) -> exists ff_ap_mce_alternating_result_fold_prefix ff_an_mce_alternating_result_fold_prefix ff_bp_mce_alternating_result_fold_prefix ff_bn_mce_alternating_result_fold_prefix ff_p_mce_alternating_result_fold_prefix ff_n_mce_alternating_result_fold_prefix. ((((exists ff_h_mce_result_fold_prefix_ap. ff_h_mce_result_fold_prefix_ap + S (ff_ap_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_ac_mce_row_result)) /\ exists ff_q_mce_result_fold_prefix_ap. ff_ab_mce_row_result = ff_q_mce_result_fold_prefix_ap * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_ac_mce_row_result) + (ff_ap_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_an. ff_h_mce_result_fold_prefix_an + S (ff_an_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_dc_mce_row_result)) /\ exists ff_q_mce_result_fold_prefix_an. ff_db_mce_row_result = ff_q_mce_result_fold_prefix_an * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_dc_mce_row_result) + (ff_an_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_bp. ff_h_mce_result_fold_prefix_bp + S (ff_bp_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ec)) /\ exists ff_q_mce_result_fold_prefix_bp. eb = ff_q_mce_result_fold_prefix_bp * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ec) + (ff_bp_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_bn. ff_h_mce_result_fold_prefix_bn + S (ff_bn_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * fc)) /\ exists ff_q_mce_result_fold_prefix_bn. fb = ff_q_mce_result_fold_prefix_bn * S ((S (ff_index_mce_alternating_result_fold_prefix)) * fc) + (ff_bn_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_positive. ff_h_mce_result_fold_prefix_positive + S (ff_p_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_uc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_prefix_positive. ff_ub_mce_fold_result_fold = ff_q_mce_result_fold_prefix_positive * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_uc_mce_fold_result_fold) + (ff_p_mce_alternating_result_fold_prefix))) /\ ((((exists ff_h_mce_result_fold_prefix_negative. ff_h_mce_result_fold_prefix_negative + S (ff_n_mce_alternating_result_fold_prefix) = S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_vc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_prefix_negative. ff_vb_mce_fold_result_fold = ff_q_mce_result_fold_prefix_negative * S ((S (ff_index_mce_alternating_result_fold_prefix)) * ff_vc_mce_fold_result_fold) + (ff_n_mce_alternating_result_fold_prefix))) /\ (((exists ff_even_mce_term_result_fold_prefix_term. ff_index_mce_alternating_result_fold_prefix = 2 * ff_even_mce_term_result_fold_prefix_term) /\ (ff_p_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) /\ ff_n_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix))) \/ ((exists ff_odd_mce_term_result_fold_prefix_term. ff_index_mce_alternating_result_fold_prefix = 2 * ff_odd_mce_term_result_fold_prefix_term + 1) /\ (ff_p_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) /\ ff_n_mce_alternating_result_fold_prefix = (ff_ap_mce_alternating_result_fold_prefix) * (ff_bp_mce_alternating_result_fold_prefix) + (ff_an_mce_alternating_result_fold_prefix) * (ff_bn_mce_alternating_result_fold_prefix))))))))))) /\ ((exists ff_u_mce_result_fold_positive ff_v_mce_result_fold_positive. ((((exists ff_h_mce_result_fold_positive_start. ff_h_mce_result_fold_positive_start + S (0) = S ((S (0)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_start. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_start * S ((S (0)) * ff_v_mce_result_fold_positive) + (0))) /\ ((((exists ff_h_mce_result_fold_positive_terminal. ff_h_mce_result_fold_positive_terminal + S (p) = S ((S ((S (q)))) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_terminal. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_terminal * S ((S ((S (q)))) * ff_v_mce_result_fold_positive) + (p))) /\ forall ff_i_mce_result_fold_positive. (exists ff_lt_mce_result_fold_positive_bound. ff_lt_mce_result_fold_positive_bound + S ff_i_mce_result_fold_positive = (S (q))) -> exists ff_a_mce_result_fold_positive ff_r_mce_result_fold_positive ff_s_mce_result_fold_positive. ((((exists ff_h_mce_result_fold_positive_summand. ff_h_mce_result_fold_positive_summand + S (ff_a_mce_result_fold_positive) = S ((S (ff_i_mce_result_fold_positive)) * ff_uc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_positive_summand. ff_ub_mce_fold_result_fold = ff_q_mce_result_fold_positive_summand * S ((S (ff_i_mce_result_fold_positive)) * ff_uc_mce_fold_result_fold) + (ff_a_mce_result_fold_positive))) /\ ((((exists ff_h_mce_result_fold_positive_partial. ff_h_mce_result_fold_positive_partial + S (ff_r_mce_result_fold_positive) = S ((S (ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_partial. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_partial * S ((S (ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive) + (ff_r_mce_result_fold_positive))) /\ ((((exists ff_h_mce_result_fold_positive_successor. ff_h_mce_result_fold_positive_successor + S (ff_s_mce_result_fold_positive) = S ((S (S ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive)) /\ exists ff_q_mce_result_fold_positive_successor. ff_u_mce_result_fold_positive = ff_q_mce_result_fold_positive_successor * S ((S (S ff_i_mce_result_fold_positive)) * ff_v_mce_result_fold_positive) + (ff_s_mce_result_fold_positive))) /\ ff_s_mce_result_fold_positive = ff_r_mce_result_fold_positive + ff_a_mce_result_fold_positive)))))) /\ (exists ff_u_mce_result_fold_negative ff_v_mce_result_fold_negative. ((((exists ff_h_mce_result_fold_negative_start. ff_h_mce_result_fold_negative_start + S (0) = S ((S (0)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_start. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_start * S ((S (0)) * ff_v_mce_result_fold_negative) + (0))) /\ ((((exists ff_h_mce_result_fold_negative_terminal. ff_h_mce_result_fold_negative_terminal + S (n) = S ((S ((S (q)))) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_terminal. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_terminal * S ((S ((S (q)))) * ff_v_mce_result_fold_negative) + (n))) /\ forall ff_i_mce_result_fold_negative. (exists ff_lt_mce_result_fold_negative_bound. ff_lt_mce_result_fold_negative_bound + S ff_i_mce_result_fold_negative = (S (q))) -> exists ff_a_mce_result_fold_negative ff_r_mce_result_fold_negative ff_s_mce_result_fold_negative. ((((exists ff_h_mce_result_fold_negative_summand. ff_h_mce_result_fold_negative_summand + S (ff_a_mce_result_fold_negative) = S ((S (ff_i_mce_result_fold_negative)) * ff_vc_mce_fold_result_fold)) /\ exists ff_q_mce_result_fold_negative_summand. ff_vb_mce_fold_result_fold = ff_q_mce_result_fold_negative_summand * S ((S (ff_i_mce_result_fold_negative)) * ff_vc_mce_fold_result_fold) + (ff_a_mce_result_fold_negative))) /\ ((((exists ff_h_mce_result_fold_negative_partial. ff_h_mce_result_fold_negative_partial + S (ff_r_mce_result_fold_negative) = S ((S (ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_partial. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_partial * S ((S (ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative) + (ff_r_mce_result_fold_negative))) /\ ((((exists ff_h_mce_result_fold_negative_successor. ff_h_mce_result_fold_negative_successor + S (ff_s_mce_result_fold_negative) = S ((S (S ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative)) /\ exists ff_q_mce_result_fold_negative_successor. ff_u_mce_result_fold_negative = ff_q_mce_result_fold_negative_successor * S ((S (S ff_i_mce_result_fold_negative)) * ff_v_mce_result_fold_negative) + (ff_s_mce_result_fold_negative))) /\ ff_s_mce_result_fold_negative = ff_r_mce_result_fold_negative + ff_a_mce_result_fold_negative))))))))))))
  20. 0020specialize signed_first_row_cofactor_fold_exists pb
  21. 0021specialize signed_first_row_cofactor_fold_exists pc
  22. 0022specialize signed_first_row_cofactor_fold_exists nb
  23. 0023specialize signed_first_row_cofactor_fold_exists nc
  24. 0024specialize signed_first_row_cofactor_fold_exists q
  25. 0025specialize signed_first_row_cofactor_fold_exists eb
  26. 0026specialize signed_first_row_cofactor_fold_exists ec
  27. 0027specialize signed_first_row_cofactor_fold_exists fb
  28. 0028specialize signed_first_row_cofactor_fold_exists fc
  29. 0029exact signed_first_row_cofactor_fold_exists
  30. 0030cases hfold
  31. 0031cases hfold_witness
  32. 0032exists x
  33. 0033exists x1
  34. 0034exists x2
  35. 0035exists x3
  36. 0036split
  37. 0037exact hfamily_witness_witness
  38. 0038exact hfold_witness_witness