		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-easy-bindings-main

Signature
(svtv-easy-bindings-main x svtv) → *
Arguments: x — Some arguments to easy-bindings.; svtv — Guard (svtv-p svtv).

Definitions and Theorems

Function: svtv-easy-bindings-main

(defun svtv-easy-bindings-main (x svtv)
 (declare (xargs :guard (svtv-p svtv)))
 (let ((__function__ 'svtv-easy-bindings-main))
  (declare (ignorable __function__))
  (cond
   ((atom x) nil)
   ((symbolp (car x))
    (cons (cons ':nat
                (cons (car x)
                      (cons (svtv->in-width (car x) svtv)
                            'nil)))
          (svtv-easy-bindings-main (cdr x) svtv)))
   ((atom (car x))
    (raise "Illegal argumen to svtv-easy-bindings: ~x0"
           (car x)))
   ((or (eq (caar x) :nat)
        (eq (caar x) :int)
        (eq (caar x) :bool)
        (eq (caar x) :skip))
    (cons (car x)
          (svtv-easy-bindings-main (cdr x) svtv)))
   ((or (eq (caar x) :mix)
        (eq (caar x) :seq))
    (let ((elems (cdar x)))
      (cons (cons (caar x)
                  (svtv-easy-bindings-main elems svtv))
            (svtv-easy-bindings-main (cdr x)
                                     svtv))))
   ((eq (caar x) :rev)
    (cons (cons :rev (svtv-easy-bindings-main (cdar x) svtv))
          (svtv-easy-bindings-main (cdr x) svtv)))
   (t
    (raise
     "Arguments to svtv-easy-bindings should be input names or ~
                 a :mix, :seq, or :rev form, so ~x0 is illegal."
     (car x))))))

Theorem: svtv-easy-bindings-main-of-svtv-fix-svtv

(defthm svtv-easy-bindings-main-of-svtv-fix-svtv
  (equal (svtv-easy-bindings-main x (svtv-fix svtv))
         (svtv-easy-bindings-main x svtv)))

Theorem: svtv-easy-bindings-main-svtv-equiv-congruence-on-svtv

(defthm svtv-easy-bindings-main-svtv-equiv-congruence-on-svtv
  (implies (svtv-equiv svtv svtv-equiv)
           (equal (svtv-easy-bindings-main x svtv)
                  (svtv-easy-bindings-main x svtv-equiv)))
  :rule-classes :congruence)