		Search-engine friendly clone of the ACL2 documentation.

Up-one-aux

Lift one variable through a bed (recursively).

Signature
(up-one-aux vlift bed order memo) → (mv bed order memo)
Arguments: vlift — The variable to lift.
Guard (atom vlift).; bed — The bed to lift it through.; order — Ordering for bed construction operations.; memo — Memo table mapping bed nodes to lifted equivalents.
Returns: bed — The resulting bed, equivalent to the input bed.; order — Updated order.; memo — Updated memo table.

Definitions and Theorems

Function: up-one-aux

(defun up-one-aux (vlift bed order memo)
       (declare (xargs :guard (atom vlift)))
       (let ((__function__ 'up-one-aux))
            (declare (ignorable __function__))
            (b* (((when (atom bed))
                  (mv (if bed t nil) order memo))
                 (look (hons-get bed memo))
                 ((when look) (mv (cdr look) order memo))
                 ((cons a b) bed)
                 ((unless (integerp b))
                  (b* (((when (equal a vlift))
                        (mv bed order (hons-acons bed bed memo)))
                       ((mv left order memo)
                        (up-one-aux vlift (car$ b) order memo))
                       ((mv right order memo)
                        (up-one-aux vlift (cdr$ b) order memo))
                       ((mv ans order)
                        (up-past-var vlift a left right order))
                       (memo (hons-acons bed ans memo)))
                      (mv ans order memo)))
                 (op (bed-op-fix b))
                 ((mv left order memo)
                  (up-one-aux vlift (car$ a) order memo))
                 ((mv right order memo)
                  (up-one-aux vlift (cdr$ a) order memo))
                 ((mv ans order)
                  (up-past-op vlift op left right order))
                 (memo (hons-acons bed ans memo)))
                (mv ans order memo))))