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