BT00MY

add_shuffle_middle

Alpha checked-use · empty-context checked

Four additive contributions can be regrouped by swapping the middle pair.

Exact expanded PA statement

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

Structural proof guide

Four additive contributions can be regrouped by swapping the middle pair.

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

Proof neighborhood

Direct dependencies

BT0002 add_comm BT0032 add_permute_outer

Direct dependents

BT00XB add_lt_add BT00XG division_double_quotient_bit

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 (b + a) + (c + d)
  6. 0006congr
  7. 0007apply add_comm
  8. 0008refl
  9. 0009trans (c + a) + (b + d)
  10. 0010apply add_permute_outer
  11. 0011congr
  12. 0012apply add_comm
  13. 0013refl