PA0092

finite_covers_into_or_omits

Alpha v34 checked-use theorem · independently closed; not Stable

Bounded occurrence search either covers the target interval or returns an explicit omission.

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 n. (forall fom_value_search_cover. (exists fom_gap_search_cover_value_bound. fom_gap_search_cover_value_bound + S (fom_value_search_cover) = n) -> exists fom_index_search_cover. ((exists fom_gap_search_cover_index_bound. fom_gap_search_cover_index_bound + S (fom_index_search_cover) = l) /\ (((exists fom_beta_height_search_cover_entry. fom_beta_height_search_cover_entry + S (fom_value_search_cover) = S ((S (fom_index_search_cover)) * c)) /\ exists fom_beta_quotient_search_cover_entry. b = fom_beta_quotient_search_cover_entry * S ((S (fom_index_search_cover)) * c) + (fom_value_search_cover))))) \/ (exists fom_value_search_omit. ((exists fom_gap_search_omit_value_bound. fom_gap_search_omit_value_bound + S (fom_value_search_omit) = n) /\ ~(exists fom_index_search_omit. ((exists fom_gap_search_omit_index_bound. fom_gap_search_omit_index_bound + S (fom_index_search_omit) = l) /\ (((exists fom_beta_height_search_omit_entry. fom_beta_height_search_omit_entry + S (fom_value_search_omit) = S ((S (fom_index_search_omit)) * c)) /\ exists fom_beta_quotient_search_omit_entry. b = fom_beta_quotient_search_omit_entry * S ((S (fom_index_search_omit)) * c) + (fom_value_search_omit)))))))

Structural proof guide

Generated structural guide

Bounded occurrence search either covers the target interval or returns an explicit omission.

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

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

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA004H finite_contains_decidable PA003D finite_lt_succ_eq_or_lt PA002O le_succ PA001A le_refl

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA004H finite_contains_decidable PA003D finite_lt_succ_eq_or_lt PA002O le_succ PA001A le_refl

Direct dependents

PA0098 finite_short_prefix_omits

Formal native tactic body

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

Read the argument

Proof checkpoints

60 script commands · 23 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 (6)
add eq zero rightsucc ne zerofinite contains decidablefinite lt succ eq or ltle succle refl

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–3

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
02Induction on nL4–4

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

  1. L4
    induction n
03Separate the logical casesL5–5

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

  1. L5
    left
04Fix variables and assumptionsL6–7

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

  1. L6
    intro y
  2. L7
    intro hy
05Separate the logical casesL8–9

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

  1. L8
    exfalso
  2. L9
    cases hy
06Establish hsyL10–17

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 hsy : S y = 0
  2. L11
    specialize add_eq_zero_right x
  3. L12
    specialize add_eq_zero_right (S y)
  4. L13
    apply add_eq_zero_right
  5. L14
    exact hy_witness
  6. L15
    specialize succ_ne_zero y
  7. L16
    apply succ_ne_zero
  8. L17
    exact hsy
07Establish hpreviousL18–19

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

  1. L18
    have hprevious : (∀ x. Lt(x,n) → ContainsPrefix(b,c,l,x)) ∨ (∃ x. Lt(x,n) ∧ ¬ContainsPrefix(b,c,l,x))Definitions: LtContainsPrefix
  2. L19
    exact IH
08Separate the logical casesL20–20

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

  1. L20
    cases hprevious
09Establish htopL21–26

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

  1. L21
    have htop : ContainsPrefix(b,c,l,n) ∨ ¬ContainsPrefix(b,c,l,n)Definitions: ContainsPrefix
  2. L22
    specialize finite_contains_decidable b
  3. L23
    specialize finite_contains_decidable c
  4. L24
    specialize finite_contains_decidable l
  5. L25
    specialize finite_contains_decidable n
  6. L26
    exact finite_contains_decidable
