Theorem band-commutativity

• Type: A user defined theorem
• Validity: The proof is valid.
• Features: simp, localsimp,
• Comment:
• Used by: band-011x, band-011x-eq, band-011x-is-unsigned, band-011x-is-unsigned-03, band-011x-is-unsigned-fix, band-011x-is-unsigned-fix-01, band-011x-is-unsigned-fix-02, band-011x-neg, band-011x-neg-01, band-011x-neg-02, band-011x-neg-04, band-011x-pos-01, band-011x-pos-02, band-011x-zero, band-255-neg, band-255-pos, band-32-not-neg, band-63-lezero, band-65535-neg, band-65535-pos, band-idempotent, band-le-zero, band-ls-zero-01, band-max-01, band-max-02, band-max-03, band-max-04, band-max-05, band-max-06, band-min-01, band-min-02, band-mod256-neg, band-mod256-pos, band-notneg, band-num, bor-assoc, bor-bitlength, bor-com, bor-notAndNot, bor-zero, bxor-bitlength, bxor-com, bxor-minus-one, bxor-zero, cast-law-leftshift, cast-law-or-one, cast-law-shift-snd-l, cast-law-shift-snd-r, cast-law-shift-snd-zr, cast-law-xor-one, divide-by-10, intshiftleft-band31, intshiftleft-is-shiftleft, intshiftleft-num, intshiftright-def-unbounded, intshiftright-ls-02, intshiftright-mone, intshiftright-unbounded-same, intshiftrsign-abs-le, intshiftrsign-band31, intshiftrsign-num, intshiftrsign-rec-neg, intshiftrsign-rec-pos, intshiftrsign-zero, intshiftrsign-zero-01, intshiftrsign32, intshiftrzero-prop-01, intshiftzero-def-unbounded, intshiftzero-mone, longshiftright-2pot-pos, longshiftright-def-unbounded, longshiftzero-band-63, longshiftzero-carry, longshiftzero-carry-01, longshiftzero-def-pos, longshiftzero-def-unbounded, longshiftzero-not-neg-01, longshiftzero-pos, longshiftzero-zero-02, longshiftzero-zero-03,
• Used by units in proved state: bytes, byte,
• Proof exists?: Yes

View the proof

Infos about the proof

• Proved?: Yes
• Interactions: 1
• Proof steps: 2
• Used lemmas: and-com, band-associativity, band-def,
• Used spec theorems:
  • Used simplifier rules:
    • int2bits/int2bits-not-empty