CE0007

signed_cofactor_minor_prefix_extend

Appending one genuinely constructed signed minor preserves every previously encoded cofactor record.

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. ∀ u. ∀ v. ∀ l. ∀ k. SignedCofactorMinorPrefix(pb,pc,nb,nc,q,u,v,l) → SignedMinorRecord(pb,pc,nb,nc,q,l,k) → ∃ x. ∃ y. SignedCofactorMinorPrefix(pb,pc,nb,nc,q,x,y,S l)

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

Definition DAG

SignedMinorRecord(pb,pc,nb,nc,q,j,z) · 1SignedCofactorMinorPrefix(pb,pc,nb,nc,q,b,c,l) · 2

Actual proof prerequisites

beta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall pb pc nb nc q u v l k. (forall ff_index_mce_family_before. (exists ff_gap_mce_before_index. ff_gap_mce_before_index + S (ff_index_mce_family_before) = (l)) -> exists ff_value_mce_family_before. ((((exists ff_h_mce_before_entry. ff_h_mce_before_entry + S (ff_value_mce_family_before) = S ((S (ff_index_mce_family_before)) * v)) /\ exists ff_q_mce_before_entry. u = ff_q_mce_before_entry * S ((S (ff_index_mce_family_before)) * v) + (ff_value_mce_family_before))) /\ (exists ff_up_mce_record_before_record ff_us_mce_record_before_record ff_un_mce_record_before_record ff_ut_mce_record_before_record. ((ff_value_mce_family_before = ((((ff_up_mce_record_before_record) + (ff_us_mce_record_before_record)) * S ((ff_up_mce_record_before_record) + (ff_us_mce_record_before_record)) + ((ff_us_mce_record_before_record) + (ff_us_mce_record_before_record))) + (((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) * S ((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) + ((ff_ut_mce_record_before_record) + (ff_ut_mce_record_before_record)))) * S ((((ff_up_mce_record_before_record) + (ff_us_mce_record_before_record)) * S ((ff_up_mce_record_before_record) + (ff_us_mce_record_before_record)) + ((ff_us_mce_record_before_record) + (ff_us_mce_record_before_record))) + (((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) * S ((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) + ((ff_ut_mce_record_before_record) + (ff_ut_mce_record_before_record)))) + ((((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) * S ((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) + ((ff_ut_mce_record_before_record) + (ff_ut_mce_record_before_record))) + (((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) * S ((ff_un_mce_record_before_record) + (ff_ut_mce_record_before_record)) + ((ff_ut_mce_record_before_record) + (ff_ut_mce_record_before_record))))) /\ (((forall ff_index_mdm_prefix_mce_before_record_minor_positive. (exists ff_gap_mdm_lt_mce_before_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_before_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_before_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_before_record_minor_positive ff_column_mdm_prefix_mce_before_record_minor_positive ff_value_mdm_prefix_mce_before_record_minor_positive. (ff_index_mdm_prefix_mce_before_record_minor_positive = (q) * ff_row_mdm_prefix_mce_before_record_minor_positive + ff_column_mdm_prefix_mce_before_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_before_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_before_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_before_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_before_record_minor_positive_cell ff_column_mdm_cell_mce_before_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_before_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_before_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_before_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_before_record_minor_positive_cell = ff_row_mdm_prefix_mce_before_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_before_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_before_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_before_record_minor_positive)) /\ ff_row_mdm_cell_mce_before_record_minor_positive_cell = S ff_row_mdm_prefix_mce_before_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_before_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_before_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_before_record_minor_positive) = (ff_index_mce_family_before)) /\ ff_column_mdm_cell_mce_before_record_minor_positive_cell = ff_column_mdm_prefix_mce_before_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_before_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_before_record_minor_positive_cell_column_after + (ff_index_mce_family_before) = (ff_column_mdm_prefix_mce_before_record_minor_positive)) /\ ff_column_mdm_cell_mce_before_record_minor_positive_cell = S ff_column_mdm_prefix_mce_before_record_minor_positive))) /\ (((exists ff_h_mdm_mce_before_record_minor_positive_cell_source. ff_h_mdm_mce_before_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_before_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_before_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_before_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_before_record_minor_positive_cell_source. pb = ff_q_mdm_mce_before_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_before_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_before_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_before_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_before_record_minor_positive_target. ff_h_mdm_mce_before_record_minor_positive_target + S (ff_value_mdm_prefix_mce_before_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_before_record_minor_positive)) * ff_us_mce_record_before_record)) /\ exists ff_q_mdm_mce_before_record_minor_positive_target. ff_up_mce_record_before_record = ff_q_mdm_mce_before_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_before_record_minor_positive)) * ff_us_mce_record_before_record) + (ff_value_mdm_prefix_mce_before_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_before_record_minor_negative. (exists ff_gap_mdm_lt_mce_before_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_before_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_before_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_before_record_minor_negative ff_column_mdm_prefix_mce_before_record_minor_negative ff_value_mdm_prefix_mce_before_record_minor_negative. (ff_index_mdm_prefix_mce_before_record_minor_negative = (q) * ff_row_mdm_prefix_mce_before_record_minor_negative + ff_column_mdm_prefix_mce_before_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_before_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_before_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_before_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_before_record_minor_negative_cell ff_column_mdm_cell_mce_before_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_before_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_before_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_before_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_before_record_minor_negative_cell = ff_row_mdm_prefix_mce_before_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_before_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_before_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_before_record_minor_negative)) /\ ff_row_mdm_cell_mce_before_record_minor_negative_cell = S ff_row_mdm_prefix_mce_before_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_before_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_before_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_before_record_minor_negative) = (ff_index_mce_family_before)) /\ ff_column_mdm_cell_mce_before_record_minor_negative_cell = ff_column_mdm_prefix_mce_before_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_before_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_before_record_minor_negative_cell_column_after + (ff_index_mce_family_before) = (ff_column_mdm_prefix_mce_before_record_minor_negative)) /\ ff_column_mdm_cell_mce_before_record_minor_negative_cell = S ff_column_mdm_prefix_mce_before_record_minor_negative))) /\ (((exists ff_h_mdm_mce_before_record_minor_negative_cell_source. ff_h_mdm_mce_before_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_before_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_before_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_before_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_before_record_minor_negative_cell_source. nb = ff_q_mdm_mce_before_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_before_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_before_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_before_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_before_record_minor_negative_target. ff_h_mdm_mce_before_record_minor_negative_target + S (ff_value_mdm_prefix_mce_before_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_before_record_minor_negative)) * ff_ut_mce_record_before_record)) /\ exists ff_q_mdm_mce_before_record_minor_negative_target. ff_un_mce_record_before_record = ff_q_mdm_mce_before_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_before_record_minor_negative)) * ff_ut_mce_record_before_record) + (ff_value_mdm_prefix_mce_before_record_minor_negative))))))))))))) -> (exists ff_up_mce_record_last ff_us_mce_record_last ff_un_mce_record_last ff_ut_mce_record_last. ((k = ((((ff_up_mce_record_last) + (ff_us_mce_record_last)) * S ((ff_up_mce_record_last) + (ff_us_mce_record_last)) + ((ff_us_mce_record_last) + (ff_us_mce_record_last))) + (((ff_un_mce_record_last) + (ff_ut_mce_record_last)) * S ((ff_un_mce_record_last) + (ff_ut_mce_record_last)) + ((ff_ut_mce_record_last) + (ff_ut_mce_record_last)))) * S ((((ff_up_mce_record_last) + (ff_us_mce_record_last)) * S ((ff_up_mce_record_last) + (ff_us_mce_record_last)) + ((ff_us_mce_record_last) + (ff_us_mce_record_last))) + (((ff_un_mce_record_last) + (ff_ut_mce_record_last)) * S ((ff_un_mce_record_last) + (ff_ut_mce_record_last)) + ((ff_ut_mce_record_last) + (ff_ut_mce_record_last)))) + ((((ff_un_mce_record_last) + (ff_ut_mce_record_last)) * S ((ff_un_mce_record_last) + (ff_ut_mce_record_last)) + ((ff_ut_mce_record_last) + (ff_ut_mce_record_last))) + (((ff_un_mce_record_last) + (ff_ut_mce_record_last)) * S ((ff_un_mce_record_last) + (ff_ut_mce_record_last)) + ((ff_ut_mce_record_last) + (ff_ut_mce_record_last))))) /\ (((forall ff_index_mdm_prefix_mce_last_minor_positive. (exists ff_gap_mdm_lt_mce_last_minor_positive_index_bound. ff_gap_mdm_lt_mce_last_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_last_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_last_minor_positive ff_column_mdm_prefix_mce_last_minor_positive ff_value_mdm_prefix_mce_last_minor_positive. (ff_index_mdm_prefix_mce_last_minor_positive = (q) * ff_row_mdm_prefix_mce_last_minor_positive + ff_column_mdm_prefix_mce_last_minor_positive /\ ((exists ff_gap_mdm_lt_mce_last_minor_positive_column_bound. ff_gap_mdm_lt_mce_last_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_last_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_last_minor_positive_cell ff_column_mdm_cell_mce_last_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_last_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_last_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_last_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_last_minor_positive_cell = ff_row_mdm_prefix_mce_last_minor_positive) \/ ((exists ff_gap_mdm_le_mce_last_minor_positive_cell_row_after. ff_gap_mdm_le_mce_last_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_last_minor_positive)) /\ ff_row_mdm_cell_mce_last_minor_positive_cell = S ff_row_mdm_prefix_mce_last_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_last_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_last_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_last_minor_positive) = (l)) /\ ff_column_mdm_cell_mce_last_minor_positive_cell = ff_column_mdm_prefix_mce_last_minor_positive) \/ ((exists ff_gap_mdm_le_mce_last_minor_positive_cell_column_after. ff_gap_mdm_le_mce_last_minor_positive_cell_column_after + (l) = (ff_column_mdm_prefix_mce_last_minor_positive)) /\ ff_column_mdm_cell_mce_last_minor_positive_cell = S ff_column_mdm_prefix_mce_last_minor_positive))) /\ (((exists ff_h_mdm_mce_last_minor_positive_cell_source. ff_h_mdm_mce_last_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_last_minor_positive) = S ((S ((ff_row_mdm_cell_mce_last_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_last_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_last_minor_positive_cell_source. pb = ff_q_mdm_mce_last_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_last_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_last_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_last_minor_positive)))))) /\ (((exists ff_h_mdm_mce_last_minor_positive_target. ff_h_mdm_mce_last_minor_positive_target + S (ff_value_mdm_prefix_mce_last_minor_positive) = S ((S (ff_index_mdm_prefix_mce_last_minor_positive)) * ff_us_mce_record_last)) /\ exists ff_q_mdm_mce_last_minor_positive_target. ff_up_mce_record_last = ff_q_mdm_mce_last_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_last_minor_positive)) * ff_us_mce_record_last) + (ff_value_mdm_prefix_mce_last_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_last_minor_negative. (exists ff_gap_mdm_lt_mce_last_minor_negative_index_bound. ff_gap_mdm_lt_mce_last_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_last_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_last_minor_negative ff_column_mdm_prefix_mce_last_minor_negative ff_value_mdm_prefix_mce_last_minor_negative. (ff_index_mdm_prefix_mce_last_minor_negative = (q) * ff_row_mdm_prefix_mce_last_minor_negative + ff_column_mdm_prefix_mce_last_minor_negative /\ ((exists ff_gap_mdm_lt_mce_last_minor_negative_column_bound. ff_gap_mdm_lt_mce_last_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_last_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_last_minor_negative_cell ff_column_mdm_cell_mce_last_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_last_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_last_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_last_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_last_minor_negative_cell = ff_row_mdm_prefix_mce_last_minor_negative) \/ ((exists ff_gap_mdm_le_mce_last_minor_negative_cell_row_after. ff_gap_mdm_le_mce_last_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_last_minor_negative)) /\ ff_row_mdm_cell_mce_last_minor_negative_cell = S ff_row_mdm_prefix_mce_last_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_last_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_last_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_last_minor_negative) = (l)) /\ ff_column_mdm_cell_mce_last_minor_negative_cell = ff_column_mdm_prefix_mce_last_minor_negative) \/ ((exists ff_gap_mdm_le_mce_last_minor_negative_cell_column_after. ff_gap_mdm_le_mce_last_minor_negative_cell_column_after + (l) = (ff_column_mdm_prefix_mce_last_minor_negative)) /\ ff_column_mdm_cell_mce_last_minor_negative_cell = S ff_column_mdm_prefix_mce_last_minor_negative))) /\ (((exists ff_h_mdm_mce_last_minor_negative_cell_source. ff_h_mdm_mce_last_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_last_minor_negative) = S ((S ((ff_row_mdm_cell_mce_last_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_last_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_last_minor_negative_cell_source. nb = ff_q_mdm_mce_last_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_last_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_last_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_last_minor_negative)))))) /\ (((exists ff_h_mdm_mce_last_minor_negative_target. ff_h_mdm_mce_last_minor_negative_target + S (ff_value_mdm_prefix_mce_last_minor_negative) = S ((S (ff_index_mdm_prefix_mce_last_minor_negative)) * ff_ut_mce_record_last)) /\ exists ff_q_mdm_mce_last_minor_negative_target. ff_un_mce_record_last = ff_q_mdm_mce_last_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_last_minor_negative)) * ff_ut_mce_record_last) + (ff_value_mdm_prefix_mce_last_minor_negative))))))))))) -> exists z e. (forall ff_index_mce_family_after. (exists ff_gap_mce_after_index. ff_gap_mce_after_index + S (ff_index_mce_family_after) = (S l)) -> exists ff_value_mce_family_after. ((((exists ff_h_mce_after_entry. ff_h_mce_after_entry + S (ff_value_mce_family_after) = S ((S (ff_index_mce_family_after)) * e)) /\ exists ff_q_mce_after_entry. z = ff_q_mce_after_entry * S ((S (ff_index_mce_family_after)) * e) + (ff_value_mce_family_after))) /\ (exists ff_up_mce_record_after_record ff_us_mce_record_after_record ff_un_mce_record_after_record ff_ut_mce_record_after_record. ((ff_value_mce_family_after = ((((ff_up_mce_record_after_record) + (ff_us_mce_record_after_record)) * S ((ff_up_mce_record_after_record) + (ff_us_mce_record_after_record)) + ((ff_us_mce_record_after_record) + (ff_us_mce_record_after_record))) + (((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) * S ((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) + ((ff_ut_mce_record_after_record) + (ff_ut_mce_record_after_record)))) * S ((((ff_up_mce_record_after_record) + (ff_us_mce_record_after_record)) * S ((ff_up_mce_record_after_record) + (ff_us_mce_record_after_record)) + ((ff_us_mce_record_after_record) + (ff_us_mce_record_after_record))) + (((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) * S ((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) + ((ff_ut_mce_record_after_record) + (ff_ut_mce_record_after_record)))) + ((((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) * S ((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) + ((ff_ut_mce_record_after_record) + (ff_ut_mce_record_after_record))) + (((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) * S ((ff_un_mce_record_after_record) + (ff_ut_mce_record_after_record)) + ((ff_ut_mce_record_after_record) + (ff_ut_mce_record_after_record))))) /\ (((forall ff_index_mdm_prefix_mce_after_record_minor_positive. (exists ff_gap_mdm_lt_mce_after_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_after_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_after_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_after_record_minor_positive ff_column_mdm_prefix_mce_after_record_minor_positive ff_value_mdm_prefix_mce_after_record_minor_positive. (ff_index_mdm_prefix_mce_after_record_minor_positive = (q) * ff_row_mdm_prefix_mce_after_record_minor_positive + ff_column_mdm_prefix_mce_after_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_after_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_after_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_after_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_after_record_minor_positive_cell ff_column_mdm_cell_mce_after_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_after_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_after_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_after_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_after_record_minor_positive_cell = ff_row_mdm_prefix_mce_after_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_after_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_after_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_after_record_minor_positive)) /\ ff_row_mdm_cell_mce_after_record_minor_positive_cell = S ff_row_mdm_prefix_mce_after_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_after_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_after_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_after_record_minor_positive) = (ff_index_mce_family_after)) /\ ff_column_mdm_cell_mce_after_record_minor_positive_cell = ff_column_mdm_prefix_mce_after_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_after_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_after_record_minor_positive_cell_column_after + (ff_index_mce_family_after) = (ff_column_mdm_prefix_mce_after_record_minor_positive)) /\ ff_column_mdm_cell_mce_after_record_minor_positive_cell = S ff_column_mdm_prefix_mce_after_record_minor_positive))) /\ (((exists ff_h_mdm_mce_after_record_minor_positive_cell_source. ff_h_mdm_mce_after_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_after_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_after_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_after_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_after_record_minor_positive_cell_source. pb = ff_q_mdm_mce_after_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_after_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_after_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_after_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_after_record_minor_positive_target. ff_h_mdm_mce_after_record_minor_positive_target + S (ff_value_mdm_prefix_mce_after_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_after_record_minor_positive)) * ff_us_mce_record_after_record)) /\ exists ff_q_mdm_mce_after_record_minor_positive_target. ff_up_mce_record_after_record = ff_q_mdm_mce_after_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_after_record_minor_positive)) * ff_us_mce_record_after_record) + (ff_value_mdm_prefix_mce_after_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_after_record_minor_negative. (exists ff_gap_mdm_lt_mce_after_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_after_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_after_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_after_record_minor_negative ff_column_mdm_prefix_mce_after_record_minor_negative ff_value_mdm_prefix_mce_after_record_minor_negative. (ff_index_mdm_prefix_mce_after_record_minor_negative = (q) * ff_row_mdm_prefix_mce_after_record_minor_negative + ff_column_mdm_prefix_mce_after_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_after_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_after_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_after_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_after_record_minor_negative_cell ff_column_mdm_cell_mce_after_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_after_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_after_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_after_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_after_record_minor_negative_cell = ff_row_mdm_prefix_mce_after_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_after_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_after_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_after_record_minor_negative)) /\ ff_row_mdm_cell_mce_after_record_minor_negative_cell = S ff_row_mdm_prefix_mce_after_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_after_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_after_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_after_record_minor_negative) = (ff_index_mce_family_after)) /\ ff_column_mdm_cell_mce_after_record_minor_negative_cell = ff_column_mdm_prefix_mce_after_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_after_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_after_record_minor_negative_cell_column_after + (ff_index_mce_family_after) = (ff_column_mdm_prefix_mce_after_record_minor_negative)) /\ ff_column_mdm_cell_mce_after_record_minor_negative_cell = S ff_column_mdm_prefix_mce_after_record_minor_negative))) /\ (((exists ff_h_mdm_mce_after_record_minor_negative_cell_source. ff_h_mdm_mce_after_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_after_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_after_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_after_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_after_record_minor_negative_cell_source. nb = ff_q_mdm_mce_after_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_after_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_after_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_after_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_after_record_minor_negative_target. ff_h_mdm_mce_after_record_minor_negative_target + S (ff_value_mdm_prefix_mce_after_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_after_record_minor_negative)) * ff_ut_mce_record_after_record)) /\ exists ff_q_mdm_mce_after_record_minor_negative_target. ff_un_mce_record_after_record = ff_q_mdm_mce_after_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_after_record_minor_negative)) * ff_ut_mce_record_after_record) + (ff_value_mdm_prefix_mce_after_record_minor_negative)))))))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

