		Search-engine friendly clone of the ACL2 documentation.

Up-one*

Signature
(up-one* vars bed order) → (mv ans order)
Arguments: vars — The variables to lift.
Guard (atom-listp vars).; bed — The bed to rewrite.; order — The order to use for bed node construction.
Returns: ans — Rewritten version of bed, equivalent to bed.; order — Resulting order.

Definitions and Theorems

Function: up-one*

(defun up-one* (vars bed order)
 (declare (xargs :guard (atom-listp vars)))
 (let ((__function__ 'up-one*))
   (declare (ignorable __function__))
   (b*
    (((when (atom vars)) (mv bed order))
     ((mv bed order)
      (time$ (up-one (car vars) bed order)
             :msg "; UP-ONE: ~st sec, ~sa bytes. (~x0 more to go)~%"
             :args (list (len (cdr vars))))))
    (up-one* (cdr vars) bed order))))

Theorem: up-one*-correct

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