PA0094

finite_inverse_choice_prefix_exists

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

Full finite coverage admits a beta-coded choice of one preimage for each target value.

Exact expanded PA statement

forall b c l n. (forall fom_value_exists_cover. (exists fom_gap_exists_cover_value_bound. fom_gap_exists_cover_value_bound + S (fom_value_exists_cover) = n) -> exists fom_index_exists_cover. ((exists fom_gap_exists_cover_index_bound. fom_gap_exists_cover_index_bound + S (fom_index_exists_cover) = l) /\ (((exists fom_beta_height_exists_cover_entry. fom_beta_height_exists_cover_entry + S (fom_value_exists_cover) = S ((S (fom_index_exists_cover)) * c)) /\ exists fom_beta_quotient_exists_cover_entry. b = fom_beta_quotient_exists_cover_entry * S ((S (fom_index_exists_cover)) * c) + (fom_value_exists_cover))))) -> exists z d. (forall fom_value_exists_result. (exists fom_gap_exists_result_value_bound. fom_gap_exists_result_value_bound + S (fom_value_exists_result) = n) -> exists fom_index_exists_result. ((((exists fom_beta_height_exists_result_choice_entry. fom_beta_height_exists_result_choice_entry + S (fom_index_exists_result) = S ((S (fom_value_exists_result)) * d)) /\ exists fom_beta_quotient_exists_result_choice_entry. z = fom_beta_quotient_exists_result_choice_entry * S ((S (fom_value_exists_result)) * d) + (fom_index_exists_result))) /\ ((exists fom_gap_exists_result_index_bound. fom_gap_exists_result_index_bound + S (fom_index_exists_result) = l) /\ (((exists fom_beta_height_exists_result_source_entry. fom_beta_height_exists_result_source_entry + S (fom_value_exists_result) = S ((S (fom_index_exists_result)) * c)) /\ exists fom_beta_quotient_exists_result_source_entry. b = fom_beta_quotient_exists_result_source_entry * S ((S (fom_index_exists_result)) * c) + (fom_value_exists_result))))))

Structural proof guide

Generated structural guide

Full finite coverage admits a beta-coded choice of one preimage for each target value.

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

The proof proceeds by structural induction (1), case analysis (3), intermediate claims (6).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0093 finite_inverse_choice_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0093 finite_inverse_choice_prefix_extend

Direct dependents

