		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)))))