		Search-engine friendly clone of the ACL2 documentation.

Bed-mk1

Mk-var1

Variable node constructor with basic reductions.

Signature
(mk-var1 var left right) → bed
Arguments: left — True branch for this variable ITE node.; right — False branch for this variable ITE node.
Returns: bed — A bed for var(left, right).

Definitions and Theorems

Function: mk-var1

(defun mk-var1 (var left right)
  (declare (xargs :guard t))
  (let ((__function__ 'mk-var1))
    (declare (ignorable __function__))
    (b* (((when (hons-equal left right)) left)
         ((mv lvarp lvar la ?lb)
          (bed-match-var left))
         ((mv rvarp rvar ?ra rb)
          (bed-match-var right))
         (left (if (and lvarp (equal lvar var))
                   la
                 left))
         (right (if (and rvarp (equal rvar var))
                    rb
                  right)))
      (mk-var-raw var left right))))

Theorem: bed-eval-of-mk-var1

(defthm bed-eval-of-mk-var1
  (equal (bed-eval (mk-var1 var left right) env)
         (if (bed-env-lookup var env)
             (bed-eval left env)
           (bed-eval right env))))