		Search-engine friendly clone of the ACL2 documentation.

Up-one

Signature
(up-one vlift bed order) → (mv bed order)
Arguments: vlift — The variable to lift.
Guard (atom vlift).; bed — The bed to lift it through.; order — The order to use.
Returns: bed — The resulting bed, equivalent to the input bed.; order — The new order to use.

Definitions and Theorems

Function: up-one

(defun up-one (vlift bed order)
       (declare (xargs :guard (atom vlift)))
       (let ((__function__ 'up-one))
            (declare (ignorable __function__))
            (b* ((memo (* 2 (fast-alist-len order)))
                 ((mv ans order memo)
                  (up-one-aux vlift bed order memo))
                 (- (fast-alist-free memo)))
                (mv ans order))))

Theorem: up-one-correct

(defthm up-one-correct
        (b* (((mv ans ?order)
              (up-one vlift bed order)))
            (implies (force (atom vlift))
                     (equal (bed-eval ans env)
                            (bed-eval bed env)))))