54 script commands · 19 reading checkpoints · 3 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.

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

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 u
  7. L7
    intro v
  8. L8
    intro l
  9. L9
    intro k
  10. L10
    intro hprefix
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hrecord
03Establish hextL12–17

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

  1. L12
    have hext : ∃ z. ∃ e. Beta(z,e,l,k) ∧ (∀ x. ∀ y. Lt(x,l) → Beta(u,v,x,y) → Beta(z,e,x,y))Definitions: BetaLtOriginal native command in the exact edition
  2. L13
    specialize beta_prefix_extend l
  3. L14
    specialize beta_prefix_extend u
  4. L15
    specialize beta_prefix_extend v
  5. L16
    specialize beta_prefix_extend k
  6. L17
    exact beta_prefix_extend
04Separate the logical casesL18–20

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

  1. L18
    cases hext
  2. L19
    cases hext_witness
  3. L20
    cases hext_witness_witness
05Construct an explicit witnessL21–22

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

  1. L21
    exists x
  2. L22
    exists x1
06Fix variables and assumptionsL23–24

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

  1. L23
    intro i
  2. L24
    intro hi
07Establish hsplitL25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L25
    have hsplit : i = l \/ exists gap. gap + S i = l
  2. L26
    specialize finite_lt_succ_eq_or_lt l
  3. L27
    specialize finite_lt_succ_eq_or_lt i
  4. L28
    apply finite_lt_succ_eq_or_lt
  5. L29
    exact hi
