• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
      • Bed-op-p
      • Bed-from-aig
      • Bed-mk1
      • Bed-eval
      • Up
        • Up-past-op
        • Up-past-var
        • Up-one-aux
        • Up-one*
        • Up-one
      • Aig-translation
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Up

Up-past-var

Lift a variable through another (single) variable.

Signature

(up-past-var vlift vpast left right order) → (mv bed order)

Arguments

vlift — The variable we are lifting.

vpast — The variable we are lifting it past.

left — Left branch of vpast, with vlift usually at the top.

right — Right branch of vpast, with vlift usually at the top.

order — Ordering to use for bed construction.

Returns

bed — Reduced bed, equivalent (if vpast left right), but with vlift lifted to the top, if possible.

order — Updated order for canonicalization.

Definitions and Theorems

Function: up-past-var

(defun up-past-var
       (vlift vpast left right order)
       (declare (xargs :guard t))
       (let ((__function__ 'up-past-var))
            (declare (ignorable __function__))
            (b* (((mv lok lvar ltrue lfalse)
                  (bed-match-var left))
                 ((mv rok rvar rtrue rfalse)
                  (bed-match-var right))
                 ((when (and lok rok (equal lvar vlift)
                             (equal rvar vlift)))
                  (mv (mk-var1 vlift (mk-var1 vpast ltrue rtrue)
                               (mk-var1 vpast lfalse rfalse))
                      order))
                 ((when (and lok (equal lvar vlift)))
                  (mv (mk-var1 vlift (mk-var1 vpast ltrue right)
                               (mk-var1 vpast lfalse right))
                      order))
                 ((when (and rok (equal rvar vlift)))
                  (mv (mk-var1 vlift (mk-var1 vpast left rtrue)
                               (mk-var1 vpast left rfalse))
                      order)))
                (mv (mk-var1 vpast left right) order))))

Theorem: up-past-var-correct

(defthm up-past-var-correct
        (b* (((mv bed ?order)
              (up-past-var vlift vpast left right order)))
            (equal (bed-eval bed env)
                   (if (bed-env-lookup vpast env)
                       (bed-eval left env)
                       (bed-eval right env)))))