PA004H

finite_contains_decidable

Stable checked-use theorem · independently closed

Occurrence of a value in a nonempty decoded prefix is constructively decidable.

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 PA statement

forall b c l y. ((exists fp_i_contains_l. ((exists fp_gap_contains_l_index. fp_gap_contains_l_index + S fp_i_contains_l = l) /\ (((exists ff_h_contains_l_entry. ff_h_contains_l_entry + S (y) = S ((S (fp_i_contains_l)) * c)) /\ exists ff_q_contains_l_entry. b = ff_q_contains_l_entry * S ((S (fp_i_contains_l)) * c) + (y))))) \/ ~(exists fp_i_contains_l. ((exists fp_gap_contains_l_index. fp_gap_contains_l_index + S fp_i_contains_l = l) /\ (((exists ff_h_contains_l_entry. ff_h_contains_l_entry + S (y) = S ((S (fp_i_contains_l)) * c)) /\ exists ff_q_contains_l_entry. b = ff_q_contains_l_entry * S ((S (fp_i_contains_l)) * c) + (y))))))

Structural proof guide

Generated structural guide

Occurrence of a value in a nonempty decoded prefix is constructively decidable.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, finite_lt_succ_eq_or_lt, beta_at_exists, beta_at_unique, eq_decidable, le_refl, le_succ as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (11), intermediate claims (5), equality transport (4).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique PA004G eq_decidable PA001A le_refl PA002O le_succ

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique PA004G eq_decidable PA001A le_refl PA002O le_succ

Direct dependents

PA004W finite_bounded_injective_surjective PA0092 finite_covers_into_or_omits

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

77 script commands · 30 reading checkpoints · 5 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 (8)
add eq zero rightsucc ne zerofinite lt succ eq or ltbeta at existsbeta at uniqueeq decidablele reflle succ
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–4

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

  1. L3
    induction l
  2. L4
    intro y
03Separate the logical casesL5–5

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

  1. L5
    right
04Fix variables and assumptionsL6–6

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

  1. L6
    intro hcontains
05Separate the logical casesL7–9

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

  1. L7
    cases hcontains
  2. L8
    cases hcontains_witness
  3. L9
    cases hcontains_witness_left
06Establish hsiL10–18

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

  1. L10
    have hsi : S x = 0
  2. L11
    specialize add_eq_zero_right x1
  3. L12
    specialize add_eq_zero_right (S x)
  4. L13
    apply add_eq_zero_right
  5. L14
    exact hcontains_witness_left_witness
  6. L15
    specialize succ_ne_zero x
  7. L16
    apply succ_ne_zero
  8. L17
    exact hsi
  9. L18
    intro y
07Establish hpresentL19–21

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

  1. L19
    have hpresent : (exists i. ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y))) \/ ~(exists i. ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y)))
  2. L20
    specialize IH y
  3. L21
    exact IH
08Separate the logical casesL22–25

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

  1. L22
    cases hpresent
  2. L23
    left
  3. L24
    cases hpresent_left
  4. L25
    cases hpresent_left_witness
09Construct an explicit witnessL26–26

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

  1. L26
    exists x
10Separate the logical casesL27–27

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

  1. L27
    split
11Use earlier factsL28–35

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

  1. L28
    specialize le_succ (S x)
  2. L29
    specialize le_succ l
  3. L30
    apply le_succ
  4. L31
    exact hpresent_left_witness_left
  5. L32
    exact hpresent_left_witness_right
  6. L33
    specialize beta_at_exists b
  7. L34
    specialize beta_at_exists c
  8. L35
    specialize beta_at_exists l
12Separate the logical casesL36–36

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

  1. L36
    cases beta_at_exists
13Use earlier factsL37–38

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

  1. L37
    specialize eq_decidable x
  2. L38
    specialize eq_decidable y
14Separate the logical casesL39–40

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

  1. L39
    cases eq_decidable
  2. L40
    left
15Construct an explicit witnessL41–41

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

  1. L41
    exists l
16Separate the logical casesL42–42

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

  1. L42
    split
17Use earlier factsL43–44

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

  1. L43
    specialize le_refl (S l)
  2. L44
    exact le_refl
18Calculate and transport equalitiesL45–46

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

  1. L45
    rewrite eq_decidable_left at beta_at_exists_witness
  2. L46
    rewrite eq_decidable_left at beta_at_exists_witness
19Use earlier factsL47–47

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

  1. L47
    exact beta_at_exists_witness
20Separate the logical casesL48–48

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

  1. L48
    right
21Fix variables and assumptionsL49–49

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

  1. L49
    intro hfull
22Separate the logical casesL50–51

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

  1. L50
    cases hfull
  2. L51
    cases hfull_witness
