TS000R · theorem body

finite_prefix_collision_or_injective

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

Every finite beta-coded prefix constructively yields either explicit distinct equal-value indices or a proof of injectivity.

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. ∀ l. (∃ x. ∃ y. ∃ z. Lt(x,l) ∧ (Lt(y,l) ∧ (¬x = y ∧ (BetaAt(b,c,x,z) ∧ BetaAt(b,c,y,z))))) ∨ InjectivePrefix(b,c,l)

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 PD0025 InjectivePrefix

In local proof propositions

PD0013 BetaAt PD0027 ContainsPrefix
Exact expanded first-order statement
forall b c l. ((exists ftsp_first_fpcd_generic ftsp_second_fpcd_generic ftsp_value_fpcd_generic. ((exists ftsp_gap_fpcd_generic_first. ftsp_gap_fpcd_generic_first + S (ftsp_first_fpcd_generic) = l) /\ ((exists ftsp_gap_fpcd_generic_second. ftsp_gap_fpcd_generic_second + S (ftsp_second_fpcd_generic) = l) /\ (~(ftsp_first_fpcd_generic = ftsp_second_fpcd_generic) /\ ((((exists ff_h_ftsp_fpcd_generic_left. ff_h_ftsp_fpcd_generic_left + S (ftsp_value_fpcd_generic) = S ((S (ftsp_first_fpcd_generic)) * c)) /\ exists ff_q_ftsp_fpcd_generic_left. b = ff_q_ftsp_fpcd_generic_left * S ((S (ftsp_first_fpcd_generic)) * c) + (ftsp_value_fpcd_generic))) /\ (((exists ff_h_ftsp_fpcd_generic_right. ff_h_ftsp_fpcd_generic_right + S (ftsp_value_fpcd_generic) = S ((S (ftsp_second_fpcd_generic)) * c)) /\ exists ff_q_ftsp_fpcd_generic_right. b = ff_q_ftsp_fpcd_generic_right * S ((S (ftsp_second_fpcd_generic)) * c) + (ftsp_value_fpcd_generic)))))))) \/ (forall fp_i_fpcd_generic fp_j_fpcd_generic fp_value_fpcd_generic. (exists fp_gap_fpcd_generic_i. fp_gap_fpcd_generic_i + S fp_i_fpcd_generic = l) -> (exists fp_gap_fpcd_generic_j. fp_gap_fpcd_generic_j + S fp_j_fpcd_generic = l) -> (((exists ff_h_fpcd_generic_left. ff_h_fpcd_generic_left + S (fp_value_fpcd_generic) = S ((S (fp_i_fpcd_generic)) * c)) /\ exists ff_q_fpcd_generic_left. b = ff_q_fpcd_generic_left * S ((S (fp_i_fpcd_generic)) * c) + (fp_value_fpcd_generic))) -> (((exists ff_h_fpcd_generic_right. ff_h_fpcd_generic_right + S (fp_value_fpcd_generic) = S ((S (fp_j_fpcd_generic)) * c)) /\ exists ff_q_fpcd_generic_right. b = ff_q_fpcd_generic_right * S ((S (fp_j_fpcd_generic)) * c) + (fp_value_fpcd_generic))) -> fp_i_fpcd_generic = fp_j_fpcd_generic))

Proof neighborhood

Direct theorem prerequisites

add_eq_zero_right · Stable closed succ_ne_zero · Stable closed TS000O finite_prefix_collision_succ beta_at_exists · Stable closed finite_contains_decidable · Stable closed TS000P finite_prefix_last_occurrence_collision TS000Q finite_prefix_injective_extend_fresh

Direct theorem dependents

TS000S finite_bounded_into_oversized_collision

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

60 script commands · 17 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.

Named ingredients (3)
finite prefix collision succfinite prefix last occurrence collisionfinite prefix injective extend fresh
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–3

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

  1. L3
    induction l
03Separate the logical casesL4–4

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

  1. L4
    right
04Fix variables and assumptionsL5–11

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

  1. L5
    intro i
  2. L6
    intro j
  3. L7
    intro v
  4. L8
    intro hibound
  5. L9
    intro hjbound
  6. L10
    intro hleft
  7. L11
    intro hright
05Separate the logical casesL12–13

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

  1. L12
    exfalso
  2. L13
    cases hibound
06Establish hzeroL14–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L14
    have hzero : S i = 0
  2. L15
    specialize add_eq_zero_right x
  3. L16
    specialize add_eq_zero_right (S i)
  4. L17
    apply add_eq_zero_right
  5. L18
    exact hibound_witness
  6. L19
    specialize succ_ne_zero i
  7. L20
    apply succ_ne_zero
  8. L21
    exact hzero
07Separate the logical casesL22–23

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

  1. L22
    cases IH
  2. L23
    left
08Use earlier factsL24–28

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

  1. L24
    specialize finite_prefix_collision_succ b
  2. L25
    specialize finite_prefix_collision_succ c
  3. L26
    specialize finite_prefix_collision_succ l
  4. L27
    apply finite_prefix_collision_succ
  5. L28
    exact IH_left
09Establish hlastL29–33

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

  1. L29
    have hlast : ∃ v. BetaAt(b,c,l,v)Definitions: BetaAt(b,c,l,v)Original native command in the exact edition
  2. L30
    specialize beta_at_exists b
  3. L31
    specialize beta_at_exists c
  4. L32
    specialize beta_at_exists l
  5. L33
    exact beta_at_exists
10Separate the logical casesL34–34

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

  1. L34
    cases hlast
