		Search-engine friendly clone of the ACL2 documentation.

Up-past-op

Lift a variable through a (single) operator.

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

Definitions and Theorems

Function: up-past-op

(defun up-past-op (vlift op left right order)
       (declare (xargs :guard (and (atom vlift) (bed-op-p op))))
       (let ((__function__ 'up-past-op))
            (declare (ignorable __function__))
            (b* ((op (bed-op-fix$ op))
                 ((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)))
                  (b* (((mv new-left order)
                        (mk-op1 op ltrue rtrue order))
                       ((mv new-right order)
                        (mk-op1 op lfalse rfalse order))
                       (ans (mk-var1 vlift new-left new-right)))
                      (mv ans order)))
                 ((when (and lok (equal lvar vlift)))
                  (b* (((mv new-left order)
                        (mk-op1 op ltrue right order))
                       ((mv new-right order)
                        (mk-op1 op lfalse right order))
                       (ans (mk-var1 vlift new-left new-right)))
                      (mv ans order)))
                 ((when (and rok (equal rvar vlift)))
                  (b* (((mv new-left order)
                        (mk-op1 op left rtrue order))
                       ((mv new-right order)
                        (mk-op1 op left rfalse order))
                       (ans (mk-var1 vlift new-left new-right)))
                      (mv ans order)))
                 ((mv ans order)
                  (mk-op1 op left right order)))
                (mv ans order))))

Theorem: up-past-op-correct

(defthm up-past-op-correct
        (implies (force (atom vlift))
                 (b* (((mv bed ?order)
                       (up-past-op vlift op left right order)))
                     (equal (bed-eval bed env)
                            (bed-op-eval op (bed-eval left env)
                                         (bed-eval right env))))))