23Establish hindexL52–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L52
    have hindex : x1 = l \/ exists h. h + S x1 = l
  2. L53
    specialize finite_lt_succ_eq_or_lt l
  3. L54
    specialize finite_lt_succ_eq_or_lt x1
  4. L55
    apply finite_lt_succ_eq_or_lt
  5. L56
    exact hfull_witness_left
24Separate the logical casesL57–57

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

  1. L57
    cases hindex
25Establish hentryL58–61

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

  1. L58
    have hentry : ((exists h. h + S y = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + y)
  2. L59
    rewrite hindex_left at hfull_witness_right
  3. L60
    rewrite hindex_left at hfull_witness_right
  4. L61
    exact hfull_witness_right
26Establish hxyL62–71

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L62
    have hxy : x = y
  2. L63
    specialize beta_at_unique b
  3. L64
    specialize beta_at_unique c
  4. L65
    specialize beta_at_unique l
  5. L66
    specialize beta_at_unique x
  6. L67
    specialize beta_at_unique y
  7. L68
    apply beta_at_unique
  8. L69
    exact beta_at_exists_witness
  9. L70
    exact hentry
  10. L71
    apply eq_decidable_right
27Use earlier factsL72–73

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

  1. L72
    exact hxy
  2. L73
    apply hpresent_right
28Construct an explicit witnessL74–74

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

  1. L74
    exists x1
29Separate the logical casesL75–75

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

  1. L75
    split
30Use earlier factsL76–77

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

  1. L76
    exact hindex_right
  2. L77
    exact hfull_witness_right

Library-wide reading audit

Original exact command ledger · 77 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro y
  5. 0005right
  6. 0006intro hcontains
  7. 0007cases hcontains
  8. 0008cases hcontains_witness
  9. 0009cases hcontains_witness_left
  10. 0010have hsi : S x = 0
  11. 0011specialize add_eq_zero_right x1
  12. 0012specialize add_eq_zero_right (S x)
  13. 0013apply add_eq_zero_right
  14. 0014exact hcontains_witness_left_witness
  15. 0015specialize succ_ne_zero x
  16. 0016apply succ_ne_zero
  17. 0017exact hsi
  18. 0018intro y
  19. 0019have hpresent : (exists i. ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y))) \/ ~(exists i. ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y)))
  20. 0020specialize IH y
  21. 0021exact IH
  22. 0022cases hpresent
  23. 0023left
  24. 0024cases hpresent_left
  25. 0025cases hpresent_left_witness
  26. 0026exists x
  27. 0027split
  28. 0028specialize le_succ (S x)
  29. 0029specialize le_succ l
  30. 0030apply le_succ
  31. 0031exact hpresent_left_witness_left
  32. 0032exact hpresent_left_witness_right
  33. 0033specialize beta_at_exists b
  34. 0034specialize beta_at_exists c
  35. 0035specialize beta_at_exists l
  36. 0036cases beta_at_exists
  37. 0037specialize eq_decidable x
  38. 0038specialize eq_decidable y
  39. 0039cases eq_decidable
  40. 0040left
  41. 0041exists l
  42. 0042split
  43. 0043specialize le_refl (S l)
  44. 0044exact le_refl
  45. 0045rewrite eq_decidable_left at beta_at_exists_witness
  46. 0046rewrite eq_decidable_left at beta_at_exists_witness
  47. 0047exact beta_at_exists_witness
  48. 0048right
  49. 0049intro hfull
  50. 0050cases hfull
  51. 0051cases hfull_witness
  52. 0052have hindex : x1 = l \/ exists h. h + S x1 = l
  53. 0053specialize finite_lt_succ_eq_or_lt l
  54. 0054specialize finite_lt_succ_eq_or_lt x1
  55. 0055apply finite_lt_succ_eq_or_lt
  56. 0056exact hfull_witness_left
  57. 0057cases hindex
  58. 0058have hentry : ((exists h. h + S y = S ((S l) * c)) /\ exists q. b = q * S ((S l) * c) + y)
  59. 0059rewrite hindex_left at hfull_witness_right
  60. 0060rewrite hindex_left at hfull_witness_right
  61. 0061exact hfull_witness_right
  62. 0062have hxy : x = y
  63. 0063specialize beta_at_unique b
  64. 0064specialize beta_at_unique c
  65. 0065specialize beta_at_unique l
  66. 0066specialize beta_at_unique x
  67. 0067specialize beta_at_unique y
  68. 0068apply beta_at_unique
  69. 0069exact beta_at_exists_witness
  70. 0070exact hentry
  71. 0071apply eq_decidable_right
  72. 0072exact hxy
  73. 0073apply hpresent_right
  74. 0074exists x1
  75. 0075split
  76. 0076exact hindex_right
  77. 0077exact hfull_witness_right