• 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-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)