08Separate the logical casesL30–30

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

  1. L30
    cases hsplit
09Construct an explicit witnessL31–31

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

  1. L31
    exists k
10Separate the logical casesL32–32

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

  1. L32
    split
11Calculate and transport equalitiesL33–34

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

  1. L33
    rewrite hsplit_left
  2. L34
    rewrite hsplit_left
12Use earlier factsL35–35

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

  1. L35
    exact hext_witness_witness_left
13Calculate and transport equalitiesL36–39

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

  1. L36
    rewrite hsplit_left
  2. L37
    rewrite hsplit_left
  3. L38
    rewrite hsplit_left
  4. L39
    rewrite hsplit_left
14Use earlier factsL40–40

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

  1. L40
    exact hrecord
15Establish hpreviousL41–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L41
    have hprevious : ∃ a. Beta(u,v,i,a) ∧ SignedMinorRecord(pb,pc,nb,nc,q,i,a)Definitions: BetaSignedMinorRecordOriginal native command in the exact edition
  2. L42
    specialize hprefix i
  3. L43
    apply hprefix
  4. L44
    exact hsplit_right
16Separate the logical casesL45–46

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

  1. L45
    cases hprevious
  2. L46
    cases hprevious_witness
17Construct an explicit witnessL47–47

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

  1. L47
    exists x2
