PA004M

finite_swap_last_bounded

Stable checked-use theorem · independently closed

A swap-last recoding preserves boundedness of the full successor prefix.

Exact expanded PA statement

forall b c z d n sn i x y. sn = S n -> (exists h. h + S i = n) -> (forall fp_i_swap_bound_old. (exists fp_gap_swap_bound_old_index. fp_gap_swap_bound_old_index + S fp_i_swap_bound_old = sn) -> exists fp_value_swap_bound_old. ((((exists ff_h_swap_bound_old_entry. ff_h_swap_bound_old_entry + S (fp_value_swap_bound_old) = S ((S (fp_i_swap_bound_old)) * c)) /\ exists ff_q_swap_bound_old_entry. b = ff_q_swap_bound_old_entry * S ((S (fp_i_swap_bound_old)) * c) + (fp_value_swap_bound_old))) /\ (exists fp_gap_swap_bound_old_value. fp_gap_swap_bound_old_value + S fp_value_swap_bound_old = sn))) -> (((exists ff_h_swap_bound_old_i. ff_h_swap_bound_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_swap_bound_old_i. b = ff_q_swap_bound_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_swap_bound_old_n. ff_h_swap_bound_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_swap_bound_old_n. b = ff_q_swap_bound_old_n * S ((S (n)) * c) + (y))) -> (((exists ff_h_swap_bound_new_i. ff_h_swap_bound_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_swap_bound_new_i. z = ff_q_swap_bound_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_swap_bound_new_n. ff_h_swap_bound_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_swap_bound_new_n. z = ff_q_swap_bound_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_bound_old_j. ff_h_swap_bound_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_swap_bound_old_j. b = ff_q_swap_bound_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_swap_bound_new_j. ff_h_swap_bound_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_swap_bound_new_j. z = ff_q_swap_bound_new_j * S ((S (j)) * d) + (a)))) -> (forall fp_i_swap_bound_new. (exists fp_gap_swap_bound_new_index. fp_gap_swap_bound_new_index + S fp_i_swap_bound_new = sn) -> exists fp_value_swap_bound_new. ((((exists ff_h_swap_bound_new_entry. ff_h_swap_bound_new_entry + S (fp_value_swap_bound_new) = S ((S (fp_i_swap_bound_new)) * d)) /\ exists ff_q_swap_bound_new_entry. z = ff_q_swap_bound_new_entry * S ((S (fp_i_swap_bound_new)) * d) + (fp_value_swap_bound_new))) /\ (exists fp_gap_swap_bound_new_value. fp_gap_swap_bound_new_value + S fp_value_swap_bound_new = sn)))

Structural proof guide

Generated structural guide

A swap-last recoding preserves boundedness of the full successor prefix.

Use the direct prerequisites finite_bounded_entry_lt, eq_decidable, le_succ, le_refl as previously established PA formulas.

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

Referenced ingredients

PA004L finite_bounded_entry_lt PA004G eq_decidable PA002O le_succ PA001A le_refl

Proof neighborhood

Direct dependencies

PA004L finite_bounded_entry_lt PA004G eq_decidable PA002O le_succ PA001A le_refl

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 z
  4. 0004intro d
  5. 0005intro n
  6. 0006intro sn
  7. 0007intro i
  8. 0008intro x
  9. 0009intro y
  10. 0010intro hsn
  11. 0011intro hi
  12. 0012intro hbounded
  13. 0013intro hold_i
  14. 0014intro hold_n
  15. 0015intro hnew_i
  16. 0016intro hnew_n
  17. 0017intro hpreserve
  18. 0018rewrite hsn at hbounded
  19. 0019rewrite hsn at hbounded
  20. 0020have hisn : exists h. h + S i = S n
  21. 0021specialize le_succ (S i)
  22. 0022specialize le_succ n
  23. 0023apply le_succ
  24. 0024exact hi
  25. 0025have hnsn : exists h. h + S n = S n
  26. 0026specialize le_refl (S n)
  27. 0027exact le_refl
  28. 0028have hentry_bound_i : forall b c l i x. (forall fp_i_entry_bound. (exists fp_gap_entry_bound_index. fp_gap_entry_bound_index + S fp_i_entry_bound = l) -> exists fp_value_entry_bound. ((((exists ff_h_entry_bound_entry. ff_h_entry_bound_entry + S (fp_value_entry_bound) = S ((S (fp_i_entry_bound)) * c)) /\ exists ff_q_entry_bound_entry. b = ff_q_entry_bound_entry * S ((S (fp_i_entry_bound)) * c) + (fp_value_entry_bound))) /\ (exists fp_gap_entry_bound_value. fp_gap_entry_bound_value + S fp_value_entry_bound = l))) -> (exists h. h + S i = l) -> (((exists ff_h_entry_bound_at. ff_h_entry_bound_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_entry_bound_at. b = ff_q_entry_bound_at * S ((S (i)) * c) + (x))) -> exists h. h + S x = l
  29. 0029exact finite_bounded_entry_lt
  30. 0030have hentry_bound_n : forall b c l i x. (forall fp_i_entry_bound. (exists fp_gap_entry_bound_index. fp_gap_entry_bound_index + S fp_i_entry_bound = l) -> exists fp_value_entry_bound. ((((exists ff_h_entry_bound_entry. ff_h_entry_bound_entry + S (fp_value_entry_bound) = S ((S (fp_i_entry_bound)) * c)) /\ exists ff_q_entry_bound_entry. b = ff_q_entry_bound_entry * S ((S (fp_i_entry_bound)) * c) + (fp_value_entry_bound))) /\ (exists fp_gap_entry_bound_value. fp_gap_entry_bound_value + S fp_value_entry_bound = l))) -> (exists h. h + S i = l) -> (((exists ff_h_entry_bound_at. ff_h_entry_bound_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_entry_bound_at. b = ff_q_entry_bound_at * S ((S (i)) * c) + (x))) -> exists h. h + S x = l
  31. 0031exact finite_bounded_entry_lt
  32. 0032have hxb : exists h. h + S x = S n
  33. 0033specialize hentry_bound_i b
  34. 0034specialize hentry_bound_i c
  35. 0035specialize hentry_bound_i (S n)
  36. 0036specialize hentry_bound_i i
  37. 0037specialize hentry_bound_i x
  38. 0038apply hentry_bound_i
  39. 0039exact hbounded
  40. 0040exact hisn
  41. 0041exact hold_i
  42. 0042have hyb : exists h. h + S y = S n
  43. 0043specialize hentry_bound_n b
  44. 0044specialize hentry_bound_n c
  45. 0045specialize hentry_bound_n (S n)
  46. 0046specialize hentry_bound_n n
  47. 0047specialize hentry_bound_n y
  48. 0048apply hentry_bound_n
  49. 0049exact hbounded
  50. 0050exact hnsn
  51. 0051exact hold_n
  52. 0052have heq_i : forall u v. u = v \/ ~(u = v)
  53. 0053exact eq_decidable
  54. 0054have heq_n : forall u v. u = v \/ ~(u = v)
  55. 0055exact eq_decidable
  56. 0056rewrite hsn
  57. 0057rewrite hsn
  58. 0058intro j
  59. 0059intro hj
  60. 0060specialize heq_i j
  61. 0061specialize heq_i i
  62. 0062cases heq_i
  63. 0063exists y
  64. 0064split
  65. 0065rewrite heq_i_left
  66. 0066rewrite heq_i_left
  67. 0067exact hnew_i
  68. 0068exact hyb
  69. 0069specialize heq_n j
  70. 0070specialize heq_n n
  71. 0071cases heq_n
  72. 0072exists x
  73. 0073split
  74. 0074rewrite heq_n_left
  75. 0075rewrite heq_n_left
  76. 0076exact hnew_n
  77. 0077exact hxb
  78. 0078specialize hbounded j
  79. 0079have hold : exists a. (((exists h. h + S a = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + a) /\ exists h. h + S a = S n)
  80. 0080apply hbounded
  81. 0081exact hj
  82. 0082cases hold
  83. 0083cases hold_witness
  84. 0084exists x1
  85. 0085split
  86. 0086specialize hpreserve j
  87. 0087specialize hpreserve x1
  88. 0088apply hpreserve
  89. 0089exact hj
  90. 0090exact heq_i_right
  91. 0091exact heq_n_right
  92. 0092exact hold_witness_left
  93. 0093exact hold_witness_right