PA004N

beta_prefix_swap_last_reflect

Stable checked-use theorem · independently closed

Every decoded swapped entry reflects to one of the two moved entries or the original index.

Exact expanded PA statement

forall b c z d n i x y. (((exists ff_h_reflect_new_i. ff_h_reflect_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_reflect_new_i. z = ff_q_reflect_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_reflect_new_n. ff_h_reflect_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_reflect_new_n. z = ff_q_reflect_new_n * S ((S (n)) * d) + (x))) -> (forall k v. (exists h. h + S k = S n) -> ~(k = i) -> ~(k = n) -> (((exists ff_h_reflect_old_k. ff_h_reflect_old_k + S (v) = S ((S (k)) * c)) /\ exists ff_q_reflect_old_k. b = ff_q_reflect_old_k * S ((S (k)) * c) + (v))) -> (((exists ff_h_reflect_new_k. ff_h_reflect_new_k + S (v) = S ((S (k)) * d)) /\ exists ff_q_reflect_new_k. z = ff_q_reflect_new_k * S ((S (k)) * d) + (v)))) -> forall j a. (exists h. h + S j = S n) -> (((exists ff_h_reflect_new_j. ff_h_reflect_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_reflect_new_j. z = ff_q_reflect_new_j * S ((S (j)) * d) + (a))) -> ((j = i /\ a = y) \/ ((j = n /\ a = x) \/ (~(j = i) /\ (~(j = n) /\ (((exists ff_h_reflect_old_j. ff_h_reflect_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_reflect_old_j. b = ff_q_reflect_old_j * S ((S (j)) * c) + (a)))))))

Structural proof guide

Generated structural guide

Every decoded swapped entry reflects to one of the two moved entries or the original index.

Use the direct prerequisites eq_decidable, beta_at_exists, beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (2), equality transport (6).

Referenced ingredients

PA004G eq_decidable PA0029 beta_at_exists PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA004G eq_decidable PA0029 beta_at_exists PA002F beta_at_unique

Direct dependents

PA004O finite_swap_last_injective PA004U finite_swap_last_surjective_back PA0054 beta_reindex_alignment_swap_last

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro n
  6. 0006intro i
  7. 0007intro x
  8. 0008intro y
  9. 0009intro hnew_i
  10. 0010intro hnew_n
  11. 0011intro hpreserve
  12. 0012intro j
  13. 0013intro a
  14. 0014intro hj
  15. 0015intro hnew
  16. 0016specialize eq_decidable j
  17. 0017specialize eq_decidable i
  18. 0018cases eq_decidable
  19. 0019left
  20. 0020split
  21. 0021exact eq_decidable_left
  22. 0022specialize beta_at_unique z
  23. 0023specialize beta_at_unique d
  24. 0024specialize beta_at_unique i
  25. 0025specialize beta_at_unique a
  26. 0026specialize beta_at_unique y
  27. 0027apply beta_at_unique
  28. 0028rewrite eq_decidable_left at hnew
  29. 0029rewrite eq_decidable_left at hnew
  30. 0030exact hnew
  31. 0031exact hnew_i
  32. 0032specialize eq_decidable_before2 n
  33. 0033cases eq_decidable_before2
  34. 0034right
  35. 0035left
  36. 0036split
  37. 0037exact eq_decidable_before2_left
  38. 0038specialize beta_at_unique z
  39. 0039specialize beta_at_unique d
  40. 0040specialize beta_at_unique n
  41. 0041specialize beta_at_unique a
  42. 0042specialize beta_at_unique x
  43. 0043apply beta_at_unique
  44. 0044rewrite eq_decidable_before2_left at hnew
  45. 0045rewrite eq_decidable_before2_left at hnew
  46. 0046exact hnew
  47. 0047exact hnew_n
  48. 0048specialize beta_at_exists b
  49. 0049specialize beta_at_exists c
  50. 0050specialize beta_at_exists j
  51. 0051cases beta_at_exists
  52. 0052have htransport : ((exists h. h + S x1 = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + x1)
  53. 0053specialize hpreserve j
  54. 0054specialize hpreserve x1
  55. 0055apply hpreserve
  56. 0056exact hj
  57. 0057exact eq_decidable_right
  58. 0058exact eq_decidable_before2_right
  59. 0059exact beta_at_exists_witness
  60. 0060have hav : a = x1
  61. 0061specialize beta_at_unique z
  62. 0062specialize beta_at_unique d
  63. 0063specialize beta_at_unique j
  64. 0064specialize beta_at_unique a
  65. 0065specialize beta_at_unique x1
  66. 0066apply beta_at_unique
  67. 0067exact hnew
  68. 0068exact htransport
  69. 0069right
  70. 0070right
  71. 0071split
  72. 0072exact eq_decidable_right
  73. 0073split
  74. 0074exact eq_decidable_before2_right
  75. 0075rewrite hav
  76. 0076rewrite hav
  77. 0077exact beta_at_exists_witness