PA0098

finite_short_prefix_omits

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

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

Exact expanded 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)))))))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites finite_covers_into_or_omits, finite_short_cover_impossible as previously established PA formulas.

The proof proceeds by case analysis (1), intermediate claims (1).

Referenced ingredients

PA0092 finite_covers_into_or_omits PA0097 finite_short_cover_impossible

Proof neighborhood

Direct dependencies

PA0092 finite_covers_into_or_omits PA0097 finite_short_cover_impossible

Direct dependents

PA009I scaled_inverse_prefix_choose_omitted_orbit PA00AE finite_prefix_choose_unused_nonendpoint

Formal native tactic body

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

  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hln
  6. 0006have 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