		Search-engine friendly clone of the ACL2 documentation.

Up-past-var

Lift a variable through another (single) variable.

Signature
(up-past-var vlift vpast left right order) → (mv bed order)
Arguments: vlift — The variable we are lifting.; vpast — The variable we are lifting it past.; left — Left branch of vpast, with vlift usually at the top.; right — Right branch of vpast, with vlift usually at the top.; order — Ordering to use for bed construction.
Returns: bed — Reduced bed, equivalent (if vpast left right), but with vlift lifted to the top, if possible.; order — Updated order for canonicalization.

Definitions and Theorems

Function: up-past-var

(defun up-past-var (vlift vpast left right order)
  (declare (xargs :guard t))
  (let ((__function__ 'up-past-var))
    (declare (ignorable __function__))
    (b* (((mv lok lvar ltrue lfalse)
          (bed-match-var left))
         ((mv rok rvar rtrue rfalse)
          (bed-match-var right))
         ((when (and lok rok (equal lvar vlift)
                     (equal rvar vlift)))
          (mv (mk-var1 vlift (mk-var1 vpast ltrue rtrue)
                       (mk-var1 vpast lfalse rfalse))
              order))
         ((when (and lok (equal lvar vlift)))
          (mv (mk-var1 vlift (mk-var1 vpast ltrue right)
                       (mk-var1 vpast lfalse right))
              order))
         ((when (and rok (equal rvar vlift)))
          (mv (mk-var1 vlift (mk-var1 vpast left rtrue)
                       (mk-var1 vpast left rfalse))
              order)))
      (mv (mk-var1 vpast left right) order))))

Theorem: up-past-var-correct

(defthm up-past-var-correct
  (b* (((mv bed ?order)
        (up-past-var vlift vpast left right order)))
    (equal (bed-eval bed env)
           (if (bed-env-lookup vpast env)
               (bed-eval left env)
             (bed-eval right env)))))