CE0008

signed_cofactor_minor_prefix_exists_bounded

Every constructively bounded first-row cofactor prefix has one beta code containing all actual signed minors.

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

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

Definition DAG

SignedCofactorMinorPrefix(pb,pc,nb,nc,q,b,c,l) · 1Le(a,b) · 1

Actual proof prerequisites

le_of_succ_le_succ · checked external prerequisitele_succ · checked external prerequisitesigned_cofactor_minor_prefix_emptysigned_cofactor_minor_record_existssigned_cofactor_minor_prefix_extend
Original expanded first-order statement 
forall pb pc nb nc q l. (exists ff_gap_mce_family_length. ff_gap_mce_family_length + (l) = (S q)) -> exists u v. (forall ff_index_mce_family_result. (exists ff_gap_mce_result_index. ff_gap_mce_result_index + S (ff_index_mce_family_result) = (l)) -> exists ff_value_mce_family_result. ((((exists ff_h_mce_result_entry. ff_h_mce_result_entry + S (ff_value_mce_family_result) = S ((S (ff_index_mce_family_result)) * v)) /\ exists ff_q_mce_result_entry. u = ff_q_mce_result_entry * S ((S (ff_index_mce_family_result)) * v) + (ff_value_mce_family_result))) /\ (exists ff_up_mce_record_result_record ff_us_mce_record_result_record ff_un_mce_record_result_record ff_ut_mce_record_result_record. ((ff_value_mce_family_result = ((((ff_up_mce_record_result_record) + (ff_us_mce_record_result_record)) * S ((ff_up_mce_record_result_record) + (ff_us_mce_record_result_record)) + ((ff_us_mce_record_result_record) + (ff_us_mce_record_result_record))) + (((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) * S ((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) + ((ff_ut_mce_record_result_record) + (ff_ut_mce_record_result_record)))) * S ((((ff_up_mce_record_result_record) + (ff_us_mce_record_result_record)) * S ((ff_up_mce_record_result_record) + (ff_us_mce_record_result_record)) + ((ff_us_mce_record_result_record) + (ff_us_mce_record_result_record))) + (((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) * S ((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) + ((ff_ut_mce_record_result_record) + (ff_ut_mce_record_result_record)))) + ((((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) * S ((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) + ((ff_ut_mce_record_result_record) + (ff_ut_mce_record_result_record))) + (((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) * S ((ff_un_mce_record_result_record) + (ff_ut_mce_record_result_record)) + ((ff_ut_mce_record_result_record) + (ff_ut_mce_record_result_record))))) /\ (((forall ff_index_mdm_prefix_mce_result_record_minor_positive. (exists ff_gap_mdm_lt_mce_result_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_result_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_result_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_result_record_minor_positive ff_column_mdm_prefix_mce_result_record_minor_positive ff_value_mdm_prefix_mce_result_record_minor_positive. (ff_index_mdm_prefix_mce_result_record_minor_positive = (q) * ff_row_mdm_prefix_mce_result_record_minor_positive + ff_column_mdm_prefix_mce_result_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_result_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_result_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_result_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_result_record_minor_positive_cell ff_column_mdm_cell_mce_result_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_result_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_result_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_result_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_result_record_minor_positive_cell = ff_row_mdm_prefix_mce_result_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_result_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_result_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_result_record_minor_positive)) /\ ff_row_mdm_cell_mce_result_record_minor_positive_cell = S ff_row_mdm_prefix_mce_result_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_result_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_result_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_result_record_minor_positive) = (ff_index_mce_family_result)) /\ ff_column_mdm_cell_mce_result_record_minor_positive_cell = ff_column_mdm_prefix_mce_result_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_result_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_result_record_minor_positive_cell_column_after + (ff_index_mce_family_result) = (ff_column_mdm_prefix_mce_result_record_minor_positive)) /\ ff_column_mdm_cell_mce_result_record_minor_positive_cell = S ff_column_mdm_prefix_mce_result_record_minor_positive))) /\ (((exists ff_h_mdm_mce_result_record_minor_positive_cell_source. ff_h_mdm_mce_result_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_result_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_result_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_result_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_result_record_minor_positive_cell_source. pb = ff_q_mdm_mce_result_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_result_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_result_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_result_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_result_record_minor_positive_target. ff_h_mdm_mce_result_record_minor_positive_target + S (ff_value_mdm_prefix_mce_result_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_result_record_minor_positive)) * ff_us_mce_record_result_record)) /\ exists ff_q_mdm_mce_result_record_minor_positive_target. ff_up_mce_record_result_record = ff_q_mdm_mce_result_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_result_record_minor_positive)) * ff_us_mce_record_result_record) + (ff_value_mdm_prefix_mce_result_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_result_record_minor_negative. (exists ff_gap_mdm_lt_mce_result_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_result_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_result_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_result_record_minor_negative ff_column_mdm_prefix_mce_result_record_minor_negative ff_value_mdm_prefix_mce_result_record_minor_negative. (ff_index_mdm_prefix_mce_result_record_minor_negative = (q) * ff_row_mdm_prefix_mce_result_record_minor_negative + ff_column_mdm_prefix_mce_result_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_result_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_result_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_result_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_result_record_minor_negative_cell ff_column_mdm_cell_mce_result_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_result_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_result_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_result_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_result_record_minor_negative_cell = ff_row_mdm_prefix_mce_result_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_result_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_result_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_result_record_minor_negative)) /\ ff_row_mdm_cell_mce_result_record_minor_negative_cell = S ff_row_mdm_prefix_mce_result_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_result_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_result_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_result_record_minor_negative) = (ff_index_mce_family_result)) /\ ff_column_mdm_cell_mce_result_record_minor_negative_cell = ff_column_mdm_prefix_mce_result_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_result_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_result_record_minor_negative_cell_column_after + (ff_index_mce_family_result) = (ff_column_mdm_prefix_mce_result_record_minor_negative)) /\ ff_column_mdm_cell_mce_result_record_minor_negative_cell = S ff_column_mdm_prefix_mce_result_record_minor_negative))) /\ (((exists ff_h_mdm_mce_result_record_minor_negative_cell_source. ff_h_mdm_mce_result_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_result_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_result_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_result_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_result_record_minor_negative_cell_source. nb = ff_q_mdm_mce_result_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_result_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_result_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_result_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_result_record_minor_negative_target. ff_h_mdm_mce_result_record_minor_negative_target + S (ff_value_mdm_prefix_mce_result_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_result_record_minor_negative)) * ff_ut_mce_record_result_record)) /\ exists ff_q_mdm_mce_result_record_minor_negative_target. ff_un_mce_record_result_record = ff_q_mdm_mce_result_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_result_record_minor_negative)) * ff_ut_mce_record_result_record) + (ff_value_mdm_prefix_mce_result_record_minor_negative)))))))))))))

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

