PA0092

finite_covers_into_or_omits

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

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

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-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. 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