PA001I

add_permute_outer

Stable checked-use theorem · independently closed

Permute the outer entries of two additive pairs.

Exact expanded PA statement

forall a b c d. (a + b) + (c + d) = (c + b) + (a + d)

Structural proof guide

Generated structural guide

Permute the outer entries of two additive pairs.

Use the direct prerequisites add_assoc, add_comm as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm

Direct dependents

PA001J balanced_bezout_euclid_step PA0022 mod_eq_add PA00CQ beta_sum_pointwise_mod_three_add

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 b
  3. 0003intro c
  4. 0004intro d
  5. 0005trans a + (b + (c + d))
  6. 0006apply add_assoc
  7. 0007trans a + ((b + c) + d)
  8. 0008congr
  9. 0009refl
  10. 0010symm
  11. 0011apply add_assoc
  12. 0012trans a + ((c + b) + d)
  13. 0013congr
  14. 0014refl
  15. 0015congr
  16. 0016apply add_comm
  17. 0017refl
  18. 0018trans (a + (c + b)) + d
  19. 0019symm
  20. 0020apply add_assoc
  21. 0021trans ((c + b) + a) + d
  22. 0022congr
  23. 0023apply add_comm
  24. 0024refl
  25. 0025apply add_assoc