55 script commands · 13 reading checkpoints · 4 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 (3)
signed cofactor minor prefix emptysigned cofactor minor record existssigned cofactor minor prefix extend

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 q
02Induction on lL6–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction l
  2. L7
    intro hbound
03Construct an explicit witnessL8–9

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

  1. L8
    exists 0
  2. L9
    exists 0
04Use earlier factsL10–17

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

  1. L10
    specialize signed_cofactor_minor_prefix_empty pb
  2. L11
    specialize signed_cofactor_minor_prefix_empty pc
  3. L12
    specialize signed_cofactor_minor_prefix_empty nb
  4. L13
    specialize signed_cofactor_minor_prefix_empty nc
  5. L14
    specialize signed_cofactor_minor_prefix_empty q
  6. L15
    specialize signed_cofactor_minor_prefix_empty 0
  7. L16
    specialize signed_cofactor_minor_prefix_empty 0
  8. L17
    exact signed_cofactor_minor_prefix_empty
05Fix variables and assumptionsL18–18

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

  1. L18
    intro hbound
06Establish hshortL19–19

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

  1. L19
    have hshort : exists ff_gap_mce_induction_short. ff_gap_mce_induction_short + (l) = (S q)
07Establish hpredecessorL20–28

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

  1. L20
    have hpredecessor : exists gap. gap + l = q
  2. L21
    specialize le_of_succ_le_succ l
  3. L22
    specialize le_of_succ_le_succ q
  4. L23
    apply le_of_succ_le_succ
  5. L24
    exact hbound
  6. L25
    specialize le_succ l
  7. L26
    specialize le_succ q
  8. L27
    apply le_succ
  9. L28
    exact hpredecessor
08Establish hpreviousL29–31

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

  1. L29
    have hprevious : ∃ u. ∃ v. SignedCofactorMinorPrefix(pb,pc,nb,nc,q,u,v,l)Definitions: SignedCofactorMinorPrefixOriginal native command in the exact edition
  2. L30
    apply IH
  3. L31
    exact hshort