18Separate the logical casesL48–48

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

  1. L48
    split
19Use earlier factsL49–54

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

  1. L49
    specialize hext_witness_witness_right i
  2. L50
    specialize hext_witness_witness_right x2
  3. L51
    apply hext_witness_witness_right
  4. L52
    exact hsplit_right
  5. L53
    exact hprevious_witness_left
  6. L54
    exact hprevious_witness_right

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro q
  6. 0006intro u
  7. 0007intro v
  8. 0008intro l
  9. 0009intro k
  10. 0010intro hprefix
  11. 0011intro hrecord
  12. 0012have hext : exists z e. ((((exists ff_h_mce_family_extension. ff_h_mce_family_extension + S (k) = S ((S (l)) * e)) /\ exists ff_q_mce_family_extension. z = ff_q_mce_family_extension * S ((S (l)) * e) + (k))) /\ forall i a. (exists ff_gap_mce_family_preserved. ff_gap_mce_family_preserved + S (i) = (l)) -> (((exists ff_h_mce_family_old. ff_h_mce_family_old + S (a) = S ((S (i)) * v)) /\ exists ff_q_mce_family_old. u = ff_q_mce_family_old * S ((S (i)) * v) + (a))) -> (((exists ff_h_mce_family_new. ff_h_mce_family_new + S (a) = S ((S (i)) * e)) /\ exists ff_q_mce_family_new. z = ff_q_mce_family_new * S ((S (i)) * e) + (a))))
  13. 0013specialize beta_prefix_extend l
  14. 0014specialize beta_prefix_extend u
  15. 0015specialize beta_prefix_extend v
  16. 0016specialize beta_prefix_extend k
  17. 0017exact beta_prefix_extend
  18. 0018cases hext
  19. 0019cases hext_witness
  20. 0020cases hext_witness_witness
  21. 0021exists x
  22. 0022exists x1
  23. 0023intro i
  24. 0024intro hi
  25. 0025have hsplit : i = l \/ exists gap. gap + S i = l
  26. 0026specialize finite_lt_succ_eq_or_lt l
  27. 0027specialize finite_lt_succ_eq_or_lt i
  28. 0028apply finite_lt_succ_eq_or_lt
  29. 0029exact hi
  30. 0030cases hsplit
  31. 0031exists k
  32. 0032split
  33. 0033rewrite hsplit_left
  34. 0034rewrite hsplit_left
  35. 0035exact hext_witness_witness_left
  36. 0036rewrite hsplit_left
  37. 0037rewrite hsplit_left
  38. 0038rewrite hsplit_left
  39. 0039rewrite hsplit_left
  40. 0040exact hrecord
  41. 0041have hprevious : exists a. ((((exists ff_h_mce_family_have_previous. ff_h_mce_family_have_previous + S (a) = S ((S (i)) * v)) /\ exists ff_q_mce_family_have_previous. u = ff_q_mce_family_have_previous * S ((S (i)) * v) + (a))) /\ (exists ff_up_mce_record_family_have_record ff_us_mce_record_family_have_record ff_un_mce_record_family_have_record ff_ut_mce_record_family_have_record. ((a = ((((ff_up_mce_record_family_have_record) + (ff_us_mce_record_family_have_record)) * S ((ff_up_mce_record_family_have_record) + (ff_us_mce_record_family_have_record)) + ((ff_us_mce_record_family_have_record) + (ff_us_mce_record_family_have_record))) + (((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) * S ((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) + ((ff_ut_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)))) * S ((((ff_up_mce_record_family_have_record) + (ff_us_mce_record_family_have_record)) * S ((ff_up_mce_record_family_have_record) + (ff_us_mce_record_family_have_record)) + ((ff_us_mce_record_family_have_record) + (ff_us_mce_record_family_have_record))) + (((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) * S ((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) + ((ff_ut_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)))) + ((((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) * S ((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) + ((ff_ut_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record))) + (((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) * S ((ff_un_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record)) + ((ff_ut_mce_record_family_have_record) + (ff_ut_mce_record_family_have_record))))) /\ (((forall ff_index_mdm_prefix_mce_family_have_record_minor_positive. (exists ff_gap_mdm_lt_mce_family_have_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_family_have_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_family_have_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_family_have_record_minor_positive ff_column_mdm_prefix_mce_family_have_record_minor_positive ff_value_mdm_prefix_mce_family_have_record_minor_positive. (ff_index_mdm_prefix_mce_family_have_record_minor_positive = (q) * ff_row_mdm_prefix_mce_family_have_record_minor_positive + ff_column_mdm_prefix_mce_family_have_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_family_have_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_family_have_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_family_have_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_family_have_record_minor_positive_cell ff_column_mdm_cell_mce_family_have_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_family_have_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_family_have_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_family_have_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_family_have_record_minor_positive_cell = ff_row_mdm_prefix_mce_family_have_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_family_have_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_family_have_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_family_have_record_minor_positive)) /\ ff_row_mdm_cell_mce_family_have_record_minor_positive_cell = S ff_row_mdm_prefix_mce_family_have_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_family_have_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_family_have_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_family_have_record_minor_positive) = (i)) /\ ff_column_mdm_cell_mce_family_have_record_minor_positive_cell = ff_column_mdm_prefix_mce_family_have_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_family_have_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_family_have_record_minor_positive_cell_column_after + (i) = (ff_column_mdm_prefix_mce_family_have_record_minor_positive)) /\ ff_column_mdm_cell_mce_family_have_record_minor_positive_cell = S ff_column_mdm_prefix_mce_family_have_record_minor_positive))) /\ (((exists ff_h_mdm_mce_family_have_record_minor_positive_cell_source. ff_h_mdm_mce_family_have_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_family_have_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_family_have_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_have_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_family_have_record_minor_positive_cell_source. pb = ff_q_mdm_mce_family_have_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_family_have_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_have_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_family_have_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_family_have_record_minor_positive_target. ff_h_mdm_mce_family_have_record_minor_positive_target + S (ff_value_mdm_prefix_mce_family_have_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_family_have_record_minor_positive)) * ff_us_mce_record_family_have_record)) /\ exists ff_q_mdm_mce_family_have_record_minor_positive_target. ff_up_mce_record_family_have_record = ff_q_mdm_mce_family_have_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_family_have_record_minor_positive)) * ff_us_mce_record_family_have_record) + (ff_value_mdm_prefix_mce_family_have_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_family_have_record_minor_negative. (exists ff_gap_mdm_lt_mce_family_have_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_family_have_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_family_have_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_family_have_record_minor_negative ff_column_mdm_prefix_mce_family_have_record_minor_negative ff_value_mdm_prefix_mce_family_have_record_minor_negative. (ff_index_mdm_prefix_mce_family_have_record_minor_negative = (q) * ff_row_mdm_prefix_mce_family_have_record_minor_negative + ff_column_mdm_prefix_mce_family_have_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_family_have_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_family_have_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_family_have_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_family_have_record_minor_negative_cell ff_column_mdm_cell_mce_family_have_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_family_have_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_family_have_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_family_have_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_family_have_record_minor_negative_cell = ff_row_mdm_prefix_mce_family_have_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_family_have_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_family_have_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_family_have_record_minor_negative)) /\ ff_row_mdm_cell_mce_family_have_record_minor_negative_cell = S ff_row_mdm_prefix_mce_family_have_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_family_have_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_family_have_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_family_have_record_minor_negative) = (i)) /\ ff_column_mdm_cell_mce_family_have_record_minor_negative_cell = ff_column_mdm_prefix_mce_family_have_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_family_have_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_family_have_record_minor_negative_cell_column_after + (i) = (ff_column_mdm_prefix_mce_family_have_record_minor_negative)) /\ ff_column_mdm_cell_mce_family_have_record_minor_negative_cell = S ff_column_mdm_prefix_mce_family_have_record_minor_negative))) /\ (((exists ff_h_mdm_mce_family_have_record_minor_negative_cell_source. ff_h_mdm_mce_family_have_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_family_have_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_family_have_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_have_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_family_have_record_minor_negative_cell_source. nb = ff_q_mdm_mce_family_have_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_family_have_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_family_have_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_family_have_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_family_have_record_minor_negative_target. ff_h_mdm_mce_family_have_record_minor_negative_target + S (ff_value_mdm_prefix_mce_family_have_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_family_have_record_minor_negative)) * ff_ut_mce_record_family_have_record)) /\ exists ff_q_mdm_mce_family_have_record_minor_negative_target. ff_un_mce_record_family_have_record = ff_q_mdm_mce_family_have_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_family_have_record_minor_negative)) * ff_ut_mce_record_family_have_record) + (ff_value_mdm_prefix_mce_family_have_record_minor_negative))))))))))))
  42. 0042specialize hprefix i
  43. 0043apply hprefix
  44. 0044exact hsplit_right
  45. 0045cases hprevious
  46. 0046cases hprevious_witness
  47. 0047exists x2
  48. 0048split
  49. 0049specialize hext_witness_witness_right i
  50. 0050specialize hext_witness_witness_right x2
  51. 0051apply hext_witness_witness_right
  52. 0052exact hsplit_right
  53. 0053exact hprevious_witness_left
  54. 0054exact hprevious_witness_right