PA004O

finite_swap_last_injective

Stable checked-use theorem · independently closed

A swap-last recoding preserves injectivity 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_inj_old fp_j_swap_inj_old fp_value_swap_inj_old. (exists fp_gap_swap_inj_old_i. fp_gap_swap_inj_old_i + S fp_i_swap_inj_old = sn) -> (exists fp_gap_swap_inj_old_j. fp_gap_swap_inj_old_j + S fp_j_swap_inj_old = sn) -> (((exists ff_h_swap_inj_old_left. ff_h_swap_inj_old_left + S (fp_value_swap_inj_old) = S ((S (fp_i_swap_inj_old)) * c)) /\ exists ff_q_swap_inj_old_left. b = ff_q_swap_inj_old_left * S ((S (fp_i_swap_inj_old)) * c) + (fp_value_swap_inj_old))) -> (((exists ff_h_swap_inj_old_right. ff_h_swap_inj_old_right + S (fp_value_swap_inj_old) = S ((S (fp_j_swap_inj_old)) * c)) /\ exists ff_q_swap_inj_old_right. b = ff_q_swap_inj_old_right * S ((S (fp_j_swap_inj_old)) * c) + (fp_value_swap_inj_old))) -> fp_i_swap_inj_old = fp_j_swap_inj_old) -> (((exists ff_h_swap_inj_old_i. ff_h_swap_inj_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_swap_inj_old_i. b = ff_q_swap_inj_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_swap_inj_old_n. ff_h_swap_inj_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_swap_inj_old_n. b = ff_q_swap_inj_old_n * S ((S (n)) * c) + (y))) -> (((exists ff_h_swap_inj_new_i. ff_h_swap_inj_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_swap_inj_new_i. z = ff_q_swap_inj_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_swap_inj_new_n. ff_h_swap_inj_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_swap_inj_new_n. z = ff_q_swap_inj_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_inj_old_j. ff_h_swap_inj_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_swap_inj_old_j. b = ff_q_swap_inj_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_swap_inj_new_j. ff_h_swap_inj_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_swap_inj_new_j. z = ff_q_swap_inj_new_j * S ((S (j)) * d) + (a)))) -> (forall fp_i_swap_inj_new fp_j_swap_inj_new fp_value_swap_inj_new. (exists fp_gap_swap_inj_new_i. fp_gap_swap_inj_new_i + S fp_i_swap_inj_new = sn) -> (exists fp_gap_swap_inj_new_j. fp_gap_swap_inj_new_j + S fp_j_swap_inj_new = sn) -> (((exists ff_h_swap_inj_new_left. ff_h_swap_inj_new_left + S (fp_value_swap_inj_new) = S ((S (fp_i_swap_inj_new)) * d)) /\ exists ff_q_swap_inj_new_left. z = ff_q_swap_inj_new_left * S ((S (fp_i_swap_inj_new)) * d) + (fp_value_swap_inj_new))) -> (((exists ff_h_swap_inj_new_right. ff_h_swap_inj_new_right + S (fp_value_swap_inj_new) = S ((S (fp_j_swap_inj_new)) * d)) /\ exists ff_q_swap_inj_new_right. z = ff_q_swap_inj_new_right * S ((S (fp_j_swap_inj_new)) * d) + (fp_value_swap_inj_new))) -> fp_i_swap_inj_new = fp_j_swap_inj_new)

Structural proof guide

Generated structural guide

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

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

The proof proceeds by case analysis (24), intermediate claims (16), equality transport (16).

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 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 hinjective
  13. 0013intro hold_i
  14. 0014intro hold_n
  15. 0015intro hnew_i
  16. 0016intro hnew_n
  17. 0017intro hpreserve
  18. 0018rewrite hsn at hinjective
  19. 0019rewrite hsn at hinjective
  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_j : 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. 0030have hreflect_k : 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)))))))
  31. 0031exact beta_prefix_swap_last_reflect
  32. 0032rewrite hsn
  33. 0033rewrite hsn
  34. 0034intro j
  35. 0035intro k
  36. 0036intro a
  37. 0037intro hj
  38. 0038intro hk
  39. 0039intro hnew_j
  40. 0040intro hnew_k
  41. 0041specialize hreflect_j b
  42. 0042specialize hreflect_j c
  43. 0043specialize hreflect_j z
  44. 0044specialize hreflect_j d
  45. 0045specialize hreflect_j n
  46. 0046specialize hreflect_j i
  47. 0047specialize hreflect_j x
  48. 0048specialize hreflect_j y
  49. 0049have hreflect_entries_j : 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)))))))
  50. 0050apply hreflect_j
  51. 0051exact hnew_i
  52. 0052exact hnew_n
  53. 0053exact hpreserve
  54. 0054specialize hreflect_entries_j j
  55. 0055specialize hreflect_entries_j a
  56. 0056have hclass_j : ((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)))))
  57. 0057apply hreflect_entries_j
  58. 0058exact hj
  59. 0059exact hnew_j
  60. 0060specialize hreflect_k b
  61. 0061specialize hreflect_k c
  62. 0062specialize hreflect_k z
  63. 0063specialize hreflect_k d
  64. 0064specialize hreflect_k n
  65. 0065specialize hreflect_k i
  66. 0066specialize hreflect_k x
  67. 0067specialize hreflect_k y
  68. 0068have hreflect_entries_k : 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)))))))
  69. 0069apply hreflect_k
  70. 0070exact hnew_i
  71. 0071exact hnew_n
  72. 0072exact hpreserve
  73. 0073specialize hreflect_entries_k k
  74. 0074specialize hreflect_entries_k a
  75. 0075have hclass_k : ((k = i /\ a = y) \/ ((k = n /\ a = x) \/ (~(k = i) /\ (~(k = n) /\ ((exists h. h + S a = S ((S k) * c)) /\ exists q. b = q * S ((S k) * c) + a)))))
  76. 0076apply hreflect_entries_k
  77. 0077exact hk
  78. 0078exact hnew_k
  79. 0079cases hclass_j
  80. 0080cases hclass_j_left
  81. 0081cases hclass_k
  82. 0082cases hclass_k_left
  83. 0083trans i
  84. 0084exact hclass_j_left_left
  85. 0085symm
  86. 0086exact hclass_k_left_left
  87. 0087cases hclass_k_right
  88. 0088cases hclass_k_right_left
  89. 0089have hxy : x = y
  90. 0090trans a
  91. 0091symm
  92. 0092exact hclass_k_right_left_right
  93. 0093exact hclass_j_left_right
  94. 0094have hin : i = n
  95. 0095specialize hinjective i
  96. 0096specialize hinjective n
  97. 0097specialize hinjective x
  98. 0098apply hinjective
  99. 0099exact hisn
  100. 0100exact hnsn
  101. 0101exact hold_i
  102. 0102rewrite hxy
  103. 0103rewrite hxy
  104. 0104exact hold_n
  105. 0105trans i
  106. 0106exact hclass_j_left_left
  107. 0107trans n
  108. 0108exact hin
  109. 0109symm
  110. 0110exact hclass_k_right_left_left
  111. 0111cases hclass_k_right_right
  112. 0112cases hclass_k_right_right_right
  113. 0113have hnk : n = k
  114. 0114specialize hinjective n
  115. 0115specialize hinjective k
  116. 0116specialize hinjective y
  117. 0117apply hinjective
  118. 0118exact hnsn
  119. 0119exact hk
  120. 0120exact hold_n
  121. 0121rewrite <- hclass_j_left_right
  122. 0122rewrite <- hclass_j_left_right
  123. 0123exact hclass_k_right_right_right_right
  124. 0124exfalso
  125. 0125apply hclass_k_right_right_right_left
  126. 0126symm
  127. 0127exact hnk
  128. 0128cases hclass_j_right
  129. 0129cases hclass_j_right_left
  130. 0130cases hclass_k
  131. 0131cases hclass_k_left
  132. 0132have hxy2 : x = y
  133. 0133trans a
  134. 0134symm
  135. 0135exact hclass_j_right_left_right
  136. 0136exact hclass_k_left_right
  137. 0137have hin2 : n = i
  138. 0138specialize hinjective n
  139. 0139specialize hinjective i
  140. 0140specialize hinjective y
  141. 0141apply hinjective
  142. 0142exact hnsn
  143. 0143exact hisn
  144. 0144exact hold_n
  145. 0145rewrite <- hxy2
  146. 0146rewrite <- hxy2
  147. 0147exact hold_i
  148. 0148trans n
  149. 0149exact hclass_j_right_left_left
  150. 0150trans i
  151. 0151exact hin2
  152. 0152symm
  153. 0153exact hclass_k_left_left
  154. 0154cases hclass_k_right
  155. 0155cases hclass_k_right_left
  156. 0156trans n
  157. 0157exact hclass_j_right_left_left
  158. 0158symm
  159. 0159exact hclass_k_right_left_left
  160. 0160cases hclass_k_right_right
  161. 0161cases hclass_k_right_right_right
  162. 0162have hik : i = k
  163. 0163specialize hinjective i
  164. 0164specialize hinjective k
  165. 0165specialize hinjective x
  166. 0166apply hinjective
  167. 0167exact hisn
  168. 0168exact hk
  169. 0169exact hold_i
  170. 0170rewrite <- hclass_j_right_left_right
  171. 0171rewrite <- hclass_j_right_left_right
  172. 0172exact hclass_k_right_right_right_right
  173. 0173exfalso
  174. 0174apply hclass_k_right_right_left
  175. 0175symm
  176. 0176exact hik
  177. 0177cases hclass_j_right_right
  178. 0178cases hclass_j_right_right_right
  179. 0179cases hclass_k
  180. 0180cases hclass_k_left
  181. 0181have hjn : j = n
  182. 0182specialize hinjective j
  183. 0183specialize hinjective n
  184. 0184specialize hinjective y
  185. 0185apply hinjective
  186. 0186exact hj
  187. 0187exact hnsn
  188. 0188rewrite <- hclass_k_left_right
  189. 0189rewrite <- hclass_k_left_right
  190. 0190exact hclass_j_right_right_right_right
  191. 0191exact hold_n
  192. 0192exfalso
  193. 0193apply hclass_j_right_right_right_left
  194. 0194exact hjn
  195. 0195cases hclass_k_right
  196. 0196cases hclass_k_right_left
  197. 0197have hji : j = i
  198. 0198specialize hinjective j
  199. 0199specialize hinjective i
  200. 0200specialize hinjective x
  201. 0201apply hinjective
  202. 0202exact hj
  203. 0203exact hisn
  204. 0204rewrite <- hclass_k_right_left_right
  205. 0205rewrite <- hclass_k_right_left_right
  206. 0206exact hclass_j_right_right_right_right
  207. 0207exact hold_i
  208. 0208exfalso
  209. 0209apply hclass_j_right_right_left
  210. 0210exact hji
  211. 0211cases hclass_k_right_right
  212. 0212cases hclass_k_right_right_right
  213. 0213specialize hinjective j
  214. 0214specialize hinjective k
  215. 0215specialize hinjective a
  216. 0216apply hinjective
  217. 0217exact hj
  218. 0218exact hk
  219. 0219exact hclass_j_right_right_right_right
  220. 0220exact hclass_k_right_right_right_right