• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
      • Fresh-logical-name-with-$s-suffix
      • Irrelevant-formals-info
      • Std/system/function-queries
      • Std/system/term-queries
      • Std/system/term-transformations
        • Make-mv-let-call
        • Mvify
        • Remove-trivial-vars
        • Remove-unused-vars
        • Fsublis-fn-rec
        • Close-lambdas
        • Fsublis-var
        • Remove-mbe-logic/exec
        • Untranslate$
        • Remove-dead-if-branches
        • Remove-progn
        • Make-mv-nth-calls
        • Apply-fn-into-ifs
        • Conjoin-equalities
        • Fapply-unary-to-terms
        • Apply-unary-to-terms
        • Apply-terms-same-args
        • Apply-term
        • Fsublis-fn-lst-simple
        • Fsublis-fn
        • Fapply-terms-same-args
        • Fsublis-fn-simple
        • Fapply-term
        • Remove-mbe-logic
        • Remove-mbe-exec
        • Quote-term
        • Quote-term-list
        • Apply-term*
        • Std/system/fsubcor-var
        • Std/system/conjoin
        • Std/system/flatten-ands-in-lit
        • Fapply-term*
        • Std/system/dumb-negate-lit
      • Std/system/enhanced-utilities
      • Install-not-normalized-event
      • Install-not-normalized-event-lst
      • Std/system/term-function-recognizers
      • Genvar$
      • Std/system/event-name-queries
      • Pseudo-tests-and-call-listp
      • Maybe-pseudo-event-formp
      • Add-suffix-to-fn-or-const
      • Chk-irrelevant-formals-ok
      • Table-alist+
      • Pseudo-tests-and-callp
      • Add-suffix-to-fn-or-const-lst
      • Known-packages+
      • Add-suffix-to-fn-lst
      • Unquote-term
      • Event-landmark-names
      • Add-suffix-lst
      • Std/system/theorem-queries
      • Unquote-term-list
      • Std/system/macro-queries
      • Pseudo-command-landmark-listp
      • Install-not-normalized$
      • Pseudo-event-landmark-listp
      • Known-packages
      • Std/system/partition-rest-and-keyword-args
      • Rune-enabledp
      • Rune-disabledp
      • Included-books
      • Std/system/pseudo-event-formp
      • Std/system/plist-worldp-with-formals
      • Std/system/w
      • Std/system/geprops
      • Std/system/arglistp
      • Std/system/constant-queries
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/system/term-transformations

Make-mv-nth-calls

Given a term term, return the list of n terms ((mv-th '0 term) ... (mv-nth 'n-1 term)).

Signature

(make-mv-nth-calls term n) → terms

Arguments

term — Guard (pseudo-termp term).

n — Guard (natp n).

Returns

terms — Type (pseudo-term-listp terms), given (pseudo-termp term).

Definitions and Theorems

Function: make-mv-nth-calls-aux

(defun make-mv-nth-calls-aux (term i n)
  (declare (xargs :guard (and (pseudo-termp term)
                              (natp i)
                              (natp n))))
  (let ((__function__ 'make-mv-nth-calls-aux))
    (declare (ignorable __function__))
    (if (or (not (mbt (natp i)))
            (not (mbt (natp n)))
            (>= i n))
        nil
      (cons (cons 'mv-nth
                  (cons (cons 'quote (cons i 'nil))
                        (cons term 'nil)))
            (make-mv-nth-calls-aux term (1+ i)
                                   n)))))

Theorem: pseudo-term-listp-of-make-mv-nth-calls-aux

(defthm pseudo-term-listp-of-make-mv-nth-calls-aux
  (implies (pseudo-termp term)
           (b* ((terms (make-mv-nth-calls-aux term i n)))
             (pseudo-term-listp terms)))
  :rule-classes :rewrite)

Theorem: len-of-make-mv-nth-calls-aux

(defthm len-of-make-mv-nth-calls-aux
  (b* ((?terms (make-mv-nth-calls-aux term i n)))
    (equal (len terms)
           (if (natp i) (nfix (- (nfix n) i)) 0))))

Function: make-mv-nth-calls

(defun make-mv-nth-calls (term n)
  (declare (xargs :guard (and (pseudo-termp term) (natp n))))
  (let ((__function__ 'make-mv-nth-calls))
    (declare (ignorable __function__))
    (make-mv-nth-calls-aux term 0 n)))

Theorem: pseudo-term-listp-of-make-mv-nth-calls

(defthm pseudo-term-listp-of-make-mv-nth-calls
  (implies (pseudo-termp term)
           (b* ((terms (make-mv-nth-calls term n)))
             (pseudo-term-listp terms)))
  :rule-classes :rewrite)

Theorem: len-of-make-mv-nth-calls

(defthm len-of-make-mv-nth-calls
  (b* ((?terms (make-mv-nth-calls term n)))
    (equal (len terms) (nfix n))))