PA00A5

prime_inverse_prefix_extend

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

Append one bounded zero-based inverse index to an inverse prefix.

Exact expanded PA statement

forall p n b c l. p = S n -> ((~(p = 1) /\ forall wip_prime_left_extend_prime wip_prime_right_extend_prime. p = wip_prime_left_extend_prime * wip_prime_right_extend_prime -> wip_prime_left_extend_prime = 1 \/ wip_prime_right_extend_prime = 1)) -> (exists wip_gap_extend_length. wip_gap_extend_length + S l = n) -> (forall wip_index_extend_before. (exists wip_gap_extend_before_prefix_bound. wip_gap_extend_before_prefix_bound + S wip_index_extend_before = l) -> exists wip_mate_extend_before. ((((exists wip_beta_height_extend_before_decoded. wip_beta_height_extend_before_decoded + S (wip_mate_extend_before) = S ((S (wip_index_extend_before)) * c)) /\ exists wip_beta_quotient_extend_before_decoded. b = wip_beta_quotient_extend_before_decoded * S ((S (wip_index_extend_before)) * c) + (wip_mate_extend_before))) /\ ((exists wip_gap_extend_before_inverse_index_bound. wip_gap_extend_before_inverse_index_bound + S wip_index_extend_before = n) /\ ((exists wip_gap_extend_before_inverse_mate_bound. wip_gap_extend_before_inverse_mate_bound + S wip_mate_extend_before = n) /\ (exists wip_mod_left_extend_before_inverse_mod wip_mod_right_extend_before_inverse_mod. ((S wip_index_extend_before) * S wip_mate_extend_before) + p * wip_mod_left_extend_before_inverse_mod = 1 + p * wip_mod_right_extend_before_inverse_mod))))) -> exists z d. (forall wip_index_extend_after. (exists wip_gap_extend_after_prefix_bound. wip_gap_extend_after_prefix_bound + S wip_index_extend_after = S l) -> exists wip_mate_extend_after. ((((exists wip_beta_height_extend_after_decoded. wip_beta_height_extend_after_decoded + S (wip_mate_extend_after) = S ((S (wip_index_extend_after)) * d)) /\ exists wip_beta_quotient_extend_after_decoded. z = wip_beta_quotient_extend_after_decoded * S ((S (wip_index_extend_after)) * d) + (wip_mate_extend_after))) /\ ((exists wip_gap_extend_after_inverse_index_bound. wip_gap_extend_after_inverse_index_bound + S wip_index_extend_after = n) /\ ((exists wip_gap_extend_after_inverse_mate_bound. wip_gap_extend_after_inverse_mate_bound + S wip_mate_extend_after = n) /\ (exists wip_mod_left_extend_after_inverse_mod wip_mod_right_extend_after_inverse_mod. ((S wip_index_extend_after) * S wip_mate_extend_after) + p * wip_mod_left_extend_after_inverse_mod = 1 + p * wip_mod_right_extend_after_inverse_mod)))))

Structural proof guide

Generated structural guide

Append one bounded zero-based inverse index to an inverse prefix.

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

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

Referenced ingredients

PA00A4 prime_inverse_index_exists PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA00A4 prime_inverse_index_exists PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA00A6 prime_inverse_prefix_exists_bounded

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 p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hln
  9. 0009intro hprefix
  10. 0010have hnew : exists j. ((exists wip_gap_extend_new_inverse_index_bound. wip_gap_extend_new_inverse_index_bound + S l = n) /\ ((exists wip_gap_extend_new_inverse_mate_bound. wip_gap_extend_new_inverse_mate_bound + S j = n) /\ (exists wip_mod_left_extend_new_inverse_mod wip_mod_right_extend_new_inverse_mod. ((S l) * S j) + p * wip_mod_left_extend_new_inverse_mod = 1 + p * wip_mod_right_extend_new_inverse_mod)))
  11. 0011specialize prime_inverse_index_exists p
  12. 0012specialize prime_inverse_index_exists n
  13. 0013specialize prime_inverse_index_exists l
  14. 0014apply prime_inverse_index_exists
  15. 0015exact hpn
  16. 0016exact hp
  17. 0017exact hln
  18. 0018cases hnew
  19. 0019specialize beta_prefix_extend l
  20. 0020specialize beta_prefix_extend b
  21. 0021specialize beta_prefix_extend c
  22. 0022specialize beta_prefix_extend x
  23. 0023cases beta_prefix_extend
  24. 0024cases beta_prefix_extend_witness
  25. 0025cases beta_prefix_extend_witness_witness
  26. 0026exists x1
  27. 0027exists x2
  28. 0028intro i
  29. 0029intro hi
  30. 0030have hsplit : i = l \/ exists h. h + S i = l
  31. 0031specialize finite_lt_succ_eq_or_lt l
  32. 0032specialize finite_lt_succ_eq_or_lt i
  33. 0033apply finite_lt_succ_eq_or_lt
  34. 0034exact hi
  35. 0035cases hsplit
  36. 0036exists x
  37. 0037split
  38. 0038rewrite hsplit_left
  39. 0039rewrite hsplit_left
  40. 0040have hnew_entry : ((exists wip_beta_height_extend_new_entry. wip_beta_height_extend_new_entry + S (x) = S ((S (l)) * x2)) /\ exists wip_beta_quotient_extend_new_entry. x1 = wip_beta_quotient_extend_new_entry * S ((S (l)) * x2) + (x))
  41. 0041exact beta_prefix_extend_witness_witness_left
  42. 0042exact hnew_entry
  43. 0043rewrite hsplit_left
  44. 0044rewrite hsplit_left
  45. 0045exact hnew_witness
  46. 0046have hold : exists j. ((((exists wip_beta_height_extend_old_entry. wip_beta_height_extend_old_entry + S (j) = S ((S (i)) * c)) /\ exists wip_beta_quotient_extend_old_entry. b = wip_beta_quotient_extend_old_entry * S ((S (i)) * c) + (j))) /\ ((exists wip_gap_extend_old_inverse_index_bound. wip_gap_extend_old_inverse_index_bound + S i = n) /\ ((exists wip_gap_extend_old_inverse_mate_bound. wip_gap_extend_old_inverse_mate_bound + S j = n) /\ (exists wip_mod_left_extend_old_inverse_mod wip_mod_right_extend_old_inverse_mod. ((S i) * S j) + p * wip_mod_left_extend_old_inverse_mod = 1 + p * wip_mod_right_extend_old_inverse_mod))))
  47. 0047specialize hprefix i
  48. 0048apply hprefix
  49. 0049exact hsplit_right
  50. 0050cases hold
  51. 0051cases hold_witness
  52. 0052exists x3
  53. 0053split
  54. 0054specialize beta_prefix_extend_witness_witness_right i
  55. 0055specialize beta_prefix_extend_witness_witness_right x3
  56. 0056apply beta_prefix_extend_witness_witness_right
  57. 0057exact hsplit_right
  58. 0058exact hold_witness_left
  59. 0059exact hold_witness_right