CE000B

signed_cofactor_minor_family_entry_projects_minor

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

Every decoded member of the complete first-row cofactor family is a genuine independently encoded signed matrix minor.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall pb pc nb nc q u v j. (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_gap_mce_record_column. ff_gap_mce_record_column + S (j) = (S q)) -> exists up us un ut. (((forall ff_index_mdm_prefix_mce_record_projection_positive. (exists ff_gap_mdm_lt_mce_record_projection_positive_index_bound. ff_gap_mdm_lt_mce_record_projection_positive_index_bound + S (ff_index_mdm_prefix_mce_record_projection_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_record_projection_positive ff_column_mdm_prefix_mce_record_projection_positive ff_value_mdm_prefix_mce_record_projection_positive. (ff_index_mdm_prefix_mce_record_projection_positive = (q) * ff_row_mdm_prefix_mce_record_projection_positive + ff_column_mdm_prefix_mce_record_projection_positive /\ ((exists ff_gap_mdm_lt_mce_record_projection_positive_column_bound. ff_gap_mdm_lt_mce_record_projection_positive_column_bound + S (ff_column_mdm_prefix_mce_record_projection_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_record_projection_positive_cell ff_column_mdm_cell_mce_record_projection_positive_cell. (((((exists ff_gap_mdm_lt_mce_record_projection_positive_cell_row_before. ff_gap_mdm_lt_mce_record_projection_positive_cell_row_before + S (ff_row_mdm_prefix_mce_record_projection_positive) = (0)) /\ ff_row_mdm_cell_mce_record_projection_positive_cell = ff_row_mdm_prefix_mce_record_projection_positive) \/ ((exists ff_gap_mdm_le_mce_record_projection_positive_cell_row_after. ff_gap_mdm_le_mce_record_projection_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_record_projection_positive)) /\ ff_row_mdm_cell_mce_record_projection_positive_cell = S ff_row_mdm_prefix_mce_record_projection_positive))) /\ (((((exists ff_gap_mdm_lt_mce_record_projection_positive_cell_column_before. ff_gap_mdm_lt_mce_record_projection_positive_cell_column_before + S (ff_column_mdm_prefix_mce_record_projection_positive) = (j)) /\ ff_column_mdm_cell_mce_record_projection_positive_cell = ff_column_mdm_prefix_mce_record_projection_positive) \/ ((exists ff_gap_mdm_le_mce_record_projection_positive_cell_column_after. ff_gap_mdm_le_mce_record_projection_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mce_record_projection_positive)) /\ ff_column_mdm_cell_mce_record_projection_positive_cell = S ff_column_mdm_prefix_mce_record_projection_positive))) /\ (((exists ff_h_mdm_mce_record_projection_positive_cell_source. ff_h_mdm_mce_record_projection_positive_cell_source + S (ff_value_mdm_prefix_mce_record_projection_positive) = S ((S ((ff_row_mdm_cell_mce_record_projection_positive_cell) * (S q) + (ff_column_mdm_cell_mce_record_projection_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_record_projection_positive_cell_source. pb = ff_q_mdm_mce_record_projection_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_record_projection_positive_cell) * (S q) + (ff_column_mdm_cell_mce_record_projection_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_record_projection_positive)))))) /\ (((exists ff_h_mdm_mce_record_projection_positive_target. ff_h_mdm_mce_record_projection_positive_target + S (ff_value_mdm_prefix_mce_record_projection_positive) = S ((S (ff_index_mdm_prefix_mce_record_projection_positive)) * us)) /\ exists ff_q_mdm_mce_record_projection_positive_target. up = ff_q_mdm_mce_record_projection_positive_target * S ((S (ff_index_mdm_prefix_mce_record_projection_positive)) * us) + (ff_value_mdm_prefix_mce_record_projection_positive))))))) /\ (forall ff_index_mdm_prefix_mce_record_projection_negative. (exists ff_gap_mdm_lt_mce_record_projection_negative_index_bound. ff_gap_mdm_lt_mce_record_projection_negative_index_bound + S (ff_index_mdm_prefix_mce_record_projection_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_record_projection_negative ff_column_mdm_prefix_mce_record_projection_negative ff_value_mdm_prefix_mce_record_projection_negative. (ff_index_mdm_prefix_mce_record_projection_negative = (q) * ff_row_mdm_prefix_mce_record_projection_negative + ff_column_mdm_prefix_mce_record_projection_negative /\ ((exists ff_gap_mdm_lt_mce_record_projection_negative_column_bound. ff_gap_mdm_lt_mce_record_projection_negative_column_bound + S (ff_column_mdm_prefix_mce_record_projection_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_record_projection_negative_cell ff_column_mdm_cell_mce_record_projection_negative_cell. (((((exists ff_gap_mdm_lt_mce_record_projection_negative_cell_row_before. ff_gap_mdm_lt_mce_record_projection_negative_cell_row_before + S (ff_row_mdm_prefix_mce_record_projection_negative) = (0)) /\ ff_row_mdm_cell_mce_record_projection_negative_cell = ff_row_mdm_prefix_mce_record_projection_negative) \/ ((exists ff_gap_mdm_le_mce_record_projection_negative_cell_row_after. ff_gap_mdm_le_mce_record_projection_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_record_projection_negative)) /\ ff_row_mdm_cell_mce_record_projection_negative_cell = S ff_row_mdm_prefix_mce_record_projection_negative))) /\ (((((exists ff_gap_mdm_lt_mce_record_projection_negative_cell_column_before. ff_gap_mdm_lt_mce_record_projection_negative_cell_column_before + S (ff_column_mdm_prefix_mce_record_projection_negative) = (j)) /\ ff_column_mdm_cell_mce_record_projection_negative_cell = ff_column_mdm_prefix_mce_record_projection_negative) \/ ((exists ff_gap_mdm_le_mce_record_projection_negative_cell_column_after. ff_gap_mdm_le_mce_record_projection_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mce_record_projection_negative)) /\ ff_column_mdm_cell_mce_record_projection_negative_cell = S ff_column_mdm_prefix_mce_record_projection_negative))) /\ (((exists ff_h_mdm_mce_record_projection_negative_cell_source. ff_h_mdm_mce_record_projection_negative_cell_source + S (ff_value_mdm_prefix_mce_record_projection_negative) = S ((S ((ff_row_mdm_cell_mce_record_projection_negative_cell) * (S q) + (ff_column_mdm_cell_mce_record_projection_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_record_projection_negative_cell_source. nb = ff_q_mdm_mce_record_projection_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_record_projection_negative_cell) * (S q) + (ff_column_mdm_cell_mce_record_projection_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_record_projection_negative)))))) /\ (((exists ff_h_mdm_mce_record_projection_negative_target. ff_h_mdm_mce_record_projection_negative_target + S (ff_value_mdm_prefix_mce_record_projection_negative) = S ((S (ff_index_mdm_prefix_mce_record_projection_negative)) * ut)) /\ exists ff_q_mdm_mce_record_projection_negative_target. un = ff_q_mdm_mce_record_projection_negative_target * S ((S (ff_index_mdm_prefix_mce_record_projection_negative)) * ut) + (ff_value_mdm_prefix_mce_record_projection_negative)))))))))

Constructive proof overview

Generated structural guide

Every decoded member of the complete first-row cofactor family is a genuine independently encoded signed matrix minor.

The unchanged tactic script uses 2 declared prerequisites and contains 33 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CE000A signed_cofactor_minor_family_entry_exists CE0005 signed_cofactor_minor_record_projects_minor

Direct dependents

none

Formal native tactic body

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

Read the argument

Proof checkpoints

33 script commands · 5 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
signed cofactor minor family entry existssigned cofactor minor record projects minor

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 j
  9. L9
    intro hfamily
  10. L10
    intro hbound
02Establish hentryL11–20

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

  1. L11
    have hentry : ∃ z. Beta(u,v,j,z) ∧ SignedMinorRecord(pb,pc,nb,nc,q,j,z)Definitions: BetaSignedMinorRecord
  2. L12
    specialize signed_cofactor_minor_family_entry_exists pb
  3. L13
    specialize signed_cofactor_minor_family_entry_exists pc
  4. L14
    specialize signed_cofactor_minor_family_entry_exists nb
  5. L15
    specialize signed_cofactor_minor_family_entry_exists nc
  6. L16
    specialize signed_cofactor_minor_family_entry_exists q
  7. L17
    specialize signed_cofactor_minor_family_entry_exists u
  8. L18
    specialize signed_cofactor_minor_family_entry_exists v
  9. L19
    specialize signed_cofactor_minor_family_entry_exists j
  10. L20
    apply signed_cofactor_minor_family_entry_exists
03Use earlier factsL21–22

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

  1. L21
    exact hfamily
  2. L22
    exact hbound
04Separate the logical casesL23–24

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

  1. L23
    cases hentry
  2. L24
    cases hentry_witness
05Use earlier factsL25–33

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

  1. L25
    specialize signed_cofactor_minor_record_projects_minor pb
  2. L26
    specialize signed_cofactor_minor_record_projects_minor pc
  3. L27
    specialize signed_cofactor_minor_record_projects_minor nb
  4. L28
    specialize signed_cofactor_minor_record_projects_minor nc
  5. L29
    specialize signed_cofactor_minor_record_projects_minor q
  6. L30
    specialize signed_cofactor_minor_record_projects_minor j
  7. L31
    specialize signed_cofactor_minor_record_projects_minor x
  8. L32
    apply signed_cofactor_minor_record_projects_minor
  9. L33
    exact hentry_witness_right

Library-wide reading audit

Original exact command ledger · 33 lines
  1. 0001intro pb
  2. 0002intro pc
  3. 0003intro nb
  4. 0004intro nc
  5. 0005intro q
  6. 0006intro u
  7. 0007intro v
  8. 0008intro j
  9. 0009intro hfamily
  10. 0010intro hbound
  11. 0011have hentry : exists z. ((((exists ff_h_mce_project_entry. ff_h_mce_project_entry + S (z) = S ((S (j)) * v)) /\ exists ff_q_mce_project_entry. u = ff_q_mce_project_entry * S ((S (j)) * v) + (z))) /\ (exists ff_up_mce_record_project_record ff_us_mce_record_project_record ff_un_mce_record_project_record ff_ut_mce_record_project_record. ((z = ((((ff_up_mce_record_project_record) + (ff_us_mce_record_project_record)) * S ((ff_up_mce_record_project_record) + (ff_us_mce_record_project_record)) + ((ff_us_mce_record_project_record) + (ff_us_mce_record_project_record))) + (((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) * S ((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) + ((ff_ut_mce_record_project_record) + (ff_ut_mce_record_project_record)))) * S ((((ff_up_mce_record_project_record) + (ff_us_mce_record_project_record)) * S ((ff_up_mce_record_project_record) + (ff_us_mce_record_project_record)) + ((ff_us_mce_record_project_record) + (ff_us_mce_record_project_record))) + (((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) * S ((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) + ((ff_ut_mce_record_project_record) + (ff_ut_mce_record_project_record)))) + ((((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) * S ((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) + ((ff_ut_mce_record_project_record) + (ff_ut_mce_record_project_record))) + (((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) * S ((ff_un_mce_record_project_record) + (ff_ut_mce_record_project_record)) + ((ff_ut_mce_record_project_record) + (ff_ut_mce_record_project_record))))) /\ (((forall ff_index_mdm_prefix_mce_project_record_minor_positive. (exists ff_gap_mdm_lt_mce_project_record_minor_positive_index_bound. ff_gap_mdm_lt_mce_project_record_minor_positive_index_bound + S (ff_index_mdm_prefix_mce_project_record_minor_positive) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_project_record_minor_positive ff_column_mdm_prefix_mce_project_record_minor_positive ff_value_mdm_prefix_mce_project_record_minor_positive. (ff_index_mdm_prefix_mce_project_record_minor_positive = (q) * ff_row_mdm_prefix_mce_project_record_minor_positive + ff_column_mdm_prefix_mce_project_record_minor_positive /\ ((exists ff_gap_mdm_lt_mce_project_record_minor_positive_column_bound. ff_gap_mdm_lt_mce_project_record_minor_positive_column_bound + S (ff_column_mdm_prefix_mce_project_record_minor_positive) = (q)) /\ ((exists ff_row_mdm_cell_mce_project_record_minor_positive_cell ff_column_mdm_cell_mce_project_record_minor_positive_cell. (((((exists ff_gap_mdm_lt_mce_project_record_minor_positive_cell_row_before. ff_gap_mdm_lt_mce_project_record_minor_positive_cell_row_before + S (ff_row_mdm_prefix_mce_project_record_minor_positive) = (0)) /\ ff_row_mdm_cell_mce_project_record_minor_positive_cell = ff_row_mdm_prefix_mce_project_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_project_record_minor_positive_cell_row_after. ff_gap_mdm_le_mce_project_record_minor_positive_cell_row_after + (0) = (ff_row_mdm_prefix_mce_project_record_minor_positive)) /\ ff_row_mdm_cell_mce_project_record_minor_positive_cell = S ff_row_mdm_prefix_mce_project_record_minor_positive))) /\ (((((exists ff_gap_mdm_lt_mce_project_record_minor_positive_cell_column_before. ff_gap_mdm_lt_mce_project_record_minor_positive_cell_column_before + S (ff_column_mdm_prefix_mce_project_record_minor_positive) = (j)) /\ ff_column_mdm_cell_mce_project_record_minor_positive_cell = ff_column_mdm_prefix_mce_project_record_minor_positive) \/ ((exists ff_gap_mdm_le_mce_project_record_minor_positive_cell_column_after. ff_gap_mdm_le_mce_project_record_minor_positive_cell_column_after + (j) = (ff_column_mdm_prefix_mce_project_record_minor_positive)) /\ ff_column_mdm_cell_mce_project_record_minor_positive_cell = S ff_column_mdm_prefix_mce_project_record_minor_positive))) /\ (((exists ff_h_mdm_mce_project_record_minor_positive_cell_source. ff_h_mdm_mce_project_record_minor_positive_cell_source + S (ff_value_mdm_prefix_mce_project_record_minor_positive) = S ((S ((ff_row_mdm_cell_mce_project_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_project_record_minor_positive_cell))) * pc)) /\ exists ff_q_mdm_mce_project_record_minor_positive_cell_source. pb = ff_q_mdm_mce_project_record_minor_positive_cell_source * S ((S ((ff_row_mdm_cell_mce_project_record_minor_positive_cell) * (S (q)) + (ff_column_mdm_cell_mce_project_record_minor_positive_cell))) * pc) + (ff_value_mdm_prefix_mce_project_record_minor_positive)))))) /\ (((exists ff_h_mdm_mce_project_record_minor_positive_target. ff_h_mdm_mce_project_record_minor_positive_target + S (ff_value_mdm_prefix_mce_project_record_minor_positive) = S ((S (ff_index_mdm_prefix_mce_project_record_minor_positive)) * ff_us_mce_record_project_record)) /\ exists ff_q_mdm_mce_project_record_minor_positive_target. ff_up_mce_record_project_record = ff_q_mdm_mce_project_record_minor_positive_target * S ((S (ff_index_mdm_prefix_mce_project_record_minor_positive)) * ff_us_mce_record_project_record) + (ff_value_mdm_prefix_mce_project_record_minor_positive))))))) /\ (forall ff_index_mdm_prefix_mce_project_record_minor_negative. (exists ff_gap_mdm_lt_mce_project_record_minor_negative_index_bound. ff_gap_mdm_lt_mce_project_record_minor_negative_index_bound + S (ff_index_mdm_prefix_mce_project_record_minor_negative) = ((q) * (q))) -> exists ff_row_mdm_prefix_mce_project_record_minor_negative ff_column_mdm_prefix_mce_project_record_minor_negative ff_value_mdm_prefix_mce_project_record_minor_negative. (ff_index_mdm_prefix_mce_project_record_minor_negative = (q) * ff_row_mdm_prefix_mce_project_record_minor_negative + ff_column_mdm_prefix_mce_project_record_minor_negative /\ ((exists ff_gap_mdm_lt_mce_project_record_minor_negative_column_bound. ff_gap_mdm_lt_mce_project_record_minor_negative_column_bound + S (ff_column_mdm_prefix_mce_project_record_minor_negative) = (q)) /\ ((exists ff_row_mdm_cell_mce_project_record_minor_negative_cell ff_column_mdm_cell_mce_project_record_minor_negative_cell. (((((exists ff_gap_mdm_lt_mce_project_record_minor_negative_cell_row_before. ff_gap_mdm_lt_mce_project_record_minor_negative_cell_row_before + S (ff_row_mdm_prefix_mce_project_record_minor_negative) = (0)) /\ ff_row_mdm_cell_mce_project_record_minor_negative_cell = ff_row_mdm_prefix_mce_project_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_project_record_minor_negative_cell_row_after. ff_gap_mdm_le_mce_project_record_minor_negative_cell_row_after + (0) = (ff_row_mdm_prefix_mce_project_record_minor_negative)) /\ ff_row_mdm_cell_mce_project_record_minor_negative_cell = S ff_row_mdm_prefix_mce_project_record_minor_negative))) /\ (((((exists ff_gap_mdm_lt_mce_project_record_minor_negative_cell_column_before. ff_gap_mdm_lt_mce_project_record_minor_negative_cell_column_before + S (ff_column_mdm_prefix_mce_project_record_minor_negative) = (j)) /\ ff_column_mdm_cell_mce_project_record_minor_negative_cell = ff_column_mdm_prefix_mce_project_record_minor_negative) \/ ((exists ff_gap_mdm_le_mce_project_record_minor_negative_cell_column_after. ff_gap_mdm_le_mce_project_record_minor_negative_cell_column_after + (j) = (ff_column_mdm_prefix_mce_project_record_minor_negative)) /\ ff_column_mdm_cell_mce_project_record_minor_negative_cell = S ff_column_mdm_prefix_mce_project_record_minor_negative))) /\ (((exists ff_h_mdm_mce_project_record_minor_negative_cell_source. ff_h_mdm_mce_project_record_minor_negative_cell_source + S (ff_value_mdm_prefix_mce_project_record_minor_negative) = S ((S ((ff_row_mdm_cell_mce_project_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_project_record_minor_negative_cell))) * nc)) /\ exists ff_q_mdm_mce_project_record_minor_negative_cell_source. nb = ff_q_mdm_mce_project_record_minor_negative_cell_source * S ((S ((ff_row_mdm_cell_mce_project_record_minor_negative_cell) * (S (q)) + (ff_column_mdm_cell_mce_project_record_minor_negative_cell))) * nc) + (ff_value_mdm_prefix_mce_project_record_minor_negative)))))) /\ (((exists ff_h_mdm_mce_project_record_minor_negative_target. ff_h_mdm_mce_project_record_minor_negative_target + S (ff_value_mdm_prefix_mce_project_record_minor_negative) = S ((S (ff_index_mdm_prefix_mce_project_record_minor_negative)) * ff_ut_mce_record_project_record)) /\ exists ff_q_mdm_mce_project_record_minor_negative_target. ff_un_mce_record_project_record = ff_q_mdm_mce_project_record_minor_negative_target * S ((S (ff_index_mdm_prefix_mce_project_record_minor_negative)) * ff_ut_mce_record_project_record) + (ff_value_mdm_prefix_mce_project_record_minor_negative))))))))))))
  12. 0012specialize signed_cofactor_minor_family_entry_exists pb
  13. 0013specialize signed_cofactor_minor_family_entry_exists pc
  14. 0014specialize signed_cofactor_minor_family_entry_exists nb
  15. 0015specialize signed_cofactor_minor_family_entry_exists nc
  16. 0016specialize signed_cofactor_minor_family_entry_exists q
  17. 0017specialize signed_cofactor_minor_family_entry_exists u
  18. 0018specialize signed_cofactor_minor_family_entry_exists v
  19. 0019specialize signed_cofactor_minor_family_entry_exists j
  20. 0020apply signed_cofactor_minor_family_entry_exists
  21. 0021exact hfamily
  22. 0022exact hbound
  23. 0023cases hentry
  24. 0024cases hentry_witness
  25. 0025specialize signed_cofactor_minor_record_projects_minor pb
  26. 0026specialize signed_cofactor_minor_record_projects_minor pc
  27. 0027specialize signed_cofactor_minor_record_projects_minor nb
  28. 0028specialize signed_cofactor_minor_record_projects_minor nc
  29. 0029specialize signed_cofactor_minor_record_projects_minor q
  30. 0030specialize signed_cofactor_minor_record_projects_minor j
  31. 0031specialize signed_cofactor_minor_record_projects_minor x
  32. 0032apply signed_cofactor_minor_record_projects_minor
  33. 0033exact hentry_witness_right

Separate complete second-wave branches: Full T13 proof · Alpha v27.