BT0032

add_permute_outer

Stable · empty-context checked

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

Permute the outer entries of two additive pairs.

Direct prerequisites: add_assoc, add_comm. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm

Direct dependents

BT0033 balanced_bezout_euclid_step BT003R mod_eq_add BT00MY add_shuffle_middle BT00Y3 beta_sum_double_carry_exact

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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