PA004K

beta_prefix_swap_last_from_entries

Stable checked-use theorem · independently closed

Swap a chosen interior beta entry with the last entry, given both decoded values.

Exact expanded PA statement

forall b c n i x y. (exists h. h + S i = n) -> (((exists ff_h_swap_old_i. ff_h_swap_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_swap_old_i. b = ff_q_swap_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_swap_old_n. ff_h_swap_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_swap_old_n. b = ff_q_swap_old_n * S ((S (n)) * c) + (y))) -> exists z d. ((((exists ff_h_swap_new_i. ff_h_swap_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_swap_new_i. z = ff_q_swap_new_i * S ((S (i)) * d) + (y))) /\ ((((exists ff_h_swap_new_n. ff_h_swap_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_swap_new_n. z = ff_q_swap_new_n * S ((S (n)) * d) + (x))) /\ forall j a. (exists h. h + S j = S n) -> ~(j = i) -> ~(j = n) -> (((exists ff_h_swap_old_j. ff_h_swap_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_swap_old_j. b = ff_q_swap_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_swap_new_j. ff_h_swap_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_swap_new_j. z = ff_q_swap_new_j * S ((S (j)) * d) + (a)))))

Structural proof guide

Generated structural guide

Swap a chosen interior beta entry with the last entry, given both decoded values.

Use the direct prerequisites beta_prefix_replace_exists, le_succ, le_refl, lt_irrefl_expanded as previously established PA formulas.

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

Referenced ingredients

PA004J beta_prefix_replace_exists PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Proof neighborhood

Direct dependencies

PA004J beta_prefix_replace_exists PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct dependents

PA004W finite_bounded_injective_surjective PA007X beta_product_permutation_invariant PA00CX beta_sum_permutation_invariant

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 n
  4. 0004intro i
  5. 0005intro x
  6. 0006intro y
  7. 0007intro hi
  8. 0008intro hxi
  9. 0009intro hyn
  10. 0010have hisn : exists h. h + S i = S n
  11. 0011specialize le_succ (S i)
  12. 0012specialize le_succ n
  13. 0013apply le_succ
  14. 0014exact hi
  15. 0015have hnsn : exists h. h + S n = S n
  16. 0016specialize le_refl (S n)
  17. 0017exact le_refl
  18. 0018have hin : ~(i = n)
  19. 0019intro hin_eq
  20. 0020specialize lt_irrefl_expanded n
  21. 0021apply lt_irrefl_expanded
  22. 0022rewrite hin_eq at hi
  23. 0023exact hi
  24. 0024have hni : ~(n = i)
  25. 0025intro hni_eq
  26. 0026apply hin
  27. 0027symm
  28. 0028exact hni_eq
  29. 0029have hfirst : exists z d. (((exists h. h + S y = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + y) /\ forall j a. (exists h. h + S j = S n) -> ~(j = i) -> ((exists h. h + S a = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a))
  30. 0030specialize beta_prefix_replace_exists b
  31. 0031specialize beta_prefix_replace_exists c
  32. 0032specialize beta_prefix_replace_exists i
  33. 0033specialize beta_prefix_replace_exists y
  34. 0034specialize beta_prefix_replace_exists (S n)
  35. 0035apply beta_prefix_replace_exists
  36. 0036exact hisn
  37. 0037cases hfirst
  38. 0038cases hfirst_witness
  39. 0039cases hfirst_witness_witness
  40. 0040have hfirst_n : ((exists h. h + S y = S ((S n) * x2)) /\ exists q. x1 = q * S ((S n) * x2) + y)
  41. 0041specialize hfirst_witness_witness_right n
  42. 0042specialize hfirst_witness_witness_right y
  43. 0043apply hfirst_witness_witness_right
  44. 0044exact hnsn
  45. 0045exact hni
  46. 0046exact hyn
  47. 0047have hsecond : exists z d. (((exists h. h + S x = S ((S n) * d)) /\ exists q. z = q * S ((S n) * d) + x) /\ forall j a. (exists h. h + S j = S n) -> ~(j = n) -> ((exists h. h + S a = S ((S j) * x2)) /\ exists q. x1 = q * S ((S j) * x2) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a))
  48. 0048specialize beta_prefix_replace_exists x1
  49. 0049specialize beta_prefix_replace_exists x2
  50. 0050specialize beta_prefix_replace_exists n
  51. 0051specialize beta_prefix_replace_exists x
  52. 0052specialize beta_prefix_replace_exists (S n)
  53. 0053apply beta_prefix_replace_exists
  54. 0054exact hnsn
  55. 0055cases hsecond
  56. 0056cases hsecond_witness
  57. 0057cases hsecond_witness_witness
  58. 0058exists x3
  59. 0059exists x4
  60. 0060split
  61. 0061specialize hsecond_witness_witness_right i
  62. 0062specialize hsecond_witness_witness_right y
  63. 0063apply hsecond_witness_witness_right
  64. 0064exact hisn
  65. 0065exact hin
  66. 0066exact hfirst_witness_witness_left
  67. 0067split
  68. 0068exact hsecond_witness_witness_left
  69. 0069intro j
  70. 0070intro a
  71. 0071intro hj
  72. 0072intro hji
  73. 0073intro hjn
  74. 0074intro hold
  75. 0075have hmiddle : ((exists h. h + S a = S ((S j) * x2)) /\ exists q. x1 = q * S ((S j) * x2) + a)
  76. 0076specialize hfirst_witness_witness_right j
  77. 0077specialize hfirst_witness_witness_right a
  78. 0078apply hfirst_witness_witness_right
  79. 0079exact hj
  80. 0080exact hji
  81. 0081exact hold
  82. 0082specialize hsecond_witness_witness_right j
  83. 0083specialize hsecond_witness_witness_right a
  84. 0084apply hsecond_witness_witness_right
  85. 0085exact hj
  86. 0086exact hjn
  87. 0087exact hmiddle