• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
          • Simplify-defun
          • Isodata
          • Tailrec
          • Schemalg
          • Restrict
          • Expdata
            • Expdata-implementation
              • Expdata-event-generation
              • Expdata-fn
              • Expdata-input-processing
                • Expdata-symbol-surjmap-alistp
                • Expdata-surjmapp
                • Expdata-pos-surjmap-alistp
                • Expdata-process-surj
                • Expdata-process-arg/res-list-surj
                • Expdata-process-inputs
                • Expdata-process-surjmaps
                • Expdata-fresh-defsurj-thm-names
                • Expdata-process-arg/res-list
                • Expdata-process-arg/res-list-surj-list
                • Expdata-process-res
                • Expdata-process-newp-of-new-name
                • Expdata-fresh-defsurj-name-with-*s-suffix
                • Expdata-process-surjmaps-ress
                • Expdata-process-surjmaps-args
                  • Expdata-process-arg/res-list-surj-add-args
                  • Expdata-process-arg/res-list-surj-add-ress
                  • Expdata-process-old
                  • Expdata-process-arg/res-list-aux
                  • Expdata-surjmap-listp
                  • Expdata-fresh-defsurj-name-with-*s-suffix-aux
                • Expdata-macro-definition
            • Casesplit
            • Simplify-term
            • Simplify-defun-sk
            • Parteval
            • Solve
            • Wrap-output
            • Propagate-iso
            • Simplify
            • Finite-difference
            • Drop-irrelevant-params
            • Copy-function
            • Lift-iso
            • Rename-params
            • Utilities
            • Simplify-term-programmatic
            • Simplify-defun-sk-programmatic
            • Simplify-defun-programmatic
            • Simplify-defun+
            • Common-options
            • Common-concepts
          • Error-checking
          • Fty-extensions
          • Isar
          • Kestrel-utilities
          • Set
          • Soft
          • C
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • 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)