PA0093

finite_inverse_choice_prefix_extend

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

Append one chosen source preimage to a beta-coded inverse-choice prefix.

Exact expanded PA statement

forall b c l z d k. (exists fp_i_extend_contains. ((exists fp_gap_extend_contains_index. fp_gap_extend_contains_index + S fp_i_extend_contains = l) /\ (((exists ff_h_extend_contains_entry. ff_h_extend_contains_entry + S (k) = S ((S (fp_i_extend_contains)) * c)) /\ exists ff_q_extend_contains_entry. b = ff_q_extend_contains_entry * S ((S (fp_i_extend_contains)) * c) + (k))))) -> (forall fom_value_extend_before. (exists fom_gap_extend_before_value_bound. fom_gap_extend_before_value_bound + S (fom_value_extend_before) = k) -> exists fom_index_extend_before. ((((exists fom_beta_height_extend_before_choice_entry. fom_beta_height_extend_before_choice_entry + S (fom_index_extend_before) = S ((S (fom_value_extend_before)) * d)) /\ exists fom_beta_quotient_extend_before_choice_entry. z = fom_beta_quotient_extend_before_choice_entry * S ((S (fom_value_extend_before)) * d) + (fom_index_extend_before))) /\ ((exists fom_gap_extend_before_index_bound. fom_gap_extend_before_index_bound + S (fom_index_extend_before) = l) /\ (((exists fom_beta_height_extend_before_source_entry. fom_beta_height_extend_before_source_entry + S (fom_value_extend_before) = S ((S (fom_index_extend_before)) * c)) /\ exists fom_beta_quotient_extend_before_source_entry. b = fom_beta_quotient_extend_before_source_entry * S ((S (fom_index_extend_before)) * c) + (fom_value_extend_before)))))) -> exists r s. (forall fom_value_extend_after. (exists fom_gap_extend_after_value_bound. fom_gap_extend_after_value_bound + S (fom_value_extend_after) = S k) -> exists fom_index_extend_after. ((((exists fom_beta_height_extend_after_choice_entry. fom_beta_height_extend_after_choice_entry + S (fom_index_extend_after) = S ((S (fom_value_extend_after)) * s)) /\ exists fom_beta_quotient_extend_after_choice_entry. r = fom_beta_quotient_extend_after_choice_entry * S ((S (fom_value_extend_after)) * s) + (fom_index_extend_after))) /\ ((exists fom_gap_extend_after_index_bound. fom_gap_extend_after_index_bound + S (fom_index_extend_after) = l) /\ (((exists fom_beta_height_extend_after_source_entry. fom_beta_height_extend_after_source_entry + S (fom_value_extend_after) = S ((S (fom_index_extend_after)) * c)) /\ exists fom_beta_quotient_extend_after_source_entry. b = fom_beta_quotient_extend_after_source_entry * S ((S (fom_index_extend_after)) * c) + (fom_value_extend_after))))))

Structural proof guide

Generated structural guide

Append one chosen source preimage to a beta-coded inverse-choice prefix.

Use the direct prerequisites beta_prefix_extend, finite_lt_succ_eq_or_lt as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (4), equality transport (4).

Referenced ingredients

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA0094 finite_inverse_choice_prefix_exists

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 k
  7. 0007intro hcontains
  8. 0008intro hchoice
  9. 0009cases hcontains
  10. 0010cases hcontains_witness
  11. 0011specialize beta_prefix_extend k
  12. 0012specialize beta_prefix_extend z
  13. 0013specialize beta_prefix_extend d
  14. 0014specialize beta_prefix_extend x
  15. 0015cases beta_prefix_extend
  16. 0016cases beta_prefix_extend_witness
  17. 0017cases beta_prefix_extend_witness_witness
  18. 0018exists x1
  19. 0019exists x2
  20. 0020intro y
  21. 0021intro hy
  22. 0022have hsplit : y = k \/ exists h. h + S y = k
  23. 0023specialize finite_lt_succ_eq_or_lt k
  24. 0024specialize finite_lt_succ_eq_or_lt y
  25. 0025apply finite_lt_succ_eq_or_lt
  26. 0026exact hy
  27. 0027cases hsplit
  28. 0028exists x
  29. 0029split
  30. 0030rewrite hsplit_left
  31. 0031rewrite hsplit_left
  32. 0032have hnew_entry : ((exists fom_beta_height_extend_new_entry. fom_beta_height_extend_new_entry + S (x) = S ((S (k)) * x2)) /\ exists fom_beta_quotient_extend_new_entry. x1 = fom_beta_quotient_extend_new_entry * S ((S (k)) * x2) + (x))
  33. 0033exact beta_prefix_extend_witness_witness_left
  34. 0034exact hnew_entry
  35. 0035split
  36. 0036exact hcontains_witness_left
  37. 0037rewrite hsplit_left
  38. 0038rewrite hsplit_left
  39. 0039exact hcontains_witness_right
  40. 0040have hold : forall fom_value_extend_old_result. (exists fom_gap_extend_old_result_value_bound. fom_gap_extend_old_result_value_bound + S (fom_value_extend_old_result) = k) -> exists fom_index_extend_old_result. ((((exists fom_beta_height_extend_old_result_choice_entry. fom_beta_height_extend_old_result_choice_entry + S (fom_index_extend_old_result) = S ((S (fom_value_extend_old_result)) * d)) /\ exists fom_beta_quotient_extend_old_result_choice_entry. z = fom_beta_quotient_extend_old_result_choice_entry * S ((S (fom_value_extend_old_result)) * d) + (fom_index_extend_old_result))) /\ ((exists fom_gap_extend_old_result_index_bound. fom_gap_extend_old_result_index_bound + S (fom_index_extend_old_result) = l) /\ (((exists fom_beta_height_extend_old_result_source_entry. fom_beta_height_extend_old_result_source_entry + S (fom_value_extend_old_result) = S ((S (fom_index_extend_old_result)) * c)) /\ exists fom_beta_quotient_extend_old_result_source_entry. b = fom_beta_quotient_extend_old_result_source_entry * S ((S (fom_index_extend_old_result)) * c) + (fom_value_extend_old_result)))))
  41. 0041exact hchoice
  42. 0042specialize hold y
  43. 0043have hold_y : 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)))
  44. 0044apply hold
  45. 0045exact hsplit_right
  46. 0046cases hold_y
  47. 0047cases hold_y_witness
  48. 0048exists x3
  49. 0049split
  50. 0050specialize beta_prefix_extend_witness_witness_right y
  51. 0051specialize beta_prefix_extend_witness_witness_right x3
  52. 0052apply beta_prefix_extend_witness_witness_right
  53. 0053exact hsplit_right
  54. 0054exact hold_y_witness_left
  55. 0055exact hold_y_witness_right