PA0097 finite_short_cover_impossible

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. 0005intro hcover
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro y
  9. 0009intro hy
  10. 0010exfalso
  11. 0011cases hy
  12. 0012have hsy : S y = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S y)
  15. 0015apply add_eq_zero_right
  16. 0016exact hy_witness
  17. 0017specialize succ_ne_zero y
  18. 0018apply succ_ne_zero
  19. 0019exact hsy
  20. 0020intro hcover
  21. 0021have hcover_all : forall fom_value_exists_successor_cover. (exists fom_gap_exists_successor_cover_value_bound. fom_gap_exists_successor_cover_value_bound + S (fom_value_exists_successor_cover) = S n) -> exists fom_index_exists_successor_cover. ((exists fom_gap_exists_successor_cover_index_bound. fom_gap_exists_successor_cover_index_bound + S (fom_index_exists_successor_cover) = l) /\ (((exists fom_beta_height_exists_successor_cover_entry. fom_beta_height_exists_successor_cover_entry + S (fom_value_exists_successor_cover) = S ((S (fom_index_exists_successor_cover)) * c)) /\ exists fom_beta_quotient_exists_successor_cover_entry. b = fom_beta_quotient_exists_successor_cover_entry * S ((S (fom_index_exists_successor_cover)) * c) + (fom_value_exists_successor_cover))))
  22. 0022exact hcover
  23. 0023have hpast : forall fom_value_exists_previous_cover. (exists fom_gap_exists_previous_cover_value_bound. fom_gap_exists_previous_cover_value_bound + S (fom_value_exists_previous_cover) = n) -> exists fom_index_exists_previous_cover. ((exists fom_gap_exists_previous_cover_index_bound. fom_gap_exists_previous_cover_index_bound + S (fom_index_exists_previous_cover) = l) /\ (((exists fom_beta_height_exists_previous_cover_entry. fom_beta_height_exists_previous_cover_entry + S (fom_value_exists_previous_cover) = S ((S (fom_index_exists_previous_cover)) * c)) /\ exists fom_beta_quotient_exists_previous_cover_entry. b = fom_beta_quotient_exists_previous_cover_entry * S ((S (fom_index_exists_previous_cover)) * c) + (fom_value_exists_previous_cover))))
  24. 0024intro y
  25. 0025intro hy
  26. 0026specialize hcover_all y
  27. 0027apply hcover_all
  28. 0028specialize le_succ (S y)
  29. 0029specialize le_succ n
  30. 0030apply le_succ
  31. 0031exact hy
  32. 0032have hprevious : exists z d. (forall fom_value_exists_previous_choice. (exists fom_gap_exists_previous_choice_value_bound. fom_gap_exists_previous_choice_value_bound + S (fom_value_exists_previous_choice) = n) -> exists fom_index_exists_previous_choice. ((((exists fom_beta_height_exists_previous_choice_choice_entry. fom_beta_height_exists_previous_choice_choice_entry + S (fom_index_exists_previous_choice) = S ((S (fom_value_exists_previous_choice)) * d)) /\ exists fom_beta_quotient_exists_previous_choice_choice_entry. z = fom_beta_quotient_exists_previous_choice_choice_entry * S ((S (fom_value_exists_previous_choice)) * d) + (fom_index_exists_previous_choice))) /\ ((exists fom_gap_exists_previous_choice_index_bound. fom_gap_exists_previous_choice_index_bound + S (fom_index_exists_previous_choice) = l) /\ (((exists fom_beta_height_exists_previous_choice_source_entry. fom_beta_height_exists_previous_choice_source_entry + S (fom_value_exists_previous_choice) = S ((S (fom_index_exists_previous_choice)) * c)) /\ exists fom_beta_quotient_exists_previous_choice_source_entry. b = fom_beta_quotient_exists_previous_choice_source_entry * S ((S (fom_index_exists_previous_choice)) * c) + (fom_value_exists_previous_choice))))))
  33. 0033apply IH
  34. 0034exact hpast
  35. 0035cases hprevious
  36. 0036cases hprevious_witness
  37. 0037have htop : exists fp_i_exists_top_contains. ((exists fp_gap_exists_top_contains_index. fp_gap_exists_top_contains_index + S fp_i_exists_top_contains = l) /\ (((exists ff_h_exists_top_contains_entry. ff_h_exists_top_contains_entry + S (n) = S ((S (fp_i_exists_top_contains)) * c)) /\ exists ff_q_exists_top_contains_entry. b = ff_q_exists_top_contains_entry * S ((S (fp_i_exists_top_contains)) * c) + (n))))
  38. 0038specialize hcover n
  39. 0039apply hcover
  40. 0040specialize le_refl (S n)
  41. 0041exact le_refl
  42. 0042have hnext : exists z d. (forall fom_value_exists_successor_choice. (exists fom_gap_exists_successor_choice_value_bound. fom_gap_exists_successor_choice_value_bound + S (fom_value_exists_successor_choice) = S n) -> exists fom_index_exists_successor_choice. ((((exists fom_beta_height_exists_successor_choice_choice_entry. fom_beta_height_exists_successor_choice_choice_entry + S (fom_index_exists_successor_choice) = S ((S (fom_value_exists_successor_choice)) * d)) /\ exists fom_beta_quotient_exists_successor_choice_choice_entry. z = fom_beta_quotient_exists_successor_choice_choice_entry * S ((S (fom_value_exists_successor_choice)) * d) + (fom_index_exists_successor_choice))) /\ ((exists fom_gap_exists_successor_choice_index_bound. fom_gap_exists_successor_choice_index_bound + S (fom_index_exists_successor_choice) = l) /\ (((exists fom_beta_height_exists_successor_choice_source_entry. fom_beta_height_exists_successor_choice_source_entry + S (fom_value_exists_successor_choice) = S ((S (fom_index_exists_successor_choice)) * c)) /\ exists fom_beta_quotient_exists_successor_choice_source_entry. b = fom_beta_quotient_exists_successor_choice_source_entry * S ((S (fom_index_exists_successor_choice)) * c) + (fom_value_exists_successor_choice))))))
  43. 0043specialize finite_inverse_choice_prefix_extend b
  44. 0044specialize finite_inverse_choice_prefix_extend c
  45. 0045specialize finite_inverse_choice_prefix_extend l
  46. 0046specialize finite_inverse_choice_prefix_extend x
  47. 0047specialize finite_inverse_choice_prefix_extend x1
  48. 0048specialize finite_inverse_choice_prefix_extend n
  49. 0049apply finite_inverse_choice_prefix_extend
  50. 0050exact htop
  51. 0051exact hprevious_witness_witness
  52. 0052exact hnext