11Establish hcontainsL35–40

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

  1. L35
    have hcontains : ContainsPrefix(b,c,l,x) ∨ ¬ContainsPrefix(b,c,l,x)Definitions: ContainsPrefix(b,c,l,x)Original native command in the exact edition
  2. L36
    specialize finite_contains_decidable b
  3. L37
    specialize finite_contains_decidable c
  4. L38
    specialize finite_contains_decidable l
  5. L39
    specialize finite_contains_decidable x
  6. L40
    exact finite_contains_decidable
12Separate the logical casesL41–42

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

  1. L41
    cases hcontains
  2. L42
    left
13Use earlier factsL43–49

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

  1. L43
    specialize finite_prefix_last_occurrence_collision b
  2. L44
    specialize finite_prefix_last_occurrence_collision c
  3. L45
    specialize finite_prefix_last_occurrence_collision l
  4. L46
    specialize finite_prefix_last_occurrence_collision x
  5. L47
    apply finite_prefix_last_occurrence_collision
  6. L48
    exact hlast_witness
  7. L49
    exact hcontains_left
14Separate the logical casesL50–50

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

  1. L50
    right
15Use earlier factsL51–57

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

  1. L51
    specialize finite_prefix_injective_extend_fresh b
  2. L52
    specialize finite_prefix_injective_extend_fresh c
  3. L53
    specialize finite_prefix_injective_extend_fresh l
  4. L54
    specialize finite_prefix_injective_extend_fresh x
  5. L55
    apply finite_prefix_injective_extend_fresh
  6. L56
    exact IH_right
  7. L57
    exact hlast_witness
16Fix variables and assumptionsL58–58

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

  1. L58
    intro hoccurs
17Use earlier factsL59–60

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

  1. L59
    apply hcontains_right
  2. L60
    exact hoccurs

Library-wide reading audit

Original defined command ledger · 60 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004right
  5. 0005intro i
  6. 0006intro j
  7. 0007intro v
  8. 0008intro hibound
  9. 0009intro hjbound
  10. 0010intro hleft
  11. 0011intro hright
  12. 0012exfalso
  13. 0013cases hibound
  14. 0014have hzero : S i = 0
  15. 0015specialize add_eq_zero_right x
  16. 0016specialize add_eq_zero_right (S i)
  17. 0017apply add_eq_zero_right
  18. 0018exact hibound_witness
  19. 0019specialize succ_ne_zero i
  20. 0020apply succ_ne_zero
  21. 0021exact hzero
  22. 0022cases IH
  23. 0023left
  24. 0024specialize finite_prefix_collision_succ b
  25. 0025specialize finite_prefix_collision_succ c
  26. 0026specialize finite_prefix_collision_succ l
  27. 0027apply finite_prefix_collision_succ
  28. 0028exact IH_left
  29. 0029have hlast : ∃ v. BetaAt(b,c,l,v)
    Exact native replay linehave hlast : exists v. (((exists ff_h_fpcd_induction_last. ff_h_fpcd_induction_last + S (v) = S ((S (l)) * c)) /\ exists ff_q_fpcd_induction_last. b = ff_q_fpcd_induction_last * S ((S (l)) * c) + (v)))
  30. 0030specialize beta_at_exists b
  31. 0031specialize beta_at_exists c
  32. 0032specialize beta_at_exists l
  33. 0033exact beta_at_exists
  34. 0034cases hlast
  35. 0035have hcontains : ContainsPrefix(b,c,l,x) ∨ ¬ContainsPrefix(b,c,l,x)
    Exact native replay linehave hcontains : ((exists fp_i_fpcd_induction_contains. ((exists fp_gap_fpcd_induction_contains_index. fp_gap_fpcd_induction_contains_index + S fp_i_fpcd_induction_contains = l) /\ (((exists ff_h_fpcd_induction_contains_entry. ff_h_fpcd_induction_contains_entry + S (x) = S ((S (fp_i_fpcd_induction_contains)) * c)) /\ exists ff_q_fpcd_induction_contains_entry. b = ff_q_fpcd_induction_contains_entry * S ((S (fp_i_fpcd_induction_contains)) * c) + (x))))) \/ ~(exists fp_i_fpcd_induction_contains. ((exists fp_gap_fpcd_induction_contains_index. fp_gap_fpcd_induction_contains_index + S fp_i_fpcd_induction_contains = l) /\ (((exists ff_h_fpcd_induction_contains_entry. ff_h_fpcd_induction_contains_entry + S (x) = S ((S (fp_i_fpcd_induction_contains)) * c)) /\ exists ff_q_fpcd_induction_contains_entry. b = ff_q_fpcd_induction_contains_entry * S ((S (fp_i_fpcd_induction_contains)) * c) + (x))))))
  36. 0036specialize finite_contains_decidable b
  37. 0037specialize finite_contains_decidable c
  38. 0038specialize finite_contains_decidable l
  39. 0039specialize finite_contains_decidable x
  40. 0040exact finite_contains_decidable
  41. 0041cases hcontains
  42. 0042left
  43. 0043specialize finite_prefix_last_occurrence_collision b
  44. 0044specialize finite_prefix_last_occurrence_collision c
  45. 0045specialize finite_prefix_last_occurrence_collision l
  46. 0046specialize finite_prefix_last_occurrence_collision x
  47. 0047apply finite_prefix_last_occurrence_collision
  48. 0048exact hlast_witness
  49. 0049exact hcontains_left
  50. 0050right
  51. 0051specialize finite_prefix_injective_extend_fresh b
  52. 0052specialize finite_prefix_injective_extend_fresh c
  53. 0053specialize finite_prefix_injective_extend_fresh l
  54. 0054specialize finite_prefix_injective_extend_fresh x
  55. 0055apply finite_prefix_injective_extend_fresh
  56. 0056exact IH_right
  57. 0057exact hlast_witness
  58. 0058intro hoccurs
  59. 0059apply hcontains_right
  60. 0060exact hoccurs