TS000R

finite_prefix_collision_or_injective

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 7 declared prerequisites and contains 60 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

Proof neighborhood

Direct dependencies

add_eq_zero_right Stable theorem; checked-use authorized succ_ne_zero Stable theorem; checked-use authorized TS000O finite_prefix_collision_succ beta_at_exists Stable theorem; checked-use authorized finite_contains_decidable Stable theorem; checked-use authorized TS000P finite_prefix_last_occurrence_collision TS000Q finite_prefix_injective_extend_fresh

Direct dependents

TS000S finite_bounded_into_oversized_collision

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

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.

Named ingredients (3)
finite prefix collision succfinite prefix last occurrence collisionfinite prefix injective extend fresh

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–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 : 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)))
  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
  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 exact 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 : 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 : ((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