		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-surjmaps-args

Signature
(expdata-process-surjmaps-args formals arg-surjmaps surjmap-id) → new-arg-surjmaps
Arguments: formals — Guard (symbol-listp formals).; arg-surjmaps — Guard (expdata-symbol-surjmap-alistp arg-surjmaps).; surjmap-id — Guard (expdata-surjmapp surjmap-id).
Returns: new-arg-surjmaps — Type (expdata-symbol-surjmap-alistp new-arg-surjmaps), given the guard.

Definitions and Theorems

Function: expdata-process-surjmaps-args

(defun expdata-process-surjmaps-args
       (formals arg-surjmaps surjmap-id)
 (declare
     (xargs :guard (and (symbol-listp formals)
                        (expdata-symbol-surjmap-alistp arg-surjmaps)
                        (expdata-surjmapp surjmap-id))))
 (let ((__function__ 'expdata-process-surjmaps-args))
  (declare (ignorable __function__))
  (b* (((when (endp formals)) nil)
       (pair (assoc-eq (car formals) arg-surjmaps)))
   (if
     (consp pair)
     (cons pair
           (expdata-process-surjmaps-args (cdr formals)
                                          arg-surjmaps surjmap-id))
    (acons
        (car formals)
        surjmap-id
        (expdata-process-surjmaps-args (cdr formals)
                                       arg-surjmaps surjmap-id))))))

Theorem: expdata-symbol-surjmap-alistp-of-expdata-process-surjmaps-args

(defthm
     expdata-symbol-surjmap-alistp-of-expdata-process-surjmaps-args
 (implies
      (and (symbol-listp formals)
           (expdata-symbol-surjmap-alistp arg-surjmaps)
           (expdata-surjmapp surjmap-id))
      (b* ((new-arg-surjmaps (expdata-process-surjmaps-args
                                  formals arg-surjmaps surjmap-id)))
        (expdata-symbol-surjmap-alistp new-arg-surjmaps)))
 :rule-classes :rewrite)