PA00CV

beta_sum_swap_last_invariant

Alpha v16 checked-use theorem · independently closed; not Stable

Swapping an interior beta-coded summand with the last summand preserves the exact finite sum.

Exact expanded PA statement

forall b c z d n i x y p q. (exists h. h + S i = n) -> (((exists ff_h_product_swap_old_i. ff_h_product_swap_old_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_product_swap_old_i. b = ff_q_product_swap_old_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_product_swap_old_n. ff_h_product_swap_old_n + S (y) = S ((S (n)) * c)) /\ exists ff_q_product_swap_old_n. b = ff_q_product_swap_old_n * S ((S (n)) * c) + (y))) -> (((exists ff_h_product_swap_new_i. ff_h_product_swap_new_i + S (y) = S ((S (i)) * d)) /\ exists ff_q_product_swap_new_i. z = ff_q_product_swap_new_i * S ((S (i)) * d) + (y))) -> (((exists ff_h_product_swap_new_n. ff_h_product_swap_new_n + S (x) = S ((S (n)) * d)) /\ exists ff_q_product_swap_new_n. z = ff_q_product_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_product_swap_old_j. ff_h_product_swap_old_j + S (a) = S ((S (j)) * c)) /\ exists ff_q_product_swap_old_j. b = ff_q_product_swap_old_j * S ((S (j)) * c) + (a))) -> (((exists ff_h_product_swap_new_j. ff_h_product_swap_new_j + S (a) = S ((S (j)) * d)) /\ exists ff_q_product_swap_new_j. z = ff_q_product_swap_new_j * S ((S (j)) * d) + (a)))) -> (exists ff_u_product_swap_old ff_v_product_swap_old. ((((exists ff_h_product_swap_old_start. ff_h_product_swap_old_start + S (0) = S ((S (0)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_start. ff_u_product_swap_old = ff_q_product_swap_old_start * S ((S (0)) * ff_v_product_swap_old) + (0))) /\ ((((exists ff_h_product_swap_old_terminal. ff_h_product_swap_old_terminal + S (p) = S ((S (S n)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_terminal. ff_u_product_swap_old = ff_q_product_swap_old_terminal * S ((S (S n)) * ff_v_product_swap_old) + (p))) /\ forall ff_i_product_swap_old. (exists ff_lt_product_swap_old_bound. ff_lt_product_swap_old_bound + S ff_i_product_swap_old = S n) -> exists ff_a_product_swap_old ff_r_product_swap_old ff_s_product_swap_old. ((((exists ff_h_product_swap_old_summand. ff_h_product_swap_old_summand + S (ff_a_product_swap_old) = S ((S (ff_i_product_swap_old)) * c)) /\ exists ff_q_product_swap_old_summand. b = ff_q_product_swap_old_summand * S ((S (ff_i_product_swap_old)) * c) + (ff_a_product_swap_old))) /\ ((((exists ff_h_product_swap_old_partial. ff_h_product_swap_old_partial + S (ff_r_product_swap_old) = S ((S (ff_i_product_swap_old)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_partial. ff_u_product_swap_old = ff_q_product_swap_old_partial * S ((S (ff_i_product_swap_old)) * ff_v_product_swap_old) + (ff_r_product_swap_old))) /\ ((((exists ff_h_product_swap_old_successor. ff_h_product_swap_old_successor + S (ff_s_product_swap_old) = S ((S (S ff_i_product_swap_old)) * ff_v_product_swap_old)) /\ exists ff_q_product_swap_old_successor. ff_u_product_swap_old = ff_q_product_swap_old_successor * S ((S (S ff_i_product_swap_old)) * ff_v_product_swap_old) + (ff_s_product_swap_old))) /\ ff_s_product_swap_old = ff_r_product_swap_old + ff_a_product_swap_old)))))) -> (exists ff_u_product_swap_new ff_v_product_swap_new. ((((exists ff_h_product_swap_new_start. ff_h_product_swap_new_start + S (0) = S ((S (0)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_start. ff_u_product_swap_new = ff_q_product_swap_new_start * S ((S (0)) * ff_v_product_swap_new) + (0))) /\ ((((exists ff_h_product_swap_new_terminal. ff_h_product_swap_new_terminal + S (q) = S ((S (S n)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_terminal. ff_u_product_swap_new = ff_q_product_swap_new_terminal * S ((S (S n)) * ff_v_product_swap_new) + (q))) /\ forall ff_i_product_swap_new. (exists ff_lt_product_swap_new_bound. ff_lt_product_swap_new_bound + S ff_i_product_swap_new = S n) -> exists ff_a_product_swap_new ff_r_product_swap_new ff_s_product_swap_new. ((((exists ff_h_product_swap_new_summand. ff_h_product_swap_new_summand + S (ff_a_product_swap_new) = S ((S (ff_i_product_swap_new)) * d)) /\ exists ff_q_product_swap_new_summand. z = ff_q_product_swap_new_summand * S ((S (ff_i_product_swap_new)) * d) + (ff_a_product_swap_new))) /\ ((((exists ff_h_product_swap_new_partial. ff_h_product_swap_new_partial + S (ff_r_product_swap_new) = S ((S (ff_i_product_swap_new)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_partial. ff_u_product_swap_new = ff_q_product_swap_new_partial * S ((S (ff_i_product_swap_new)) * ff_v_product_swap_new) + (ff_r_product_swap_new))) /\ ((((exists ff_h_product_swap_new_successor. ff_h_product_swap_new_successor + S (ff_s_product_swap_new) = S ((S (S ff_i_product_swap_new)) * ff_v_product_swap_new)) /\ exists ff_q_product_swap_new_successor. ff_u_product_swap_new = ff_q_product_swap_new_successor * S ((S (S ff_i_product_swap_new)) * ff_v_product_swap_new) + (ff_s_product_swap_new))) /\ ff_s_product_swap_new = ff_r_product_swap_new + ff_a_product_swap_new)))))) -> p = q

Structural proof guide

Generated structural guide

Swapping an interior beta-coded summand with the last summand preserves the exact finite sum.

Use the direct prerequisites beta_sum_replace_balance, beta_sum_succ_decompose, beta_at_unique, le_succ, le_refl, lt_irrefl_expanded as previously established PA formulas.

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

Referenced ingredients

PA00CU beta_sum_replace_balance PA003Y beta_sum_succ_decompose PA002F beta_at_unique PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Proof neighborhood

Direct dependencies

PA00CU beta_sum_replace_balance PA003Y beta_sum_succ_decompose PA002F beta_at_unique PA002O le_succ PA001A le_refl PA0010 lt_irrefl_expanded

Direct dependents

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 Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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 p
  10. 0010intro q
  11. 0011intro hi
  12. 0012intro hold_i
  13. 0013intro hold_n
  14. 0014intro hnew_i
  15. 0015intro hnew_n
  16. 0016intro hpreserve
  17. 0017intro hproduct_old
  18. 0018intro hproduct_new
  19. 0019have hold_decomp : exists a r. (((exists ff_h_swap_old_last. ff_h_swap_old_last + S (a) = S ((S (n)) * c)) /\ exists ff_q_swap_old_last. b = ff_q_swap_old_last * S ((S (n)) * c) + (a))) /\ ((exists ff_u_swap_old_prefix ff_v_swap_old_prefix. ((((exists ff_h_swap_old_prefix_start. ff_h_swap_old_prefix_start + S (0) = S ((S (0)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_start. ff_u_swap_old_prefix = ff_q_swap_old_prefix_start * S ((S (0)) * ff_v_swap_old_prefix) + (0))) /\ ((((exists ff_h_swap_old_prefix_terminal. ff_h_swap_old_prefix_terminal + S (r) = S ((S (n)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_terminal. ff_u_swap_old_prefix = ff_q_swap_old_prefix_terminal * S ((S (n)) * ff_v_swap_old_prefix) + (r))) /\ forall ff_i_swap_old_prefix. (exists ff_lt_swap_old_prefix_bound. ff_lt_swap_old_prefix_bound + S ff_i_swap_old_prefix = n) -> exists ff_a_swap_old_prefix ff_r_swap_old_prefix ff_s_swap_old_prefix. ((((exists ff_h_swap_old_prefix_summand. ff_h_swap_old_prefix_summand + S (ff_a_swap_old_prefix) = S ((S (ff_i_swap_old_prefix)) * c)) /\ exists ff_q_swap_old_prefix_summand. b = ff_q_swap_old_prefix_summand * S ((S (ff_i_swap_old_prefix)) * c) + (ff_a_swap_old_prefix))) /\ ((((exists ff_h_swap_old_prefix_partial. ff_h_swap_old_prefix_partial + S (ff_r_swap_old_prefix) = S ((S (ff_i_swap_old_prefix)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_partial. ff_u_swap_old_prefix = ff_q_swap_old_prefix_partial * S ((S (ff_i_swap_old_prefix)) * ff_v_swap_old_prefix) + (ff_r_swap_old_prefix))) /\ ((((exists ff_h_swap_old_prefix_successor. ff_h_swap_old_prefix_successor + S (ff_s_swap_old_prefix) = S ((S (S ff_i_swap_old_prefix)) * ff_v_swap_old_prefix)) /\ exists ff_q_swap_old_prefix_successor. ff_u_swap_old_prefix = ff_q_swap_old_prefix_successor * S ((S (S ff_i_swap_old_prefix)) * ff_v_swap_old_prefix) + (ff_s_swap_old_prefix))) /\ ff_s_swap_old_prefix = ff_r_swap_old_prefix + ff_a_swap_old_prefix)))))) /\ p = r + a)
  20. 0020specialize beta_sum_succ_decompose b
  21. 0021specialize beta_sum_succ_decompose c
  22. 0022specialize beta_sum_succ_decompose n
  23. 0023specialize beta_sum_succ_decompose p
  24. 0024apply beta_sum_succ_decompose
  25. 0025exact hproduct_old
  26. 0026have hnew_decomp : exists a r. (((exists ff_h_swap_new_last. ff_h_swap_new_last + S (a) = S ((S (n)) * d)) /\ exists ff_q_swap_new_last. z = ff_q_swap_new_last * S ((S (n)) * d) + (a))) /\ ((exists ff_u_swap_new_prefix ff_v_swap_new_prefix. ((((exists ff_h_swap_new_prefix_start. ff_h_swap_new_prefix_start + S (0) = S ((S (0)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_start. ff_u_swap_new_prefix = ff_q_swap_new_prefix_start * S ((S (0)) * ff_v_swap_new_prefix) + (0))) /\ ((((exists ff_h_swap_new_prefix_terminal. ff_h_swap_new_prefix_terminal + S (r) = S ((S (n)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_terminal. ff_u_swap_new_prefix = ff_q_swap_new_prefix_terminal * S ((S (n)) * ff_v_swap_new_prefix) + (r))) /\ forall ff_i_swap_new_prefix. (exists ff_lt_swap_new_prefix_bound. ff_lt_swap_new_prefix_bound + S ff_i_swap_new_prefix = n) -> exists ff_a_swap_new_prefix ff_r_swap_new_prefix ff_s_swap_new_prefix. ((((exists ff_h_swap_new_prefix_summand. ff_h_swap_new_prefix_summand + S (ff_a_swap_new_prefix) = S ((S (ff_i_swap_new_prefix)) * d)) /\ exists ff_q_swap_new_prefix_summand. z = ff_q_swap_new_prefix_summand * S ((S (ff_i_swap_new_prefix)) * d) + (ff_a_swap_new_prefix))) /\ ((((exists ff_h_swap_new_prefix_partial. ff_h_swap_new_prefix_partial + S (ff_r_swap_new_prefix) = S ((S (ff_i_swap_new_prefix)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_partial. ff_u_swap_new_prefix = ff_q_swap_new_prefix_partial * S ((S (ff_i_swap_new_prefix)) * ff_v_swap_new_prefix) + (ff_r_swap_new_prefix))) /\ ((((exists ff_h_swap_new_prefix_successor. ff_h_swap_new_prefix_successor + S (ff_s_swap_new_prefix) = S ((S (S ff_i_swap_new_prefix)) * ff_v_swap_new_prefix)) /\ exists ff_q_swap_new_prefix_successor. ff_u_swap_new_prefix = ff_q_swap_new_prefix_successor * S ((S (S ff_i_swap_new_prefix)) * ff_v_swap_new_prefix) + (ff_s_swap_new_prefix))) /\ ff_s_swap_new_prefix = ff_r_swap_new_prefix + ff_a_swap_new_prefix)))))) /\ q = r + a)
  27. 0027specialize beta_sum_succ_decompose z
  28. 0028specialize beta_sum_succ_decompose d
  29. 0029specialize beta_sum_succ_decompose n
  30. 0030specialize beta_sum_succ_decompose q
  31. 0031apply beta_sum_succ_decompose
  32. 0032exact hproduct_new
  33. 0033cases hold_decomp
  34. 0034cases hold_decomp_witness
  35. 0035cases hold_decomp_witness_witness
  36. 0036cases hold_decomp_witness_witness_right
  37. 0037cases hnew_decomp
  38. 0038cases hnew_decomp_witness
  39. 0039cases hnew_decomp_witness_witness
  40. 0040cases hnew_decomp_witness_witness_right
  41. 0041have hold_last : x1 = y
  42. 0042specialize beta_at_unique b
  43. 0043specialize beta_at_unique c
  44. 0044specialize beta_at_unique n
  45. 0045specialize beta_at_unique x1
  46. 0046specialize beta_at_unique y
  47. 0047apply beta_at_unique
  48. 0048exact hold_decomp_witness_witness_left
  49. 0049exact hold_n
  50. 0050have hnew_last : x3 = x
  51. 0051specialize beta_at_unique z
  52. 0052specialize beta_at_unique d
  53. 0053specialize beta_at_unique n
  54. 0054specialize beta_at_unique x3
  55. 0055specialize beta_at_unique x
  56. 0056apply beta_at_unique
  57. 0057exact hnew_decomp_witness_witness_left
  58. 0058exact hnew_n
  59. 0059have hprefix_preserve : forall j a. (exists h. h + S j = n) -> ~(j = i) -> ((exists h. h + S a = S ((S j) * c)) /\ exists w. b = w * S ((S j) * c) + a) -> ((exists h. h + S a = S ((S j) * d)) /\ exists w. z = w * S ((S j) * d) + a)
  60. 0060intro j
  61. 0061intro a
  62. 0062intro hj
  63. 0063intro hji
  64. 0064intro hold
  65. 0065specialize hpreserve j
  66. 0066specialize hpreserve a
  67. 0067apply hpreserve
  68. 0068specialize le_succ (S j)
  69. 0069specialize le_succ n
  70. 0070apply le_succ
  71. 0071exact hj
  72. 0072exact hji
  73. 0073intro hjn
  74. 0074specialize lt_irrefl_expanded n
  75. 0075apply lt_irrefl_expanded
  76. 0076rewrite hjn at hj
  77. 0077exact hj
  78. 0078exact hold
  79. 0079have hbalance : x4 + x = x2 + y
  80. 0080specialize beta_sum_replace_balance n
  81. 0081specialize beta_sum_replace_balance b
  82. 0082specialize beta_sum_replace_balance c
  83. 0083specialize beta_sum_replace_balance z
  84. 0084specialize beta_sum_replace_balance d
  85. 0085specialize beta_sum_replace_balance i
  86. 0086specialize beta_sum_replace_balance x
  87. 0087specialize beta_sum_replace_balance y
  88. 0088specialize beta_sum_replace_balance x2
  89. 0089specialize beta_sum_replace_balance x4
  90. 0090apply beta_sum_replace_balance
  91. 0091exact hi
  92. 0092exact hold_i
  93. 0093exact hnew_i
  94. 0094exact hprefix_preserve
  95. 0095exact hold_decomp_witness_witness_right_left
  96. 0096exact hnew_decomp_witness_witness_right_left
  97. 0097rewrite hold_decomp_witness_witness_right_right
  98. 0098rewrite hnew_decomp_witness_witness_right_right
  99. 0099rewrite hold_last
  100. 0100rewrite hnew_last
  101. 0101symm
  102. 0102exact hbalance