		Search-engine friendly clone of the ACL2 documentation.

Logops-bit-functions

Simplify-bit-functions

Rewrite: Simplification rules for all binary b- functions including commutative rules, reductions with 1 explicit value, and reductions for identical agruments and complemented arguments.

Definitions and Theorems

Theorem: simplify-bit-functions

(defthm simplify-bit-functions
  (and (equal (b-and x y) (b-and y x))
       (equal (b-and 0 x) 0)
       (equal (b-and 1 x) (bfix x))
       (equal (b-and x x) (bfix x))
       (equal (b-and x (b-not x)) 0)
       (equal (b-ior x y) (b-ior y x))
       (equal (b-ior 0 x) (bfix x))
       (equal (b-ior 1 x) 1)
       (equal (b-ior x x) (bfix x))
       (equal (b-ior x (b-not x)) 1)
       (equal (b-xor x y) (b-xor y x))
       (equal (b-xor 0 x) (bfix x))
       (equal (b-xor 1 x) (b-not x))
       (equal (b-xor x x) 0)
       (equal (b-xor x (b-not x)) 1)
       (equal (b-eqv x y) (b-eqv y x))
       (equal (b-eqv 0 x) (b-not x))
       (equal (b-eqv 1 x) (bfix x))
       (equal (b-eqv x x) 1)
       (equal (b-eqv x (b-not x)) 0)
       (equal (b-nand x y) (b-nand y x))
       (equal (b-nand 0 x) 1)
       (equal (b-nand 1 x) (b-not x))
       (equal (b-nand x x) (b-not x))
       (equal (b-nand x (b-not x)) 1)
       (equal (b-nor x y) (b-nor y x))
       (equal (b-nor 0 x) (b-not x))
       (equal (b-nor 1 x) 0)
       (equal (b-nor x x) (b-not x))
       (equal (b-nor x (b-not x)) 0)
       (equal (b-andc1 0 x) (bfix x))
       (equal (b-andc1 x 0) 0)
       (equal (b-andc1 1 x) 0)
       (equal (b-andc1 x 1) (b-not x))
       (equal (b-andc1 x x) 0)
       (equal (b-andc1 x (b-not x)) (b-not x))
       (equal (b-andc1 (b-not x) x) (bfix x))
       (equal (b-andc2 0 x) 0)
       (equal (b-andc2 x 0) (bfix x))
       (equal (b-andc2 1 x) (b-not x))
       (equal (b-andc2 x 1) 0)
       (equal (b-andc2 x x) 0)
       (equal (b-andc2 x (b-not x)) (bfix x))
       (equal (b-andc2 (b-not x) x) (b-not x))
       (equal (b-orc1 0 x) 1)
       (equal (b-orc1 x 0) (b-not x))
       (equal (b-orc1 1 x) (bfix x))
       (equal (b-orc1 x 1) 1)
       (equal (b-orc1 x x) 1)
       (equal (b-orc1 x (b-not x)) (b-not x))
       (equal (b-orc1 (b-not x) x) (bfix x))
       (equal (b-orc2 0 x) (b-not x))
       (equal (b-orc2 x 0) 1)
       (equal (b-orc2 1 x) 1)
       (equal (b-orc2 x 1) (bfix x))
       (equal (b-orc2 x x) 1)
       (equal (b-orc2 x (b-not x)) (bfix x))
       (equal (b-orc2 (b-not x) x) (b-not x))
       (equal (b-ite 1 then else) (bfix then))
       (equal (b-ite 0 then else) (bfix else))
       (equal (b-ite test 1 0) (bfix test))
       (equal (b-ite test 0 1) (b-not test))
       (equal (b-ite test then then)
              (bfix then))
       (equal (b-ite test then 0)
              (b-and test then))
       (equal (b-ite test then 1)
              (b-ior (b-not test) then))
       (equal (b-ite test then test)
              (b-and test then))
       (equal (b-ite test 1 else)
              (b-ior test else))
       (equal (b-ite test 0 else)
              (b-and (b-not test) else))
       (equal (b-ite test test else)
              (b-ior test else))))