09Separate the logical casesL32–33

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

  1. L32
    cases hprevious
  2. L33
    cases hprevious_witness
10Establish hrecordL34–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed cofactor minor record exists.

  1. L34
    have hrecord : ∃ z. SignedMinorRecord(pb,pc,nb,nc,q,l,z)Definitions: SignedMinorRecordOriginal native command in the exact edition
  2. L35
    specialize signed_cofactor_minor_record_exists pb
  3. L36
    specialize signed_cofactor_minor_record_exists pc
  4. L37
    specialize signed_cofactor_minor_record_exists nb
  5. L38
    specialize signed_cofactor_minor_record_exists nc
  6. L39
    specialize signed_cofactor_minor_record_exists q
  7. L40
    specialize signed_cofactor_minor_record_exists l
  8. L41
    apply signed_cofactor_minor_record_exists
  9. L42
    exact hbound
11Separate the logical casesL43–43

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

  1. L43
    cases hrecord
12Use earlier factsL44–53

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

  1. L44
    specialize signed_cofactor_minor_prefix_extend pb
  2. L45
    specialize signed_cofactor_minor_prefix_extend pc
  3. L46
    specialize signed_cofactor_minor_prefix_extend nb
  4. L47
    specialize signed_cofactor_minor_prefix_extend nc
  5. L48
    specialize signed_cofactor_minor_prefix_extend q
  6. L49
    specialize signed_cofactor_minor_prefix_extend x
  7. L50
    specialize signed_cofactor_minor_prefix_extend x1
  8. L51
    specialize signed_cofactor_minor_prefix_extend l
  9. L52
    specialize signed_cofactor_minor_prefix_extend x2
  10. L53
    apply signed_cofactor_minor_prefix_extend