10Separate the logical casesL27–28

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

  1. L27
    cases htop
  2. L28
    left
11Establish hsuccessor_coverL29–31

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

  1. L29
    have hsuccessor_cover : ∀ fom_value_search_successor_cover. Lt(fom_value_search_successor_cover,S n) → ContainsPrefix(b,c,l,fom_value_search_successor_cover)Definitions: LtContainsPrefix
  2. L30
    intro y
  3. L31
    intro hy
12Establish hsplitL32–36

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. L32
    have hsplit : y = n \/ exists h. h + S y = n
  2. L33
    specialize finite_lt_succ_eq_or_lt n
  3. L34
    specialize finite_lt_succ_eq_or_lt y
  4. L35
    apply finite_lt_succ_eq_or_lt
  5. L36
    exact hy
13Separate the logical casesL37–37

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

  1. L37
    cases hsplit
14Calculate and transport equalitiesL38–39

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

  1. L38
    rewrite hsplit_left
  2. L39
    rewrite hsplit_left
15Use earlier factsL40–44

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

  1. L40
    exact htop_left
  2. L41
    specialize hprevious_left y
  3. L42
    apply hprevious_left
  4. L43
    exact hsplit_right
  5. L44
    exact hsuccessor_cover
16Separate the logical casesL45–45

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

  1. L45
    right
17Construct an explicit witnessL46–46

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

  1. L46
    exists n
18Separate the logical casesL47–47

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

  1. L47
    split
19Use earlier factsL48–50

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

  1. L48
    specialize le_refl (S n)
  2. L49
    exact le_refl
  3. L50
    exact htop_right
20Separate the logical casesL51–53

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

  1. L51
    right
  2. L52
    cases hprevious_right
  3. L53
    cases hprevious_right_witness
21Construct an explicit witnessL54–54

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

  1. L54
    exists x
22Separate the logical casesL55–55

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

  1. L55
    split
