		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Mk-op1

Operator node constructor with basic reductions.

Signature
(mk-op1 op left right order) → (mv bed order)
Arguments: op — Guard (bed-op-p op).; left — First argument to the operator (a bed).; right — Second argument to the operator (a bed).; order — The ordering for bed-order.
Returns: bed — A bed for op(left, right).; order — The (perhaps extended) order.

Definitions and Theorems

Function: mk-op1

(defun mk-op1 (op left right order)
  (declare (xargs :guard (bed-op-p op)))
  (let ((__function__ 'mk-op1))
    (declare (ignorable __function__))
    (b* ((op (bed-op-fix$ op))
         ((when (eql op (bed-op-true)))
          (mv t order))
         ((when (eql op (bed-op-false)))
          (mv nil order))
         ((when (eql op (bed-op-arg1)))
          (mv left order))
         ((when (eql op (bed-op-arg2)))
          (mv right order))
         ((when (or (atom left) (atom right)))
          (mv (cond ((and (atom left) (atom right))
                     (mk-const-prop op left right))
                    ((atom left)
                     (if left (mk-op-true-x op right)
                       (mk-op-false-x op right)))
                    (t (if right (mk-op-x-true op left)
                         (mk-op-x-false op left))))
              order))
         ((when (hons-equal left right))
          (mv (mk-op-x-x op left) order)))
      (mk-op-reorder op left right order))))

Theorem: bed-eval-of-mk-op1

(defthm bed-eval-of-mk-op1
  (b* (((mv bed &)
        (mk-op1 op left right order)))
    (equal (bed-eval bed env)
           (bed-op-eval op (bed-eval left env)
                        (bed-eval right env)))))