PA0095

finite_inverse_choice_bounded_into

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

Every inverse-choice prefix is bounded into the source domain.

Exact expanded PA statement

forall b c l z d n. (forall fom_value_bounded_choice. (exists fom_gap_bounded_choice_value_bound. fom_gap_bounded_choice_value_bound + S (fom_value_bounded_choice) = n) -> exists fom_index_bounded_choice. ((((exists fom_beta_height_bounded_choice_choice_entry. fom_beta_height_bounded_choice_choice_entry + S (fom_index_bounded_choice) = S ((S (fom_value_bounded_choice)) * d)) /\ exists fom_beta_quotient_bounded_choice_choice_entry. z = fom_beta_quotient_bounded_choice_choice_entry * S ((S (fom_value_bounded_choice)) * d) + (fom_index_bounded_choice))) /\ ((exists fom_gap_bounded_choice_index_bound. fom_gap_bounded_choice_index_bound + S (fom_index_bounded_choice) = l) /\ (((exists fom_beta_height_bounded_choice_source_entry. fom_beta_height_bounded_choice_source_entry + S (fom_value_bounded_choice) = S ((S (fom_index_bounded_choice)) * c)) /\ exists fom_beta_quotient_bounded_choice_source_entry. b = fom_beta_quotient_bounded_choice_source_entry * S ((S (fom_index_bounded_choice)) * c) + (fom_value_bounded_choice)))))) -> (forall fom_index_bounded_result. (exists fom_gap_bounded_result_index_bound. fom_gap_bounded_result_index_bound + S (fom_index_bounded_result) = n) -> exists fom_value_bounded_result. ((((exists fom_beta_height_bounded_result_entry. fom_beta_height_bounded_result_entry + S (fom_value_bounded_result) = S ((S (fom_index_bounded_result)) * d)) /\ exists fom_beta_quotient_bounded_result_entry. z = fom_beta_quotient_bounded_result_entry * S ((S (fom_index_bounded_result)) * d) + (fom_value_bounded_result))) /\ (exists fom_gap_bounded_result_value_bound. fom_gap_bounded_result_value_bound + S (fom_value_bounded_result) = l)))

Structural proof guide

Generated structural guide

Every inverse-choice prefix is bounded into the source domain.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

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

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

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. 0004intro z
  5. 0005intro d
  6. 0006intro n
  7. 0007intro hchoice
  8. 0008intro y
  9. 0009intro hy
  10. 0010specialize hchoice y
  11. 0011have hstored : exists i. (((exists h. h + S i = S ((S y) * d)) /\ exists q. z = q * S ((S y) * d) + i) /\ ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y)))
  12. 0012apply hchoice
  13. 0013exact hy
  14. 0014cases hstored
  15. 0015cases hstored_witness
  16. 0016cases hstored_witness_right
  17. 0017exists x
  18. 0018split
  19. 0019exact hstored_witness_left
  20. 0020exact hstored_witness_right_left