TS000P

finite_prefix_last_occurrence_collision

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

If the last decoded value already occurs, its earlier index and final index form an explicit witnessed collision.

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 b c n v. (((exists ff_h_fpcd_last. ff_h_fpcd_last + S (v) = S ((S (n)) * c)) /\ exists ff_q_fpcd_last. b = ff_q_fpcd_last * S ((S (n)) * c) + (v))) -> (exists fp_i_fpcd_contains. ((exists fp_gap_fpcd_contains_index. fp_gap_fpcd_contains_index + S fp_i_fpcd_contains = n) /\ (((exists ff_h_fpcd_contains_entry. ff_h_fpcd_contains_entry + S (v) = S ((S (fp_i_fpcd_contains)) * c)) /\ exists ff_q_fpcd_contains_entry. b = ff_q_fpcd_contains_entry * S ((S (fp_i_fpcd_contains)) * c) + (v))))) -> (exists ftsp_first_fpcd_next ftsp_second_fpcd_next ftsp_value_fpcd_next. ((exists ftsp_gap_fpcd_next_first. ftsp_gap_fpcd_next_first + S (ftsp_first_fpcd_next) = S n) /\ ((exists ftsp_gap_fpcd_next_second. ftsp_gap_fpcd_next_second + S (ftsp_second_fpcd_next) = S n) /\ (~(ftsp_first_fpcd_next = ftsp_second_fpcd_next) /\ ((((exists ff_h_ftsp_fpcd_next_left. ff_h_ftsp_fpcd_next_left + S (ftsp_value_fpcd_next) = S ((S (ftsp_first_fpcd_next)) * c)) /\ exists ff_q_ftsp_fpcd_next_left. b = ff_q_ftsp_fpcd_next_left * S ((S (ftsp_first_fpcd_next)) * c) + (ftsp_value_fpcd_next))) /\ (((exists ff_h_ftsp_fpcd_next_right. ff_h_ftsp_fpcd_next_right + S (ftsp_value_fpcd_next) = S ((S (ftsp_second_fpcd_next)) * c)) /\ exists ff_q_ftsp_fpcd_next_right. b = ff_q_ftsp_fpcd_next_right * S ((S (ftsp_second_fpcd_next)) * c) + (ftsp_value_fpcd_next))))))))

Constructive proof overview

Generated structural guide

If the last decoded value already occurs, its earlier index and final index form an explicit witnessed collision.

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

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

le_succ Stable theorem; checked-use authorized le_refl Stable theorem; checked-use authorized lt_irrefl_expanded Stable theorem; checked-use authorized

Direct dependents

TS000R finite_prefix_collision_or_injective

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

28 script commands · 13 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro n
  4. L4
    intro v
  5. L5
    intro hlast
  6. L6
    intro hcontains
02Separate the logical casesL7–8

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

  1. L7
    cases hcontains
  2. L8
    cases hcontains_witness
03Construct an explicit witnessL9–11

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

  1. L9
    exists x
  2. L10
    exists n
  3. L11
    exists v
04Separate the logical casesL12–12

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

  1. L12
    split
05Use earlier factsL13–16

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

  1. L13
    specialize le_succ (S x)
  2. L14
    specialize le_succ n
  3. L15
    apply le_succ
  4. L16
    exact hcontains_witness_left
06Separate the logical casesL17–17

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

  1. L17
    split
07Use earlier factsL18–19

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

  1. L18
    specialize le_refl (S n)
  2. L19
    exact le_refl
08Separate the logical casesL20–20

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

  1. L20
    split
09Fix variables and assumptionsL21–21

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

  1. L21
    intro hequal
10Calculate and transport equalitiesL22–22

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

  1. L22
    rewrite hequal at hcontains_witness_left
11Use earlier factsL23–25

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

  1. L23
    specialize lt_irrefl_expanded n
  2. L24
    apply lt_irrefl_expanded
  3. L25
    exact hcontains_witness_left
12Separate the logical casesL26–26

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

  1. L26
    split
13Use earlier factsL27–28

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

  1. L27
    exact hcontains_witness_right
  2. L28
    exact hlast

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro n
  4. 0004intro v
  5. 0005intro hlast
  6. 0006intro hcontains
  7. 0007cases hcontains
  8. 0008cases hcontains_witness
  9. 0009exists x
  10. 0010exists n
  11. 0011exists v
  12. 0012split
  13. 0013specialize le_succ (S x)
  14. 0014specialize le_succ n
  15. 0015apply le_succ
  16. 0016exact hcontains_witness_left
  17. 0017split
  18. 0018specialize le_refl (S n)
  19. 0019exact le_refl
  20. 0020split
  21. 0021intro hequal
  22. 0022rewrite hequal at hcontains_witness_left
  23. 0023specialize lt_irrefl_expanded n
  24. 0024apply lt_irrefl_expanded
  25. 0025exact hcontains_witness_left
  26. 0026split
  27. 0027exact hcontains_witness_right
  28. 0028exact hlast