23Use earlier factsL56–60

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

  1. L56
    specialize le_succ (S x)
  2. L57
    specialize le_succ n
  3. L58
    apply le_succ
  4. L59
    exact hprevious_right_witness_left
  5. L60
    exact hprevious_right_witness_right

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004induction n
  5. 0005left
  6. 0006intro y
  7. 0007intro hy
  8. 0008exfalso
  9. 0009cases hy
  10. 0010have hsy : S y = 0
  11. 0011specialize add_eq_zero_right x
  12. 0012specialize add_eq_zero_right (S y)
  13. 0013apply add_eq_zero_right
  14. 0014exact hy_witness
  15. 0015specialize succ_ne_zero y
  16. 0016apply succ_ne_zero
  17. 0017exact hsy
  18. 0018have hprevious : (forall fom_value_search_previous_cover. (exists fom_gap_search_previous_cover_value_bound. fom_gap_search_previous_cover_value_bound + S (fom_value_search_previous_cover) = n) -> exists fom_index_search_previous_cover. ((exists fom_gap_search_previous_cover_index_bound. fom_gap_search_previous_cover_index_bound + S (fom_index_search_previous_cover) = l) /\ (((exists fom_beta_height_search_previous_cover_entry. fom_beta_height_search_previous_cover_entry + S (fom_value_search_previous_cover) = S ((S (fom_index_search_previous_cover)) * c)) /\ exists fom_beta_quotient_search_previous_cover_entry. b = fom_beta_quotient_search_previous_cover_entry * S ((S (fom_index_search_previous_cover)) * c) + (fom_value_search_previous_cover))))) \/ (exists fom_value_search_previous_omit. ((exists fom_gap_search_previous_omit_value_bound. fom_gap_search_previous_omit_value_bound + S (fom_value_search_previous_omit) = n) /\ ~(exists fom_index_search_previous_omit. ((exists fom_gap_search_previous_omit_index_bound. fom_gap_search_previous_omit_index_bound + S (fom_index_search_previous_omit) = l) /\ (((exists fom_beta_height_search_previous_omit_entry. fom_beta_height_search_previous_omit_entry + S (fom_value_search_previous_omit) = S ((S (fom_index_search_previous_omit)) * c)) /\ exists fom_beta_quotient_search_previous_omit_entry. b = fom_beta_quotient_search_previous_omit_entry * S ((S (fom_index_search_previous_omit)) * c) + (fom_value_search_previous_omit)))))))
  19. 0019exact IH
  20. 0020cases hprevious
  21. 0021have htop : (exists fp_i_search_top_contains. ((exists fp_gap_search_top_contains_index. fp_gap_search_top_contains_index + S fp_i_search_top_contains = l) /\ (((exists ff_h_search_top_contains_entry. ff_h_search_top_contains_entry + S (n) = S ((S (fp_i_search_top_contains)) * c)) /\ exists ff_q_search_top_contains_entry. b = ff_q_search_top_contains_entry * S ((S (fp_i_search_top_contains)) * c) + (n))))) \/ ~(exists fp_i_search_top_contains. ((exists fp_gap_search_top_contains_index. fp_gap_search_top_contains_index + S fp_i_search_top_contains = l) /\ (((exists ff_h_search_top_contains_entry. ff_h_search_top_contains_entry + S (n) = S ((S (fp_i_search_top_contains)) * c)) /\ exists ff_q_search_top_contains_entry. b = ff_q_search_top_contains_entry * S ((S (fp_i_search_top_contains)) * c) + (n)))))
  22. 0022specialize finite_contains_decidable b
  23. 0023specialize finite_contains_decidable c
  24. 0024specialize finite_contains_decidable l
  25. 0025specialize finite_contains_decidable n
  26. 0026exact finite_contains_decidable
  27. 0027cases htop
  28. 0028left
  29. 0029have hsuccessor_cover : forall fom_value_search_successor_cover. (exists fom_gap_search_successor_cover_value_bound. fom_gap_search_successor_cover_value_bound + S (fom_value_search_successor_cover) = S n) -> exists fom_index_search_successor_cover. ((exists fom_gap_search_successor_cover_index_bound. fom_gap_search_successor_cover_index_bound + S (fom_index_search_successor_cover) = l) /\ (((exists fom_beta_height_search_successor_cover_entry. fom_beta_height_search_successor_cover_entry + S (fom_value_search_successor_cover) = S ((S (fom_index_search_successor_cover)) * c)) /\ exists fom_beta_quotient_search_successor_cover_entry. b = fom_beta_quotient_search_successor_cover_entry * S ((S (fom_index_search_successor_cover)) * c) + (fom_value_search_successor_cover))))
  30. 0030intro y
  31. 0031intro hy
  32. 0032have hsplit : y = n \/ exists h. h + S y = n
  33. 0033specialize finite_lt_succ_eq_or_lt n
  34. 0034specialize finite_lt_succ_eq_or_lt y
  35. 0035apply finite_lt_succ_eq_or_lt
  36. 0036exact hy
  37. 0037cases hsplit
  38. 0038rewrite hsplit_left
  39. 0039rewrite hsplit_left
  40. 0040exact htop_left
  41. 0041specialize hprevious_left y
  42. 0042apply hprevious_left
  43. 0043exact hsplit_right
  44. 0044exact hsuccessor_cover
  45. 0045right
  46. 0046exists n
  47. 0047split
  48. 0048specialize le_refl (S n)
  49. 0049exact le_refl
  50. 0050exact htop_right
  51. 0051right
  52. 0052cases hprevious_right
  53. 0053cases hprevious_right_witness
  54. 0054exists x
  55. 0055split
  56. 0056specialize le_succ (S x)
  57. 0057specialize le_succ n
  58. 0058apply le_succ
  59. 0059exact hprevious_right_witness_left
  60. 0060exact hprevious_right_witness_right