PA0098 · theorem

finite_short_prefix_omits

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

Every beta-coded prefix shorter than n explicitly omits a value below n.

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. ∀ n. Lt(l,n) → ∃ x. Lt(x,n) ∧ ¬ContainsPrefix(b,c,l,x)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0027 ContainsPrefix

3 occurrences

In local proof propositions

PD0002 Lt PD0027 ContainsPrefix

4 occurrences

Exact expanded native-PA statement
forall b c l n. (exists h. h + S l = n) -> (exists fom_value_short_omit. ((exists fom_gap_short_omit_value_bound. fom_gap_short_omit_value_bound + S (fom_value_short_omit) = n) /\ ~(exists fom_index_short_omit. ((exists fom_gap_short_omit_index_bound. fom_gap_short_omit_index_bound + S (fom_index_short_omit) = l) /\ (((exists fom_beta_height_short_omit_entry. fom_beta_height_short_omit_entry + S (fom_value_short_omit) = S ((S (fom_index_short_omit)) * c)) /\ exists fom_beta_quotient_short_omit_entry. b = fom_beta_quotient_short_omit_entry * S ((S (fom_index_short_omit)) * c) + (fom_value_short_omit)))))))

Proof neighborhood

Direct theorem prerequisites

PA0092 finite_covers_into_or_omits PA0097 finite_short_cover_impossible

Direct theorem dependents

PA009I scaled_inverse_prefix_choose_omitted_orbit PA00AE finite_prefix_choose_unused_nonendpoint

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

21 script commands · 4 reading checkpoints · 1 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 (2)
finite covers into or omitsfinite short cover impossible
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro hln
02Establish hsearchL6–11

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

  1. L6
    have hsearch : (∀ x. Lt(x,n) → ContainsPrefix(b,c,l,x)) ∨ (∃ x. Lt(x,n) ∧ ¬ContainsPrefix(b,c,l,x))Definitions: Lt(x,n)ContainsPrefix(b,c,l,x)Original native command in the exact edition
  2. L7
    specialize finite_covers_into_or_omits b
  3. L8
    specialize finite_covers_into_or_omits c
  4. L9
    specialize finite_covers_into_or_omits l
  5. L10
    specialize finite_covers_into_or_omits n
  6. L11
    exact finite_covers_into_or_omits
03Separate the logical casesL12–13

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

  1. L12
    cases hsearch
  2. L13
    exfalso
04Use earlier factsL14–21

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

  1. L14
    specialize finite_short_cover_impossible b
  2. L15
    specialize finite_short_cover_impossible c
  3. L16
    specialize finite_short_cover_impossible l
  4. L17
    specialize finite_short_cover_impossible n
  5. L18
    apply finite_short_cover_impossible
  6. L19
    exact hln
  7. L20
    exact hsearch_left
  8. L21
    exact hsearch_right

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hln
  6. 0006have hsearch : (∀ x. Lt(x,n) → ContainsPrefix(b,c,l,x)) ∨ (∃ x. Lt(x,n) ∧ ¬ContainsPrefix(b,c,l,x))
    Exact native replay linehave hsearch : ((forall fom_value_short_cover. (exists fom_gap_short_cover_value_bound. fom_gap_short_cover_value_bound + S (fom_value_short_cover) = n) -> exists fom_index_short_cover. ((exists fom_gap_short_cover_index_bound. fom_gap_short_cover_index_bound + S (fom_index_short_cover) = l) /\ (((exists fom_beta_height_short_cover_entry. fom_beta_height_short_cover_entry + S (fom_value_short_cover) = S ((S (fom_index_short_cover)) * c)) /\ exists fom_beta_quotient_short_cover_entry. b = fom_beta_quotient_short_cover_entry * S ((S (fom_index_short_cover)) * c) + (fom_value_short_cover))))) \/ (exists fom_value_short_omit. ((exists fom_gap_short_omit_value_bound. fom_gap_short_omit_value_bound + S (fom_value_short_omit) = n) /\ ~(exists fom_index_short_omit. ((exists fom_gap_short_omit_index_bound. fom_gap_short_omit_index_bound + S (fom_index_short_omit) = l) /\ (((exists fom_beta_height_short_omit_entry. fom_beta_height_short_omit_entry + S (fom_value_short_omit) = S ((S (fom_index_short_omit)) * c)) /\ exists fom_beta_quotient_short_omit_entry. b = fom_beta_quotient_short_omit_entry * S ((S (fom_index_short_omit)) * c) + (fom_value_short_omit))))))))
  7. 0007specialize finite_covers_into_or_omits b
  8. 0008specialize finite_covers_into_or_omits c
  9. 0009specialize finite_covers_into_or_omits l
  10. 0010specialize finite_covers_into_or_omits n
  11. 0011exact finite_covers_into_or_omits
  12. 0012cases hsearch
  13. 0013exfalso
  14. 0014specialize finite_short_cover_impossible b
  15. 0015specialize finite_short_cover_impossible c
  16. 0016specialize finite_short_cover_impossible l
  17. 0017specialize finite_short_cover_impossible n
  18. 0018apply finite_short_cover_impossible
  19. 0019exact hln
  20. 0020exact hsearch_left
  21. 0021exact hsearch_right