13Use earlier factsL54–55

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

  1. L54
    exact hprevious_witness_witness
  2. L55
    exact hrecord_witness

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro q
  6. 0006induction l
  7. 0007intro hbound
  8. 0008exists 0
  9. 0009exists 0
  10. 0010specialize signed_cofactor_minor_prefix_empty pb
  11. 0011specialize signed_cofactor_minor_prefix_empty pc
  12. 0012specialize signed_cofactor_minor_prefix_empty nb
  13. 0013specialize signed_cofactor_minor_prefix_empty nc
  14. 0014specialize signed_cofactor_minor_prefix_empty q
  15. 0015specialize signed_cofactor_minor_prefix_empty 0
  16. 0016specialize signed_cofactor_minor_prefix_empty 0
  17. 0017exact signed_cofactor_minor_prefix_empty
  18. 0018intro hbound
  19. 0019have hshort : exists ff_gap_mce_induction_short. ff_gap_mce_induction_short + (l) = (S q)
  20. 0020have hpredecessor : exists gap. gap + l = q
  21. 0021specialize le_of_succ_le_succ l
  22. 0022specialize le_of_succ_le_succ q
  23. 0023apply le_of_succ_le_succ
  24. 0024exact hbound
  25. 0025specialize le_succ l
  26. 0026specialize le_succ q
  27. 0027apply le_succ
  28. 0028exact hpredecessor
  29. 0029have hprevious : exists u v. (forall ff_index_mce_family_induction_previous. (exists ff_gap_mce_induction_previous_index. ff_gap_mce_induction_previous_index + S (ff_index_mce_family_induction_previous) = (l)) -> exists ff_value_mce_family_induction_previous. ((((exists ff_h_mce_induction_previous_entry. ff_h_mce_induction_previous_entry + S (ff_value_mce_family_induction_previous) = S ((S (ff_index_mce_family_induction_previous)) * v)) /\ exists ff_q_mce_induction_previous_entry. u = ff_q_mce_induction_previous_entry * S ((S (ff_index_mce_family_induction_previous)) * v) + (ff_value_mce_family_induction_previous))) /\ (exists ff_up_mce_record_induction_previous_record ff_us_mce_record_induction_previous_record ff_un_mce_record_induction_previous_record ff_ut_mce_record_induction_previous_record. ((ff_value_mce_family_induction_previous = ((((ff_up_mce_record_induction_previous_record) + (ff_us_mce_record_induction_previous_record)) * S ((ff_up_mce_record_induction_previous_record) + (ff_us_mce_record_induction_previous_record)) + ((ff_us_mce_record_induction_previous_record) + (ff_us_mce_record_induction_previous_record))) + (((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) * S ((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) + ((ff_ut_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)))) * S ((((ff_up_mce_record_induction_previous_record) + (ff_us_mce_record_induction_previous_record)) * S ((ff_up_mce_record_induction_previous_record) + (ff_us_mce_record_induction_previous_record)) + ((ff_us_mce_record_induction_previous_record) + (ff_us_mce_record_induction_previous_record))) + (((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) * S ((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) + ((ff_ut_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)))) + ((((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) * S ((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) + ((ff_ut_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record))) + (((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) * S ((ff_un_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record)) + ((ff_ut_mce_record_induction_previous_record) + (ff_ut_mce_record_induction_previous_record))))) /\ (((forall ff_index_mdm_prefix_mce_induction_previous_record_minor_positive. (exists ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_induction_previous_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_induction_previous_record_minor_positive ff_column_mdm_prefix_mce_induction_previous_record_minor_positive ff_value_mdm_prefix_mce_induction_previous_record_minor_positive. (ff_index_mdm_prefix_mce_induction_previous_record_minor_positive = (q) * ff_row_mdm_prefix_mce_induction_previous_record_minor_positive + ff_column_mdm_prefix_mce_induction_previous_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_induction_previous_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_induction_previous_record_minor_positive_cell ff_column_mdm_cell_mce_induction_previous_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_induction_previous_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_induction_previous_record_minor_positive_cell = ff_row_mdm_prefix_mce_induction_previous_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_induction_previous_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_induction_previous_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_induction_previous_record_minor_positive)) /\ ff_row_mdm_cell_mce_induction_previous_record_minor_positive_cell = S ff_row_mdm_prefix_mce_induction_previous_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_induction_previous_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_induction_previous_record_minor_positive) = (ff_index_mce_family_induction_previous)) /\ ff_column_mdm_cell_mce_induction_previous_record_minor_positive_cell = ff_column_mdm_prefix_mce_induction_previous_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_induction_previous_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_induction_previous_record_minor_positive_cell_column_after + (ff_index_mce_family_induction_previous) = (ff_column_mdm_prefix_mce_induction_previous_record_minor_positive)) /\ ff_column_mdm_cell_mce_induction_previous_record_minor_positive_cell = S ff_column_mdm_prefix_mce_induction_previous_record_minor_positive))) /\ (((exists ff_h_mdm_mce_induction_previous_record_minor_positive_cell_source. ff_h_mdm_mce_induction_previous_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_induction_previous_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_induction_previous_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_previous_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_induction_previous_record_minor_positive_cell_source. pb = ff_q_mdm_mce_induction_previous_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_induction_previous_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_previous_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_induction_previous_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_induction_previous_record_minor_positive_target. ff_h_mdm_mce_induction_previous_record_minor_positive_target + S (ff_value_mdm_prefix_mce_induction_previous_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_induction_previous_record_minor_positive)) * ff_us_mce_record_induction_previous_record)) /\ exists ff_q_mdm_mce_induction_previous_record_minor_positive_target. ff_up_mce_record_induction_previous_record = ff_q_mdm_mce_induction_previous_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_induction_previous_record_minor_positive)) * ff_us_mce_record_induction_previous_record) + (ff_value_mdm_prefix_mce_induction_previous_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_induction_previous_record_minor_negative. (exists ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_induction_previous_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_induction_previous_record_minor_negative ff_column_mdm_prefix_mce_induction_previous_record_minor_negative ff_value_mdm_prefix_mce_induction_previous_record_minor_negative. (ff_index_mdm_prefix_mce_induction_previous_record_minor_negative = (q) * ff_row_mdm_prefix_mce_induction_previous_record_minor_negative + ff_column_mdm_prefix_mce_induction_previous_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_induction_previous_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_induction_previous_record_minor_negative_cell ff_column_mdm_cell_mce_induction_previous_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_induction_previous_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_induction_previous_record_minor_negative_cell = ff_row_mdm_prefix_mce_induction_previous_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_induction_previous_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_induction_previous_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_induction_previous_record_minor_negative)) /\ ff_row_mdm_cell_mce_induction_previous_record_minor_negative_cell = S ff_row_mdm_prefix_mce_induction_previous_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_induction_previous_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_induction_previous_record_minor_negative) = (ff_index_mce_family_induction_previous)) /\ ff_column_mdm_cell_mce_induction_previous_record_minor_negative_cell = ff_column_mdm_prefix_mce_induction_previous_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_induction_previous_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_induction_previous_record_minor_negative_cell_column_after + (ff_index_mce_family_induction_previous) = (ff_column_mdm_prefix_mce_induction_previous_record_minor_negative)) /\ ff_column_mdm_cell_mce_induction_previous_record_minor_negative_cell = S ff_column_mdm_prefix_mce_induction_previous_record_minor_negative))) /\ (((exists ff_h_mdm_mce_induction_previous_record_minor_negative_cell_source. ff_h_mdm_mce_induction_previous_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_induction_previous_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_induction_previous_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_previous_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_induction_previous_record_minor_negative_cell_source. nb = ff_q_mdm_mce_induction_previous_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_induction_previous_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_previous_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_induction_previous_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_induction_previous_record_minor_negative_target. ff_h_mdm_mce_induction_previous_record_minor_negative_target + S (ff_value_mdm_prefix_mce_induction_previous_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_induction_previous_record_minor_negative)) * ff_ut_mce_record_induction_previous_record)) /\ exists ff_q_mdm_mce_induction_previous_record_minor_negative_target. ff_un_mce_record_induction_previous_record = ff_q_mdm_mce_induction_previous_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_induction_previous_record_minor_negative)) * ff_ut_mce_record_induction_previous_record) + (ff_value_mdm_prefix_mce_induction_previous_record_minor_negative)))))))))))))
  30. 0030apply IH
  31. 0031exact hshort
  32. 0032cases hprevious
  33. 0033cases hprevious_witness
  34. 0034have hrecord : exists z. (exists ff_up_mce_record_induction_record ff_us_mce_record_induction_record ff_un_mce_record_induction_record ff_ut_mce_record_induction_record. ((z = ((((ff_up_mce_record_induction_record) + (ff_us_mce_record_induction_record)) * S ((ff_up_mce_record_induction_record) + (ff_us_mce_record_induction_record)) + ((ff_us_mce_record_induction_record) + (ff_us_mce_record_induction_record))) + (((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) * S ((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) + ((ff_ut_mce_record_induction_record) + (ff_ut_mce_record_induction_record)))) * S ((((ff_up_mce_record_induction_record) + (ff_us_mce_record_induction_record)) * S ((ff_up_mce_record_induction_record) + (ff_us_mce_record_induction_record)) + ((ff_us_mce_record_induction_record) + (ff_us_mce_record_induction_record))) + (((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) * S ((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) + ((ff_ut_mce_record_induction_record) + (ff_ut_mce_record_induction_record)))) + ((((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) * S ((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) + ((ff_ut_mce_record_induction_record) + (ff_ut_mce_record_induction_record))) + (((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) * S ((ff_un_mce_record_induction_record) + (ff_ut_mce_record_induction_record)) + ((ff_ut_mce_record_induction_record) + (ff_ut_mce_record_induction_record))))) /\ (((forall ff_index_mdm_prefix_mce_induction_record_minor_positive. (exists ff_gap_mdm_lt_mce_induction_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_induction_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_induction_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_induction_record_minor_positive ff_column_mdm_prefix_mce_induction_record_minor_positive ff_value_mdm_prefix_mce_induction_record_minor_positive. (ff_index_mdm_prefix_mce_induction_record_minor_positive = (q) * ff_row_mdm_prefix_mce_induction_record_minor_positive + ff_column_mdm_prefix_mce_induction_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_induction_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_induction_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_induction_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_induction_record_minor_positive_cell ff_column_mdm_cell_mce_induction_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_induction_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_induction_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_induction_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_induction_record_minor_positive_cell = ff_row_mdm_prefix_mce_induction_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_induction_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_induction_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_induction_record_minor_positive)) /\ ff_row_mdm_cell_mce_induction_record_minor_positive_cell = S ff_row_mdm_prefix_mce_induction_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_induction_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_induction_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_induction_record_minor_positive) = (l)) /\ ff_column_mdm_cell_mce_induction_record_minor_positive_cell = ff_column_mdm_prefix_mce_induction_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_induction_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_induction_record_minor_positive_cell_column_after + (l) = (ff_column_mdm_prefix_mce_induction_record_minor_positive)) /\ ff_column_mdm_cell_mce_induction_record_minor_positive_cell = S ff_column_mdm_prefix_mce_induction_record_minor_positive))) /\ (((exists ff_h_mdm_mce_induction_record_minor_positive_cell_source. ff_h_mdm_mce_induction_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_induction_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_induction_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_induction_record_minor_positive_cell_source. pb = ff_q_mdm_mce_induction_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_induction_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_induction_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_induction_record_minor_positive_target. ff_h_mdm_mce_induction_record_minor_positive_target + S (ff_value_mdm_prefix_mce_induction_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_induction_record_minor_positive)) * ff_us_mce_record_induction_record)) /\ exists ff_q_mdm_mce_induction_record_minor_positive_target. ff_up_mce_record_induction_record = ff_q_mdm_mce_induction_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_induction_record_minor_positive)) * ff_us_mce_record_induction_record) + (ff_value_mdm_prefix_mce_induction_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_induction_record_minor_negative. (exists ff_gap_mdm_lt_mce_induction_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_induction_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_induction_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_induction_record_minor_negative ff_column_mdm_prefix_mce_induction_record_minor_negative ff_value_mdm_prefix_mce_induction_record_minor_negative. (ff_index_mdm_prefix_mce_induction_record_minor_negative = (q) * ff_row_mdm_prefix_mce_induction_record_minor_negative + ff_column_mdm_prefix_mce_induction_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_induction_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_induction_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_induction_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_induction_record_minor_negative_cell ff_column_mdm_cell_mce_induction_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_induction_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_induction_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_induction_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_induction_record_minor_negative_cell = ff_row_mdm_prefix_mce_induction_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_induction_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_induction_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_induction_record_minor_negative)) /\ ff_row_mdm_cell_mce_induction_record_minor_negative_cell = S ff_row_mdm_prefix_mce_induction_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_induction_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_induction_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_induction_record_minor_negative) = (l)) /\ ff_column_mdm_cell_mce_induction_record_minor_negative_cell = ff_column_mdm_prefix_mce_induction_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_induction_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_induction_record_minor_negative_cell_column_after + (l) = (ff_column_mdm_prefix_mce_induction_record_minor_negative)) /\ ff_column_mdm_cell_mce_induction_record_minor_negative_cell = S ff_column_mdm_prefix_mce_induction_record_minor_negative))) /\ (((exists ff_h_mdm_mce_induction_record_minor_negative_cell_source. ff_h_mdm_mce_induction_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_induction_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_induction_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_induction_record_minor_negative_cell_source. nb = ff_q_mdm_mce_induction_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_induction_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_induction_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_induction_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_induction_record_minor_negative_target. ff_h_mdm_mce_induction_record_minor_negative_target + S (ff_value_mdm_prefix_mce_induction_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_induction_record_minor_negative)) * ff_ut_mce_record_induction_record)) /\ exists ff_q_mdm_mce_induction_record_minor_negative_target. ff_un_mce_record_induction_record = ff_q_mdm_mce_induction_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_induction_record_minor_negative)) * ff_ut_mce_record_induction_record) + (ff_value_mdm_prefix_mce_induction_record_minor_negative)))))))))))
  35. 0035specialize signed_cofactor_minor_record_exists pb
  36. 0036specialize signed_cofactor_minor_record_exists pc
  37. 0037specialize signed_cofactor_minor_record_exists nb
  38. 0038specialize signed_cofactor_minor_record_exists nc
  39. 0039specialize signed_cofactor_minor_record_exists q
  40. 0040specialize signed_cofactor_minor_record_exists l
  41. 0041apply signed_cofactor_minor_record_exists
  42. 0042exact hbound
  43. 0043cases hrecord
  44. 0044specialize signed_cofactor_minor_prefix_extend pb
  45. 0045specialize signed_cofactor_minor_prefix_extend pc
  46. 0046specialize signed_cofactor_minor_prefix_extend nb
  47. 0047specialize signed_cofactor_minor_prefix_extend nc
  48. 0048specialize signed_cofactor_minor_prefix_extend q
  49. 0049specialize signed_cofactor_minor_prefix_extend x
  50. 0050specialize signed_cofactor_minor_prefix_extend x1
  51. 0051specialize signed_cofactor_minor_prefix_extend l
  52. 0052specialize signed_cofactor_minor_prefix_extend x2
  53. 0053apply signed_cofactor_minor_prefix_extend
  54. 0054exact hprevious_witness_witness
  55. 0055exact hrecord_witness