PA005X

pow_add

Stable checked-use theorem · independently closed

Relational powers turn addition of exponents into multiplication.

Exact expanded PA statement

forall a e f s x y z. s = e + f -> (exists ff_b_add_left ff_c_add_left. ((forall ff_i_add_left_repeat. (exists ff_lt_add_left_repeat_bound. ff_lt_add_left_repeat_bound + S ff_i_add_left_repeat = e) -> (((exists ff_h_add_left_repeat_decoded. ff_h_add_left_repeat_decoded + S (a) = S ((S (ff_i_add_left_repeat)) * ff_c_add_left)) /\ exists ff_q_add_left_repeat_decoded. ff_b_add_left = ff_q_add_left_repeat_decoded * S ((S (ff_i_add_left_repeat)) * ff_c_add_left) + (a)))) /\ (exists ff_u_add_left_product ff_v_add_left_product. ((((exists ff_h_add_left_product_start. ff_h_add_left_product_start + S (1) = S ((S (0)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_start. ff_u_add_left_product = ff_q_add_left_product_start * S ((S (0)) * ff_v_add_left_product) + (1))) /\ ((((exists ff_h_add_left_product_terminal. ff_h_add_left_product_terminal + S (x) = S ((S (e)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_terminal. ff_u_add_left_product = ff_q_add_left_product_terminal * S ((S (e)) * ff_v_add_left_product) + (x))) /\ forall ff_i_add_left_product. (exists ff_lt_add_left_product_bound. ff_lt_add_left_product_bound + S ff_i_add_left_product = e) -> exists ff_p_add_left_product ff_r_add_left_product ff_s_add_left_product. ((((exists ff_h_add_left_product_factor. ff_h_add_left_product_factor + S (ff_p_add_left_product) = S ((S (ff_i_add_left_product)) * ff_c_add_left)) /\ exists ff_q_add_left_product_factor. ff_b_add_left = ff_q_add_left_product_factor * S ((S (ff_i_add_left_product)) * ff_c_add_left) + (ff_p_add_left_product))) /\ ((((exists ff_h_add_left_product_partial. ff_h_add_left_product_partial + S (ff_r_add_left_product) = S ((S (ff_i_add_left_product)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_partial. ff_u_add_left_product = ff_q_add_left_product_partial * S ((S (ff_i_add_left_product)) * ff_v_add_left_product) + (ff_r_add_left_product))) /\ ((((exists ff_h_add_left_product_successor. ff_h_add_left_product_successor + S (ff_s_add_left_product) = S ((S (S ff_i_add_left_product)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_successor. ff_u_add_left_product = ff_q_add_left_product_successor * S ((S (S ff_i_add_left_product)) * ff_v_add_left_product) + (ff_s_add_left_product))) /\ ff_s_add_left_product = ff_r_add_left_product * ff_p_add_left_product)))))))) -> (exists ff_b_add_right ff_c_add_right. ((forall ff_i_add_right_repeat. (exists ff_lt_add_right_repeat_bound. ff_lt_add_right_repeat_bound + S ff_i_add_right_repeat = f) -> (((exists ff_h_add_right_repeat_decoded. ff_h_add_right_repeat_decoded + S (a) = S ((S (ff_i_add_right_repeat)) * ff_c_add_right)) /\ exists ff_q_add_right_repeat_decoded. ff_b_add_right = ff_q_add_right_repeat_decoded * S ((S (ff_i_add_right_repeat)) * ff_c_add_right) + (a)))) /\ (exists ff_u_add_right_product ff_v_add_right_product. ((((exists ff_h_add_right_product_start. ff_h_add_right_product_start + S (1) = S ((S (0)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_start. ff_u_add_right_product = ff_q_add_right_product_start * S ((S (0)) * ff_v_add_right_product) + (1))) /\ ((((exists ff_h_add_right_product_terminal. ff_h_add_right_product_terminal + S (y) = S ((S (f)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_terminal. ff_u_add_right_product = ff_q_add_right_product_terminal * S ((S (f)) * ff_v_add_right_product) + (y))) /\ forall ff_i_add_right_product. (exists ff_lt_add_right_product_bound. ff_lt_add_right_product_bound + S ff_i_add_right_product = f) -> exists ff_p_add_right_product ff_r_add_right_product ff_s_add_right_product. ((((exists ff_h_add_right_product_factor. ff_h_add_right_product_factor + S (ff_p_add_right_product) = S ((S (ff_i_add_right_product)) * ff_c_add_right)) /\ exists ff_q_add_right_product_factor. ff_b_add_right = ff_q_add_right_product_factor * S ((S (ff_i_add_right_product)) * ff_c_add_right) + (ff_p_add_right_product))) /\ ((((exists ff_h_add_right_product_partial. ff_h_add_right_product_partial + S (ff_r_add_right_product) = S ((S (ff_i_add_right_product)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_partial. ff_u_add_right_product = ff_q_add_right_product_partial * S ((S (ff_i_add_right_product)) * ff_v_add_right_product) + (ff_r_add_right_product))) /\ ((((exists ff_h_add_right_product_successor. ff_h_add_right_product_successor + S (ff_s_add_right_product) = S ((S (S ff_i_add_right_product)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_successor. ff_u_add_right_product = ff_q_add_right_product_successor * S ((S (S ff_i_add_right_product)) * ff_v_add_right_product) + (ff_s_add_right_product))) /\ ff_s_add_right_product = ff_r_add_right_product * ff_p_add_right_product)))))))) -> (exists ff_b_add_total ff_c_add_total. ((forall ff_i_add_total_repeat. (exists ff_lt_add_total_repeat_bound. ff_lt_add_total_repeat_bound + S ff_i_add_total_repeat = s) -> (((exists ff_h_add_total_repeat_decoded. ff_h_add_total_repeat_decoded + S (a) = S ((S (ff_i_add_total_repeat)) * ff_c_add_total)) /\ exists ff_q_add_total_repeat_decoded. ff_b_add_total = ff_q_add_total_repeat_decoded * S ((S (ff_i_add_total_repeat)) * ff_c_add_total) + (a)))) /\ (exists ff_u_add_total_product ff_v_add_total_product. ((((exists ff_h_add_total_product_start. ff_h_add_total_product_start + S (1) = S ((S (0)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_start. ff_u_add_total_product = ff_q_add_total_product_start * S ((S (0)) * ff_v_add_total_product) + (1))) /\ ((((exists ff_h_add_total_product_terminal. ff_h_add_total_product_terminal + S (z) = S ((S (s)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_terminal. ff_u_add_total_product = ff_q_add_total_product_terminal * S ((S (s)) * ff_v_add_total_product) + (z))) /\ forall ff_i_add_total_product. (exists ff_lt_add_total_product_bound. ff_lt_add_total_product_bound + S ff_i_add_total_product = s) -> exists ff_p_add_total_product ff_r_add_total_product ff_s_add_total_product. ((((exists ff_h_add_total_product_factor. ff_h_add_total_product_factor + S (ff_p_add_total_product) = S ((S (ff_i_add_total_product)) * ff_c_add_total)) /\ exists ff_q_add_total_product_factor. ff_b_add_total = ff_q_add_total_product_factor * S ((S (ff_i_add_total_product)) * ff_c_add_total) + (ff_p_add_total_product))) /\ ((((exists ff_h_add_total_product_partial. ff_h_add_total_product_partial + S (ff_r_add_total_product) = S ((S (ff_i_add_total_product)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_partial. ff_u_add_total_product = ff_q_add_total_product_partial * S ((S (ff_i_add_total_product)) * ff_v_add_total_product) + (ff_r_add_total_product))) /\ ((((exists ff_h_add_total_product_successor. ff_h_add_total_product_successor + S (ff_s_add_total_product) = S ((S (S ff_i_add_total_product)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_successor. ff_u_add_total_product = ff_q_add_total_product_successor * S ((S (S ff_i_add_total_product)) * ff_v_add_total_product) + (ff_s_add_total_product))) /\ ff_s_add_total_product = ff_r_add_total_product * ff_p_add_total_product)))))))) -> z = x * y

Structural proof guide

Generated structural guide

Relational powers turn addition of exponents into multiplication.

Use the direct prerequisites pow_zero, pow_functional, pow_successor_decompose, mul_one, mul_assoc as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (4), intermediate claims (6), equality transport (7).

Referenced ingredients

PA004B pow_zero PA005G pow_functional PA004D pow_successor_decompose PA0002 mul_one PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA004B pow_zero PA005G pow_functional PA004D pow_successor_decompose PA0002 mul_one PA000B mul_assoc

Direct dependents

PA005Y pow_mul_exp

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 a
  2. 0002intro e
  3. 0003induction f
  4. 0004intro s
  5. 0005intro x
  6. 0006intro y
  7. 0007intro z
  8. 0008intro hs
  9. 0009intro hx
  10. 0010intro hy
  11. 0011intro hz
  12. 0012rewrite PA3 at hs
  13. 0013rewrite hs at hz
  14. 0014rewrite hs at hz
  15. 0015rewrite hs at hz
  16. 0016rewrite hs at hz
  17. 0017have hzx : z = x
  18. 0018specialize pow_functional a
  19. 0019specialize pow_functional e
  20. 0020specialize pow_functional z
  21. 0021specialize pow_functional x
  22. 0022apply pow_functional
  23. 0023exact hz
  24. 0024exact hx
  25. 0025have hy1 : y = 1
  26. 0026specialize pow_zero a
  27. 0027specialize pow_zero 0
  28. 0028specialize pow_zero y
  29. 0029apply pow_zero
  30. 0030refl
  31. 0031exact hy
  32. 0032rewrite hzx
  33. 0033rewrite hy1
  34. 0034specialize mul_one x
  35. 0035symm
  36. 0036exact mul_one
  37. 0037intro s
  38. 0038intro x
  39. 0039intro y
  40. 0040intro z
  41. 0041intro hs
  42. 0042intro hx
  43. 0043intro hy
  44. 0044intro hz
  45. 0045have hy_step : exists r. (exists ff_b_add_y_prefix ff_c_add_y_prefix. ((forall ff_i_add_y_prefix_repeat. (exists ff_lt_add_y_prefix_repeat_bound. ff_lt_add_y_prefix_repeat_bound + S ff_i_add_y_prefix_repeat = f) -> (((exists ff_h_add_y_prefix_repeat_decoded. ff_h_add_y_prefix_repeat_decoded + S (a) = S ((S (ff_i_add_y_prefix_repeat)) * ff_c_add_y_prefix)) /\ exists ff_q_add_y_prefix_repeat_decoded. ff_b_add_y_prefix = ff_q_add_y_prefix_repeat_decoded * S ((S (ff_i_add_y_prefix_repeat)) * ff_c_add_y_prefix) + (a)))) /\ (exists ff_u_add_y_prefix_product ff_v_add_y_prefix_product. ((((exists ff_h_add_y_prefix_product_start. ff_h_add_y_prefix_product_start + S (1) = S ((S (0)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_start. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_start * S ((S (0)) * ff_v_add_y_prefix_product) + (1))) /\ ((((exists ff_h_add_y_prefix_product_terminal. ff_h_add_y_prefix_product_terminal + S (r) = S ((S (f)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_terminal. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_terminal * S ((S (f)) * ff_v_add_y_prefix_product) + (r))) /\ forall ff_i_add_y_prefix_product. (exists ff_lt_add_y_prefix_product_bound. ff_lt_add_y_prefix_product_bound + S ff_i_add_y_prefix_product = f) -> exists ff_p_add_y_prefix_product ff_r_add_y_prefix_product ff_s_add_y_prefix_product. ((((exists ff_h_add_y_prefix_product_factor. ff_h_add_y_prefix_product_factor + S (ff_p_add_y_prefix_product) = S ((S (ff_i_add_y_prefix_product)) * ff_c_add_y_prefix)) /\ exists ff_q_add_y_prefix_product_factor. ff_b_add_y_prefix = ff_q_add_y_prefix_product_factor * S ((S (ff_i_add_y_prefix_product)) * ff_c_add_y_prefix) + (ff_p_add_y_prefix_product))) /\ ((((exists ff_h_add_y_prefix_product_partial. ff_h_add_y_prefix_product_partial + S (ff_r_add_y_prefix_product) = S ((S (ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_partial. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_partial * S ((S (ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product) + (ff_r_add_y_prefix_product))) /\ ((((exists ff_h_add_y_prefix_product_successor. ff_h_add_y_prefix_product_successor + S (ff_s_add_y_prefix_product) = S ((S (S ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_successor. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_successor * S ((S (S ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product) + (ff_s_add_y_prefix_product))) /\ ff_s_add_y_prefix_product = ff_r_add_y_prefix_product * ff_p_add_y_prefix_product)))))))) /\ y = r * a
  46. 0046specialize pow_successor_decompose a
  47. 0047specialize pow_successor_decompose f
  48. 0048specialize pow_successor_decompose (S f)
  49. 0049specialize pow_successor_decompose y
  50. 0050apply pow_successor_decompose
  51. 0051refl
  52. 0052exact hy
  53. 0053cases hy_step
  54. 0054cases hy_step_witness
  55. 0055have hst : s = S (e + f)
  56. 0056trans e + S f
  57. 0057exact hs
  58. 0058apply PA4
  59. 0059have hz_step : exists r. (exists pa_b_add_z_prefix pa_c_add_z_prefix. ((forall pa_i_add_z_prefix_repeat. (exists pa_lt_add_z_prefix_repeat_bound. pa_lt_add_z_prefix_repeat_bound + S pa_i_add_z_prefix_repeat = e + f) -> (((exists pa_h_add_z_prefix_repeat_decoded. pa_h_add_z_prefix_repeat_decoded + S (a) = S ((S (pa_i_add_z_prefix_repeat)) * pa_c_add_z_prefix)) /\ exists pa_q_add_z_prefix_repeat_decoded. pa_b_add_z_prefix = pa_q_add_z_prefix_repeat_decoded * S ((S (pa_i_add_z_prefix_repeat)) * pa_c_add_z_prefix) + (a)))) /\ (exists pa_u_add_z_prefix_product pa_v_add_z_prefix_product. ((((exists pa_h_add_z_prefix_product_start. pa_h_add_z_prefix_product_start + S (1) = S ((S (0)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_start. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_start * S ((S (0)) * pa_v_add_z_prefix_product) + (1))) /\ ((((exists pa_h_add_z_prefix_product_terminal. pa_h_add_z_prefix_product_terminal + S (r) = S ((S (e + f)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_terminal. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_terminal * S ((S (e + f)) * pa_v_add_z_prefix_product) + (r))) /\ forall pa_i_add_z_prefix_product. (exists pa_lt_add_z_prefix_product_bound. pa_lt_add_z_prefix_product_bound + S pa_i_add_z_prefix_product = e + f) -> exists pa_p_add_z_prefix_product pa_r_add_z_prefix_product pa_s_add_z_prefix_product. ((((exists pa_h_add_z_prefix_product_factor. pa_h_add_z_prefix_product_factor + S (pa_p_add_z_prefix_product) = S ((S (pa_i_add_z_prefix_product)) * pa_c_add_z_prefix)) /\ exists pa_q_add_z_prefix_product_factor. pa_b_add_z_prefix = pa_q_add_z_prefix_product_factor * S ((S (pa_i_add_z_prefix_product)) * pa_c_add_z_prefix) + (pa_p_add_z_prefix_product))) /\ ((((exists pa_h_add_z_prefix_product_partial. pa_h_add_z_prefix_product_partial + S (pa_r_add_z_prefix_product) = S ((S (pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_partial. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_partial * S ((S (pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product) + (pa_r_add_z_prefix_product))) /\ ((((exists pa_h_add_z_prefix_product_successor. pa_h_add_z_prefix_product_successor + S (pa_s_add_z_prefix_product) = S ((S (S pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_successor. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_successor * S ((S (S pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product) + (pa_s_add_z_prefix_product))) /\ pa_s_add_z_prefix_product = pa_r_add_z_prefix_product * pa_p_add_z_prefix_product)))))))) /\ z = r * a
  60. 0060specialize pow_successor_decompose a
  61. 0061specialize pow_successor_decompose (e + f)
  62. 0062specialize pow_successor_decompose s
  63. 0063specialize pow_successor_decompose z
  64. 0064apply pow_successor_decompose
  65. 0065exact hst
  66. 0066exact hz
  67. 0067cases hz_step
  68. 0068cases hz_step_witness
  69. 0069have hprefix : x2 = x * x1
  70. 0070specialize IH (e + f)
  71. 0071specialize IH x
  72. 0072specialize IH x1
  73. 0073specialize IH x2
  74. 0074apply IH
  75. 0075refl
  76. 0076exact hx
  77. 0077exact hy_step_witness_left
  78. 0078exact hz_step_witness_left
  79. 0079trans x2 * a
  80. 0080exact hz_step_witness_right
  81. 0081trans (x * x1) * a
  82. 0082congr
  83. 0083exact hprefix
  84. 0084refl
  85. 0085trans x * (x1 * a)
  86. 0086apply mul_assoc
  87. 0087congr
  88. 0088refl
  89. 0089symm
  90. 0090exact hy_step_witness_right