		Search-engine friendly clone of the ACL2 documentation.

Expdata-input-processing

Expdata-process-surjmaps-ress

Signature
(expdata-process-surjmaps-ress j m res-surjmaps surjmap-id) → new-res-surjmaps
Arguments: j — Guard (posp j).; m — Guard (posp m).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; surjmap-id — Guard (expdata-surjmapp surjmap-id).
Returns: new-res-surjmaps — Type (expdata-pos-surjmap-alistp new-res-surjmaps), given the guard.

Definitions and Theorems

Function: expdata-process-surjmaps-ress

(defun expdata-process-surjmaps-ress (j m res-surjmaps surjmap-id)
 (declare
      (xargs :guard (and (posp j)
                         (posp m)
                         (expdata-pos-surjmap-alistp res-surjmaps)
                         (expdata-surjmapp surjmap-id))))
 (let ((__function__ 'expdata-process-surjmaps-ress))
  (declare (ignorable __function__))
  (b* (((unless (mbt (and (posp j) (posp m))))
        nil)
       ((when (> j m)) nil)
       (pair (assoc j res-surjmaps)))
   (if
    (consp pair)
    (cons pair
          (expdata-process-surjmaps-ress (1+ j)
                                         m res-surjmaps surjmap-id))
    (acons
      j surjmap-id
      (expdata-process-surjmaps-ress (1+ j)
                                     m res-surjmaps surjmap-id))))))

Theorem: expdata-pos-surjmap-alistp-of-expdata-process-surjmaps-ress

(defthm expdata-pos-surjmap-alistp-of-expdata-process-surjmaps-ress
 (implies
  (and (posp j)
       (posp m)
       (expdata-pos-surjmap-alistp res-surjmaps)
       (expdata-surjmapp surjmap-id))
  (b*
   ((new-res-surjmaps
       (expdata-process-surjmaps-ress j m res-surjmaps surjmap-id)))
   (expdata-pos-surjmap-alistp new-res-surjmaps)))
 :rule-classes :rewrite)