• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
          • Syntax-for-tools
          • Atc
            • Atc-implementation
              • Atc-abstract-syntax
              • Atc-pretty-printer
              • Atc-event-and-code-generation
              • Fty-pseudo-term-utilities
                • Fty-check-mv-let-call
                  • Fty-check-lambda-call
                  • Fty-check-if-call
                  • Fty-remove-equal-formals-actuals
                  • Fty-check-and-call
                  • Fty-check-or-call
                  • Fty-check-fn-call
                  • Fty-check-not-call
                  • Fty-check-list-call
                  • Fty-fsublis-var-lst
                  • Fty-if-to-if*
                  • Fty-fsublis-var
                • Atc-term-recognizers
                • Atc-input-processing
                • Atc-shallow-embedding
                • Atc-process-inputs-and-gen-everything
                • Atc-table
                • Atc-fn
                • Atc-pretty-printing-options
                • Atc-types
                • Atc-macro-definition
              • Atc-tutorial
            • Language
            • Representation
            • Transformation-tools
            • Insertion-sort
            • Pack
          • 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
    • Fty-pseudo-term-utilities

    Fty-check-mv-let-call

    FTY version of check-mv-let-call.

    Signature
    (fty-check-mv-let-call term) 
      → 
    (mv yes/no mv-var vars indices hides mv-term body-term)
    Arguments
    term — Guard (pseudo-termp term).
    Returns
    yes/no — Type (booleanp yes/no).
    mv-var — Type (symbolp mv-var).
    vars — Type (symbol-listp vars).
    indices — Type (nat-listp indices).
    hides — Type (boolean-listp hides).
    mv-term — Type (pseudo-termp mv-term).
    body-term — Type (pseudo-termp body-term).

    Definitions and Theorems

    Function: fty-check-mv-let-call

    (defun fty-check-mv-let-call (term)
      (declare (xargs :guard (pseudo-termp term)))
      (let ((__function__ 'fty-check-mv-let-call))
        (declare (ignorable __function__))
        (check-mv-let-call (pseudo-term-fix term))))

    Theorem: booleanp-of-fty-check-mv-let-call.yes/no

    (defthm booleanp-of-fty-check-mv-let-call.yes/no
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (booleanp yes/no))
      :rule-classes :rewrite)

    Theorem: symbolp-of-fty-check-mv-let-call.mv-var

    (defthm symbolp-of-fty-check-mv-let-call.mv-var
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (symbolp mv-var))
      :rule-classes :rewrite)

    Theorem: symbol-listp-of-fty-check-mv-let-call.vars

    (defthm symbol-listp-of-fty-check-mv-let-call.vars
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (symbol-listp vars))
      :rule-classes :rewrite)

    Theorem: nat-listp-of-fty-check-mv-let-call.indices

    (defthm nat-listp-of-fty-check-mv-let-call.indices
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (nat-listp indices))
      :rule-classes :rewrite)

    Theorem: boolean-listp-of-fty-check-mv-let-call.hides

    (defthm boolean-listp-of-fty-check-mv-let-call.hides
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (boolean-listp hides))
      :rule-classes :rewrite)

    Theorem: pseudo-termp-of-fty-check-mv-let-call.mv-term

    (defthm pseudo-termp-of-fty-check-mv-let-call.mv-term
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (pseudo-termp mv-term))
      :rule-classes :rewrite)

    Theorem: pseudo-termp-of-fty-check-mv-let-call.body-term

    (defthm pseudo-termp-of-fty-check-mv-let-call.body-term
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (pseudo-termp body-term))
      :rule-classes :rewrite)

    Theorem: len-of-fty-check-mv-let-call.indices/vars

    (defthm len-of-fty-check-mv-let-call.indices/vars
      (implies (and (pseudo-termp term))
               (b* (((mv ?yes/no ?mv-var ?vars
                         ?indices ?hides ?mv-term ?body-term)
                     (fty-check-mv-let-call term)))
                 (implies yes/no
                          (equal (len indices) (len vars))))))

    Theorem: len-of-fty-check-mv-let-call.hides/vars

    (defthm len-of-fty-check-mv-let-call.hides/vars
      (implies (and (pseudo-termp term))
               (b* (((mv ?yes/no ?mv-var ?vars
                         ?indices ?hides ?mv-term ?body-term)
                     (fty-check-mv-let-call term)))
                 (implies yes/no
                          (equal (len hides) (len vars))))))

    Theorem: pseudo-term-count-of-check-mv-let-call.mv-term

    (defthm pseudo-term-count-of-check-mv-let-call.mv-term
      (implies (pseudo-termp term)
               (b* (((mv yes/no & & & & mv-term &)
                     (check-mv-let-call term)))
                 (implies yes/no
                          (< (pseudo-term-count mv-term)
                             (pseudo-term-count term)))))
      :rule-classes :linear)

    Theorem: pseudo-term-count-of-fty-check-mv-let-call.mv-term

    (defthm pseudo-term-count-of-fty-check-mv-let-call.mv-term
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (implies yes/no
                 (< (pseudo-term-count mv-term)
                    (pseudo-term-count term))))
      :rule-classes :linear)

    Theorem: pseudo-term-count-of-check-mv-let-call.body-term

    (defthm pseudo-term-count-of-check-mv-let-call.body-term
      (implies (pseudo-termp term)
               (b* (((mv yes/no & & & & & body-term)
                     (check-mv-let-call term)))
                 (implies yes/no
                          (< (pseudo-term-count body-term)
                             (pseudo-term-count term)))))
      :rule-classes :linear)

    Theorem: pseudo-term-count-of-fty-check-mv-let-call.body-term

    (defthm pseudo-term-count-of-fty-check-mv-let-call.body-term
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (implies yes/no
                 (< (pseudo-term-count body-term)
                    (pseudo-term-count term))))
      :rule-classes :linear)

    Theorem: pseudo-term-count-of-check-mv-let-call

    (defthm pseudo-term-count-of-check-mv-let-call
      (implies (pseudo-termp term)
               (b* (((mv yes/no & & & & mv-term body-term)
                     (check-mv-let-call term)))
                 (implies yes/no
                          (< (+ (pseudo-term-count mv-term)
                                (pseudo-term-count body-term))
                             (pseudo-term-count term)))))
      :rule-classes :linear)

    Theorem: pseudo-term-count-if-fty-check-mv-let-call

    (defthm pseudo-term-count-if-fty-check-mv-let-call
      (b* (((mv ?yes/no ?mv-var ?vars
                ?indices ?hides ?mv-term ?body-term)
            (fty-check-mv-let-call term)))
        (implies yes/no
                 (b* (((mv yes/no & & & & mv-term body-term)
                       (fty-check-mv-let-call term)))
                   (implies yes/no
                            (< (+ (pseudo-term-count mv-term)
                                  (pseudo-term-count body-term))
                               (pseudo-term-count term))))))
      :rule-classes :linear)