• 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
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Bed-mk1

Mk-op-x-true

Construct a reduced BED for op(left, true).

Signature

(mk-op-x-true op left) → bed

Arguments

op — The operator being applied.
    Guard (bed-op-p op).

left — First argument to the operator (a bed).

Definitions and Theorems

Function: mk-op-x-true

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

Theorem: bed-eval-of-mk-op-x-true

(defthm bed-eval-of-mk-op-x-true
  (equal (bed-eval (mk-op-x-true op left) env)
         (bed-eval (mk-op-raw op left t) env)))