TS000P · theorem body

finite_prefix_last_occurrence_collision

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

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

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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.

Statement with defined notation

∀ b. ∀ c. ∀ n. ∀ v. BetaAt(b,c,n,v) → ContainsPrefix(b,c,n,v) → ∃ x. ∃ y. ∃ z. Lt(x,S n) ∧ (Lt(y,S n) ∧ (¬x = y ∧ (BetaAt(b,c,x,z) ∧ BetaAt(b,c,y,z))))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt PD0027 ContainsPrefix

In local proof propositions

none
Exact expanded first-order 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))))))))

Proof neighborhood

Direct theorem prerequisites

le_succ · Stable closed le_refl · Stable closed lt_irrefl_expanded · Stable closed

Direct theorem dependents

TS000R finite_prefix_collision_or_injective

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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