BT011P

bertrand_add_six_permute

Alpha body-checked · checked-use disabled

Normalize the six addends used by the 163-to-317 cover.

Exact expanded PA statement

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

Structural proof guide

Normalize the six addends used by the 163-to-317 cover.

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

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT011O bertrand_add_swap_nested

Direct dependents

BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one

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. 0005intro e
  6. 0006intro f
  7. 0007trans (a + (b + (c + d))) + (e + f)
  8. 0008congr
  9. 0009apply add_assoc
  10. 0010refl
  11. 0011trans a + ((b + (c + d)) + (e + f))
  12. 0012apply add_assoc
  13. 0013trans a + (b + ((c + d) + (e + f)))
  14. 0014congr
  15. 0015refl
  16. 0016apply add_assoc
  17. 0017trans a + (b + (c + (d + (e + f))))
  18. 0018congr
  19. 0019refl
  20. 0020congr
  21. 0021refl
  22. 0022apply add_assoc
  23. 0023trans a + (b + (c + (e + (d + f))))
  24. 0024congr
  25. 0025refl
  26. 0026congr
  27. 0027refl
  28. 0028congr
  29. 0029refl
  30. 0030apply bertrand_add_swap_nested
  31. 0031trans a + (b + (e + (c + (d + f))))
  32. 0032congr
  33. 0033refl
  34. 0034congr
  35. 0035refl
  36. 0036apply bertrand_add_swap_nested
  37. 0037trans a + (e + (b + (c + (d + f))))
  38. 0038congr
  39. 0039refl
  40. 0040apply bertrand_add_swap_nested
  41. 0041trans (a + e) + (b + (c + (d + f)))
  42. 0042symm
  43. 0043apply add_assoc
  44. 0044trans (a + e) + ((b + c) + (d + f))
  45. 0045congr
  46. 0046refl
  47. 0047symm
  48. 0048apply add_assoc
  49. 0049refl