PA004U

finite_swap_last_surjective_back

Stable checked-use theorem · independently closed

Surjectivity of a swapped successor prefix transports back to the original code.

Exact expanded PA statement

forall b c z d n sn i x y. sn = S n -> (exists h. h + S i = n) -> (((exists ff_h_swap_surj_old_i. ff_h_swap_surj_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_swap_surj_old_i. b = ff_q_swap_surj_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_swap_surj_old_n. ff_h_swap_surj_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_swap_surj_old_n. b = ff_q_swap_surj_old_n * S ((S (n)) * c) + (y))) -> (((exists ff_h_swap_surj_new_i. ff_h_swap_surj_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_swap_surj_new_i. z = ff_q_swap_surj_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_swap_surj_new_n. ff_h_swap_surj_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_swap_surj_new_n. z = ff_q_swap_surj_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_surj_old_j. ff_h_swap_surj_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_swap_surj_old_j. b = ff_q_swap_surj_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_swap_surj_new_j. ff_h_swap_surj_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_swap_surj_new_j. z = ff_q_swap_surj_new_j * S ((S (j)) * d) + (a)))) -> (forall fp_value_swap_surj_new. (exists fp_gap_swap_surj_new_value. fp_gap_swap_surj_new_value + S fp_value_swap_surj_new = sn) -> exists fp_i_swap_surj_new. ((exists fp_gap_swap_surj_new_index. fp_gap_swap_surj_new_index + S fp_i_swap_surj_new = sn) /\ (((exists ff_h_swap_surj_new_entry. ff_h_swap_surj_new_entry + S (fp_value_swap_surj_new) = S ((S (fp_i_swap_surj_new)) * d)) /\ exists ff_q_swap_surj_new_entry. z = ff_q_swap_surj_new_entry * S ((S (fp_i_swap_surj_new)) * d) + (fp_value_swap_surj_new))))) -> (forall fp_value_swap_surj_old. (exists fp_gap_swap_surj_old_value. fp_gap_swap_surj_old_value + S fp_value_swap_surj_old = sn) -> exists fp_i_swap_surj_old. ((exists fp_gap_swap_surj_old_index. fp_gap_swap_surj_old_index + S fp_i_swap_surj_old = sn) /\ (((exists ff_h_swap_surj_old_entry. ff_h_swap_surj_old_entry + S (fp_value_swap_surj_old) = S ((S (fp_i_swap_surj_old)) * c)) /\ exists ff_q_swap_surj_old_entry. b = ff_q_swap_surj_old_entry * S ((S (fp_i_swap_surj_old)) * c) + (fp_value_swap_surj_old)))))

Structural proof guide

Generated structural guide

Surjectivity of a swapped successor prefix transports back to the original code.

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

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

Referenced ingredients

PA004N beta_prefix_swap_last_reflect PA002O le_succ PA001A le_refl

Proof neighborhood

Direct dependencies

PA004N beta_prefix_swap_last_reflect PA002O le_succ PA001A le_refl

Direct dependents

PA004W finite_bounded_injective_surjective

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 hold_i
  13. 0013intro hold_n
  14. 0014intro hnew_i
  15. 0015intro hnew_n
  16. 0016intro hpreserve
  17. 0017intro hsurjective
  18. 0018rewrite hsn at hsurjective
  19. 0019rewrite hsn at hsurjective
  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 hreflect : 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)))))))
  29. 0029exact beta_prefix_swap_last_reflect
  30. 0030specialize hreflect b
  31. 0031specialize hreflect c
  32. 0032specialize hreflect z
  33. 0033specialize hreflect d
  34. 0034specialize hreflect n
  35. 0035specialize hreflect i
  36. 0036specialize hreflect x
  37. 0037specialize hreflect y
  38. 0038have hreflect_entries : forall j a. (exists h. h + S j = S n) -> ((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a) -> ((j = i /\ a = y) \/ ((j = n /\ a = x) \/ (~(j = i) /\ (~(j = n) /\ ((exists h. h + S a = S ((S j) * c)) /\ exists q. b = q * S ((S j) * c) + a)))))
  39. 0039apply hreflect
  40. 0040exact hnew_i
  41. 0041exact hnew_n
  42. 0042exact hpreserve
  43. 0043rewrite hsn
  44. 0044rewrite hsn
  45. 0045intro a
  46. 0046intro ha
  47. 0047specialize hsurjective a
  48. 0048have hoccurs : exists j. ((exists h. h + S j = S n) /\ ((exists h. h + S a = S ((S j) * d)) /\ exists q. z = q * S ((S j) * d) + a))
  49. 0049apply hsurjective
  50. 0050exact ha
  51. 0051cases hoccurs
  52. 0052cases hoccurs_witness
  53. 0053specialize hreflect_entries x1
  54. 0054specialize hreflect_entries a
  55. 0055have hsource : ((x1 = i /\ a = y) \/ ((x1 = n /\ a = x) \/ (~(x1 = i) /\ (~(x1 = n) /\ ((exists h. h + S a = S ((S x1) * c)) /\ exists q. b = q * S ((S x1) * c) + a)))))
  56. 0056apply hreflect_entries
  57. 0057exact hoccurs_witness_left
  58. 0058exact hoccurs_witness_right
  59. 0059cases hsource
  60. 0060cases hsource_left
  61. 0061exists n
  62. 0062split
  63. 0063exact hnsn
  64. 0064rewrite hsource_left_right
  65. 0065rewrite hsource_left_right
  66. 0066exact hold_n
  67. 0067cases hsource_right
  68. 0068cases hsource_right_left
  69. 0069exists i
  70. 0070split
  71. 0071exact hisn
  72. 0072rewrite hsource_right_left_right
  73. 0073rewrite hsource_right_left_right
  74. 0074exact hold_i
  75. 0075cases hsource_right_right
  76. 0076cases hsource_right_right_right
  77. 0077exists x1
  78. 0078split
  79. 0079exact hoccurs_witness_left
  80. 0080exact hsource_right_right_right_right