• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
      • Bed-op-p
      • Bed-from-aig
      • Bed-mk1
        • Mk-op-reorder
        • Bed-order
        • Mk-not
        • Mk-op1
        • Mk-op-x-x
        • Mk-op-x-true
        • Mk-op-x-false
        • Mk-op-true-x
        • Mk-op-false-x
        • Bed-match-var
        • Mk-var1
        • Mk-const-prop
        • Mk-op-raw
        • Mk-var-raw
      • Bed-eval
      • Up
      • Aig-translation
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bed-mk1

Mk-not

Construct a reduced BED for not(x).

Signature

(mk-not x) → bed

Arguments

x — Node to negate (a bed).

We do just a few straightforward reductions.

If we don't make a reduction, we use not2(t, x) as our usual way of writing not(x). This particular choice always keeps the arguments in bed-order, since t is the smallest bed in this order.

Definitions and Theorems

Function: mk-not

(defun mk-not (x)
  (declare (xargs :guard t))
  (let ((__function__ 'mk-not))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (not x))
         ((cons a b) x)
         ((unless (integerp b))
          (mk-var-raw a (mk-not (car$ b))
                      (mk-not (cdr$ b))))
         (op (bed-op-fix b))
         (left (car$ a))
         (right (cdr$ a))
         ((when (eql op (bed-op-true))) nil)
         ((when (eql op (bed-op-false))) t)
         ((when (eql op (bed-op-not1))) left)
         ((when (eql op (bed-op-not2))) right)
         ((when (eql op (bed-op-arg1)))
          (mk-not left))
         ((when (eql op (bed-op-arg2)))
          (mk-not right))
         ((when (eql op (bed-op-orc1)))
          (mk-op-raw (bed-op-andc2) left right))
         ((when (eql op (bed-op-orc2)))
          (mk-op-raw (bed-op-andc1) left right))
         ((when (eql op (bed-op-andc1)))
          (mk-op-raw (bed-op-orc2) left right))
         ((when (eql op (bed-op-andc2)))
          (mk-op-raw (bed-op-orc1) left right))
         ((when (eql op (bed-op-eqv)))
          (mk-op-raw (bed-op-xor) left right))
         ((when (eql op (bed-op-xor)))
          (mk-op-raw (bed-op-eqv) left right))
         ((when (eql op (bed-op-nand)))
          (mk-op-raw (bed-op-and) left right))
         ((when (eql op (bed-op-and)))
          (mk-op-raw (bed-op-nand) left right))
         ((when (eql op (bed-op-nor)))
          (mk-op-raw (bed-op-ior) left right))
         ((when (eql op (bed-op-ior)))
          (mk-op-raw (bed-op-nor) left right)))
      (mk-op-raw (bed-op-not2) t x))))

Theorem: bed-eval-of-mk-not

(defthm bed-eval-of-mk-not
  (equal (bed-eval (mk-not x) env)
         (b-not (bed-eval x env))))