• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
          • Uninterpreted-fn-cp
          • Smt-hint-interface
          • Function-expansion
            • Ex-args
            • Expand
            • Expand-measure
            • Ex-outs
          • Smt-config
          • Fty-support
          • Smt-computed-hints
          • Add-hypo-cp
          • Smt-hint-please
          • Type-extract-cp
          • Smt-extract
          • Smtlink-process-user-hint
          • Smt-basics
          • Smt-type-hyp
          • Smt-magic-fix
        • Trusted
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Verified

Function-expansion

Function expansion

Definitions and Theorems

Function: sym-nat-alistp

(defun sym-nat-alistp (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'sym-nat-alistp))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        (eq x nil)
      (and (consp (car x))
           (symbolp (caar x))
           (natp (cdar x))
           (sym-nat-alistp (cdr x))))))

Theorem: sym-nat-alistp-of-revappend

(defthm sym-nat-alistp-of-revappend
  (equal (sym-nat-alistp (revappend acl2::x acl2::y))
         (and (sym-nat-alistp (acl2::list-fix acl2::x))
              (sym-nat-alistp acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-remove

(defthm sym-nat-alistp-of-remove
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (remove acl2::a acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-last

(defthm sym-nat-alistp-of-last
  (implies (sym-nat-alistp (double-rewrite acl2::x))
           (sym-nat-alistp (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-nthcdr

(defthm sym-nat-alistp-of-nthcdr
  (implies (sym-nat-alistp (double-rewrite acl2::x))
           (sym-nat-alistp (nthcdr acl2::n acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-butlast

(defthm sym-nat-alistp-of-butlast
  (implies (sym-nat-alistp (double-rewrite acl2::x))
           (sym-nat-alistp (butlast acl2::x acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-update-nth

(defthm sym-nat-alistp-of-update-nth
 (implies (sym-nat-alistp (double-rewrite acl2::x))
          (iff (sym-nat-alistp (update-nth acl2::n acl2::y acl2::x))
               (and (and (consp acl2::y)
                         (symbolp (car acl2::y))
                         (natp (cdr acl2::y)))
                    (or (<= (nfix acl2::n) (len acl2::x))
                        (and (consp nil)
                             (symbolp (car nil))
                             (natp (cdr nil)))))))
 :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-repeat

(defthm sym-nat-alistp-of-repeat
  (iff (sym-nat-alistp (acl2::repeat acl2::n acl2::x))
       (or (and (consp acl2::x)
                (symbolp (car acl2::x))
                (natp (cdr acl2::x)))
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-take

(defthm sym-nat-alistp-of-take
  (implies (sym-nat-alistp (double-rewrite acl2::x))
           (iff (sym-nat-alistp (take acl2::n acl2::x))
                (or (and (consp nil)
                         (symbolp (car nil))
                         (natp (cdr nil)))
                    (<= (nfix acl2::n) (len acl2::x)))))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-union-equal

(defthm sym-nat-alistp-of-union-equal
  (equal (sym-nat-alistp (union-equal acl2::x acl2::y))
         (and (sym-nat-alistp (acl2::list-fix acl2::x))
              (sym-nat-alistp (double-rewrite acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-intersection-equal-2

(defthm sym-nat-alistp-of-intersection-equal-2
  (implies (sym-nat-alistp (double-rewrite acl2::y))
           (sym-nat-alistp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-intersection-equal-1

(defthm sym-nat-alistp-of-intersection-equal-1
  (implies (sym-nat-alistp (double-rewrite acl2::x))
           (sym-nat-alistp (intersection-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-set-difference-equal

(defthm sym-nat-alistp-of-set-difference-equal
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (set-difference-equal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-when-subsetp-equal

(defthm sym-nat-alistp-when-subsetp-equal
  (and (implies (and (subsetp-equal acl2::x acl2::y)
                     (sym-nat-alistp acl2::y))
                (equal (sym-nat-alistp acl2::x)
                       (true-listp acl2::x)))
       (implies (and (sym-nat-alistp acl2::y)
                     (subsetp-equal acl2::x acl2::y))
                (equal (sym-nat-alistp acl2::x)
                       (true-listp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-rcons

(defthm sym-nat-alistp-of-rcons
  (iff (sym-nat-alistp (acl2::rcons acl2::a acl2::x))
       (and (and (consp acl2::a)
                 (symbolp (car acl2::a))
                 (natp (cdr acl2::a)))
            (sym-nat-alistp (acl2::list-fix acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-append

(defthm sym-nat-alistp-of-append
  (equal (sym-nat-alistp (append acl2::a acl2::b))
         (and (sym-nat-alistp (acl2::list-fix acl2::a))
              (sym-nat-alistp acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-rev

(defthm sym-nat-alistp-of-rev
  (equal (sym-nat-alistp (acl2::rev acl2::x))
         (sym-nat-alistp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-duplicated-members

(defthm sym-nat-alistp-of-duplicated-members
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (acl2::duplicated-members acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-difference

(defthm sym-nat-alistp-of-difference
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (set::difference acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-intersect-2

(defthm sym-nat-alistp-of-intersect-2
  (implies (sym-nat-alistp acl2::y)
           (sym-nat-alistp (set::intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-intersect-1

(defthm sym-nat-alistp-of-intersect-1
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (set::intersect acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-union

(defthm sym-nat-alistp-of-union
  (iff (sym-nat-alistp (set::union acl2::x acl2::y))
       (and (sym-nat-alistp (set::sfix acl2::x))
            (sym-nat-alistp (set::sfix acl2::y))))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-mergesort

(defthm sym-nat-alistp-of-mergesort
  (iff (sym-nat-alistp (set::mergesort acl2::x))
       (sym-nat-alistp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-delete

(defthm sym-nat-alistp-of-delete
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (set::delete acl2::k acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-insert

(defthm sym-nat-alistp-of-insert
  (iff (sym-nat-alistp (set::insert acl2::a acl2::x))
       (and (sym-nat-alistp (set::sfix acl2::x))
            (and (consp acl2::a)
                 (symbolp (car acl2::a))
                 (natp (cdr acl2::a)))))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-sfix

(defthm sym-nat-alistp-of-sfix
  (iff (sym-nat-alistp (set::sfix acl2::x))
       (or (sym-nat-alistp acl2::x)
           (not (set::setp acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-list-fix

(defthm sym-nat-alistp-of-list-fix
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-sym-nat-alistp-compound-recognizer

(defthm true-listp-when-sym-nat-alistp-compound-recognizer
  (implies (sym-nat-alistp acl2::x)
           (true-listp acl2::x))
  :rule-classes :compound-recognizer)

Theorem: sym-nat-alistp-when-not-consp

(defthm sym-nat-alistp-when-not-consp
  (implies (not (consp acl2::x))
           (equal (sym-nat-alistp acl2::x)
                  (not acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-cdr-when-sym-nat-alistp

(defthm sym-nat-alistp-of-cdr-when-sym-nat-alistp
  (implies (sym-nat-alistp (double-rewrite acl2::x))
           (sym-nat-alistp (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-cons

(defthm sym-nat-alistp-of-cons
  (equal (sym-nat-alistp (cons acl2::a acl2::x))
         (and (and (consp acl2::a)
                   (symbolp (car acl2::a))
                   (natp (cdr acl2::a)))
              (sym-nat-alistp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-make-fal

(defthm sym-nat-alistp-of-make-fal
  (implies (and (sym-nat-alistp acl2::x)
                (sym-nat-alistp acl2::y))
           (sym-nat-alistp (acl2::make-fal acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: natp-of-cdr-when-member-equal-of-sym-nat-alistp

(defthm natp-of-cdr-when-member-equal-of-sym-nat-alistp
  (and (implies (and (sym-nat-alistp acl2::x)
                     (member-equal acl2::a acl2::x))
                (natp (cdr acl2::a)))
       (implies (and (member-equal acl2::a acl2::x)
                     (sym-nat-alistp acl2::x))
                (natp (cdr acl2::a))))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-car-when-member-equal-of-sym-nat-alistp

(defthm symbolp-of-car-when-member-equal-of-sym-nat-alistp
  (and (implies (and (sym-nat-alistp acl2::x)
                     (member-equal acl2::a acl2::x))
                (symbolp (car acl2::a)))
       (implies (and (member-equal acl2::a acl2::x)
                     (sym-nat-alistp acl2::x))
                (symbolp (car acl2::a))))
  :rule-classes ((:rewrite)))

Theorem: consp-when-member-equal-of-sym-nat-alistp

(defthm consp-when-member-equal-of-sym-nat-alistp
  (implies (and (sym-nat-alistp acl2::x)
                (member-equal acl2::a acl2::x))
           (consp acl2::a))
  :rule-classes
  ((:rewrite :backchain-limit-lst (0 0))
   (:rewrite :backchain-limit-lst (0 0)
             :corollary (implies (if (member-equal acl2::a acl2::x)
                                     (sym-nat-alistp acl2::x)
                                   'nil)
                                 (consp acl2::a)))))

Theorem: sym-nat-alistp-of-remove-assoc

(defthm sym-nat-alistp-of-remove-assoc
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (remove-assoc-equal acl2::name acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-put-assoc

(defthm sym-nat-alistp-of-put-assoc
 (implies
  (and (sym-nat-alistp acl2::x))
  (iff
     (sym-nat-alistp (put-assoc-equal acl2::name acl2::val acl2::x))
     (and (symbolp acl2::name)
          (natp acl2::val))))
 :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-fast-alist-clean

(defthm sym-nat-alistp-of-fast-alist-clean
  (implies (sym-nat-alistp acl2::x)
           (sym-nat-alistp (fast-alist-clean acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-hons-shrink-alist

(defthm sym-nat-alistp-of-hons-shrink-alist
  (implies (and (sym-nat-alistp acl2::x)
                (sym-nat-alistp acl2::y))
           (sym-nat-alistp (hons-shrink-alist acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: sym-nat-alistp-of-hons-acons

(defthm sym-nat-alistp-of-hons-acons
  (equal (sym-nat-alistp (hons-acons acl2::a acl2::n acl2::x))
         (and (symbolp acl2::a)
              (natp acl2::n)
              (sym-nat-alistp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: natp-of-cdr-of-hons-assoc-equal-when-sym-nat-alistp

(defthm natp-of-cdr-of-hons-assoc-equal-when-sym-nat-alistp
  (implies (sym-nat-alistp acl2::x)
           (iff (natp (cdr (hons-assoc-equal acl2::k acl2::x)))
                (or (hons-assoc-equal acl2::k acl2::x)
                    (natp nil))))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-sym-nat-alistp-rewrite

(defthm alistp-when-sym-nat-alistp-rewrite
  (implies (sym-nat-alistp acl2::x)
           (alistp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-sym-nat-alistp

(defthm alistp-when-sym-nat-alistp
  (implies (sym-nat-alistp acl2::x)
           (alistp acl2::x))
  :rule-classes :tau-system)

Theorem: natp-of-cdar-when-sym-nat-alistp

(defthm natp-of-cdar-when-sym-nat-alistp
  (implies (sym-nat-alistp acl2::x)
           (iff (natp (cdar acl2::x))
                (or (consp acl2::x) (natp nil))))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-caar-when-sym-nat-alistp

(defthm symbolp-of-caar-when-sym-nat-alistp
  (implies (sym-nat-alistp acl2::x)
           (iff (symbolp (caar acl2::x))
                (or (consp acl2::x) (symbolp nil))))
  :rule-classes ((:rewrite)))

Function: sym-nat-alist-fix$inline

(defun sym-nat-alist-fix$inline (x)
  (declare (xargs :guard (sym-nat-alistp x)))
  (let ((acl2::__function__ 'sym-nat-alist-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (atom x)
             nil
           (if (consp (car x))
               (cons (cons (symbol-fix (caar x))
                           (nfix (cdar x)))
                     (sym-nat-alist-fix (cdr x)))
             (sym-nat-alist-fix (cdr x))))
         :exec x)))

Theorem: sym-nat-alistp-of-sym-nat-alist-fix

(defthm sym-nat-alistp-of-sym-nat-alist-fix
  (b* ((fty::newx (sym-nat-alist-fix$inline x)))
    (sym-nat-alistp fty::newx))
  :rule-classes :rewrite)

Theorem: sym-nat-alist-fix-when-sym-nat-alistp

(defthm sym-nat-alist-fix-when-sym-nat-alistp
  (implies (sym-nat-alistp x)
           (equal (sym-nat-alist-fix x) x)))

Function: sym-nat-alist-equiv$inline

(defun sym-nat-alist-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (sym-nat-alistp acl2::x)
                              (sym-nat-alistp acl2::y))))
  (equal (sym-nat-alist-fix acl2::x)
         (sym-nat-alist-fix acl2::y)))

Theorem: sym-nat-alist-equiv-is-an-equivalence

(defthm sym-nat-alist-equiv-is-an-equivalence
  (and (booleanp (sym-nat-alist-equiv x y))
       (sym-nat-alist-equiv x x)
       (implies (sym-nat-alist-equiv x y)
                (sym-nat-alist-equiv y x))
       (implies (and (sym-nat-alist-equiv x y)
                     (sym-nat-alist-equiv y z))
                (sym-nat-alist-equiv x z)))
  :rule-classes (:equivalence))

Theorem: sym-nat-alist-equiv-implies-equal-sym-nat-alist-fix-1

(defthm sym-nat-alist-equiv-implies-equal-sym-nat-alist-fix-1
  (implies (sym-nat-alist-equiv acl2::x x-equiv)
           (equal (sym-nat-alist-fix acl2::x)
                  (sym-nat-alist-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: sym-nat-alist-fix-under-sym-nat-alist-equiv

(defthm sym-nat-alist-fix-under-sym-nat-alist-equiv
  (sym-nat-alist-equiv (sym-nat-alist-fix acl2::x)
                       acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-sym-nat-alist-fix-1-forward-to-sym-nat-alist-equiv

(defthm equal-of-sym-nat-alist-fix-1-forward-to-sym-nat-alist-equiv
  (implies (equal (sym-nat-alist-fix acl2::x)
                  acl2::y)
           (sym-nat-alist-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-sym-nat-alist-fix-2-forward-to-sym-nat-alist-equiv

(defthm equal-of-sym-nat-alist-fix-2-forward-to-sym-nat-alist-equiv
  (implies (equal acl2::x (sym-nat-alist-fix acl2::y))
           (sym-nat-alist-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: sym-nat-alist-equiv-of-sym-nat-alist-fix-1-forward

(defthm sym-nat-alist-equiv-of-sym-nat-alist-fix-1-forward
  (implies (sym-nat-alist-equiv (sym-nat-alist-fix acl2::x)
                                acl2::y)
           (sym-nat-alist-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: sym-nat-alist-equiv-of-sym-nat-alist-fix-2-forward

(defthm sym-nat-alist-equiv-of-sym-nat-alist-fix-2-forward
  (implies (sym-nat-alist-equiv acl2::x (sym-nat-alist-fix acl2::y))
           (sym-nat-alist-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: cons-of-symbol-fix-k-under-sym-nat-alist-equiv

(defthm cons-of-symbol-fix-k-under-sym-nat-alist-equiv
  (sym-nat-alist-equiv (cons (cons (symbol-fix acl2::k) acl2::v)
                             acl2::x)
                       (cons (cons acl2::k acl2::v) acl2::x)))

Theorem: cons-symbol-equiv-congruence-on-k-under-sym-nat-alist-equiv

(defthm cons-symbol-equiv-congruence-on-k-under-sym-nat-alist-equiv
  (implies
       (acl2::symbol-equiv acl2::k k-equiv)
       (sym-nat-alist-equiv (cons (cons acl2::k acl2::v) acl2::x)
                            (cons (cons k-equiv acl2::v) acl2::x)))
  :rule-classes :congruence)

Theorem: cons-of-nfix-v-under-sym-nat-alist-equiv

(defthm cons-of-nfix-v-under-sym-nat-alist-equiv
  (sym-nat-alist-equiv (cons (cons acl2::k (nfix acl2::v))
                             acl2::x)
                       (cons (cons acl2::k acl2::v) acl2::x)))

Theorem: cons-nat-equiv-congruence-on-v-under-sym-nat-alist-equiv

(defthm cons-nat-equiv-congruence-on-v-under-sym-nat-alist-equiv
  (implies
       (acl2::nat-equiv acl2::v v-equiv)
       (sym-nat-alist-equiv (cons (cons acl2::k acl2::v) acl2::x)
                            (cons (cons acl2::k v-equiv) acl2::x)))
  :rule-classes :congruence)

Theorem: cons-of-sym-nat-alist-fix-y-under-sym-nat-alist-equiv

(defthm cons-of-sym-nat-alist-fix-y-under-sym-nat-alist-equiv
  (sym-nat-alist-equiv (cons acl2::x (sym-nat-alist-fix acl2::y))
                       (cons acl2::x acl2::y)))

Theorem: cons-sym-nat-alist-equiv-congruence-on-y-under-sym-nat-alist-equiv

(defthm
 cons-sym-nat-alist-equiv-congruence-on-y-under-sym-nat-alist-equiv
 (implies (sym-nat-alist-equiv acl2::y y-equiv)
          (sym-nat-alist-equiv (cons acl2::x acl2::y)
                               (cons acl2::x y-equiv)))
 :rule-classes :congruence)

Theorem: sym-nat-alist-fix-of-acons

(defthm sym-nat-alist-fix-of-acons
  (equal (sym-nat-alist-fix (cons (cons acl2::a acl2::b) x))
         (cons (cons (symbol-fix acl2::a)
                     (nfix acl2::b))
               (sym-nat-alist-fix x))))

Theorem: sym-nat-alist-fix-of-append

(defthm sym-nat-alist-fix-of-append
  (equal (sym-nat-alist-fix (append std::a std::b))
         (append (sym-nat-alist-fix std::a)
                 (sym-nat-alist-fix std::b))))

Theorem: consp-car-of-sym-nat-alist-fix

(defthm consp-car-of-sym-nat-alist-fix
  (equal (consp (car (sym-nat-alist-fix x)))
         (consp (sym-nat-alist-fix x))))

Function: update-fn-lvls

(defun update-fn-lvls (fn fn-lvls)
  (declare (xargs :guard (and (symbolp fn)
                              (sym-nat-alistp fn-lvls))))
  (let ((acl2::__function__ 'update-fn-lvls))
    (declare (ignorable acl2::__function__))
    (b* ((fn (symbol-fix fn))
         (fn-lvls (sym-nat-alist-fix fn-lvls))
         ((unless (consp fn-lvls)) nil)
         ((cons first rest) fn-lvls)
         ((cons this-fn this-lvl) first)
         ((unless (equal fn this-fn))
          (cons (cons this-fn this-lvl)
                (update-fn-lvls fn rest))))
      (if (zp this-lvl)
          (cons (cons this-fn 0) rest)
        (cons (cons this-fn (1- this-lvl))
              rest)))))

Theorem: sym-nat-alistp-of-update-fn-lvls

(defthm sym-nat-alistp-of-update-fn-lvls
  (b* ((updated-fn-lvls (update-fn-lvls fn fn-lvls)))
    (sym-nat-alistp updated-fn-lvls))
  :rule-classes :rewrite)

Theorem: updated-fn-lvls-decrease

(defthm updated-fn-lvls-decrease
  (b* ((updated-fn-lvls (update-fn-lvls fn fn-lvls)))
    (implies (and (symbolp fn)
                  (sym-nat-alistp fn-lvls)
                  (consp fn-lvls)
                  (assoc-equal fn fn-lvls)
                  (not (equal (cdr (assoc-equal fn fn-lvls))
                              0)))
             (< (cdr (assoc fn updated-fn-lvls))
                (cdr (assoc fn fn-lvls)))))
  :rule-classes :rewrite)

Function: ex-args-p

(defun ex-args-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'ex-args-p))
  (declare (ignorable acl2::__function__))
  (and
   (mbe
     :logic
     (and (alistp x)
          (equal (strip-cars x)
                 '(term-lst fn-lst fn-lvls wrld-fn-len expand-lst)))
     :exec (fty::alist-with-carsp
                x
                '(term-lst fn-lst fn-lvls wrld-fn-len expand-lst)))
   (b* ((term-lst (cdr (std::da-nth 0 x)))
        (fn-lst (cdr (std::da-nth 1 x)))
        (fn-lvls (cdr (std::da-nth 2 x)))
        (wrld-fn-len (cdr (std::da-nth 3 x)))
        (expand-lst (cdr (std::da-nth 4 x))))
     (and (pseudo-term-listp term-lst)
          (func-alistp fn-lst)
          (sym-nat-alistp fn-lvls)
          (natp wrld-fn-len)
          (pseudo-term-alistp expand-lst))))))

Theorem: consp-when-ex-args-p

(defthm consp-when-ex-args-p
  (implies (ex-args-p x) (consp x))
  :rule-classes :compound-recognizer)

Function: ex-args-fix$inline

(defun ex-args-fix$inline (x)
 (declare (xargs :guard (ex-args-p x)))
 (let ((acl2::__function__ 'ex-args-fix))
  (declare (ignorable acl2::__function__))
  (mbe
    :logic
    (b*
      ((term-lst (pseudo-term-list-fix (cdr (std::da-nth 0 x))))
       (fn-lst (func-alist-fix (cdr (std::da-nth 1 x))))
       (fn-lvls (sym-nat-alist-fix (cdr (std::da-nth 2 x))))
       (wrld-fn-len (nfix (cdr (std::da-nth 3 x))))
       (expand-lst (pseudo-term-alist-fix (cdr (std::da-nth 4 x)))))
      (list (cons 'term-lst term-lst)
            (cons 'fn-lst fn-lst)
            (cons 'fn-lvls fn-lvls)
            (cons 'wrld-fn-len wrld-fn-len)
            (cons 'expand-lst expand-lst)))
    :exec x)))

Theorem: ex-args-p-of-ex-args-fix

(defthm ex-args-p-of-ex-args-fix
  (b* ((new-x (ex-args-fix$inline x)))
    (ex-args-p new-x))
  :rule-classes :rewrite)

Theorem: ex-args-fix-when-ex-args-p

(defthm ex-args-fix-when-ex-args-p
  (implies (ex-args-p x)
           (equal (ex-args-fix x) x)))

Function: ex-args-equiv$inline

(defun ex-args-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (ex-args-p acl2::x)
                              (ex-args-p acl2::y))))
  (equal (ex-args-fix acl2::x)
         (ex-args-fix acl2::y)))

Theorem: ex-args-equiv-is-an-equivalence

(defthm ex-args-equiv-is-an-equivalence
  (and (booleanp (ex-args-equiv x y))
       (ex-args-equiv x x)
       (implies (ex-args-equiv x y)
                (ex-args-equiv y x))
       (implies (and (ex-args-equiv x y)
                     (ex-args-equiv y z))
                (ex-args-equiv x z)))
  :rule-classes (:equivalence))

Theorem: ex-args-equiv-implies-equal-ex-args-fix-1

(defthm ex-args-equiv-implies-equal-ex-args-fix-1
  (implies (ex-args-equiv acl2::x x-equiv)
           (equal (ex-args-fix acl2::x)
                  (ex-args-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: ex-args-fix-under-ex-args-equiv

(defthm ex-args-fix-under-ex-args-equiv
  (ex-args-equiv (ex-args-fix acl2::x)
                 acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-ex-args-fix-1-forward-to-ex-args-equiv

(defthm equal-of-ex-args-fix-1-forward-to-ex-args-equiv
  (implies (equal (ex-args-fix acl2::x) acl2::y)
           (ex-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-ex-args-fix-2-forward-to-ex-args-equiv

(defthm equal-of-ex-args-fix-2-forward-to-ex-args-equiv
  (implies (equal acl2::x (ex-args-fix acl2::y))
           (ex-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: ex-args-equiv-of-ex-args-fix-1-forward

(defthm ex-args-equiv-of-ex-args-fix-1-forward
  (implies (ex-args-equiv (ex-args-fix acl2::x)
                          acl2::y)
           (ex-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: ex-args-equiv-of-ex-args-fix-2-forward

(defthm ex-args-equiv-of-ex-args-fix-2-forward
  (implies (ex-args-equiv acl2::x (ex-args-fix acl2::y))
           (ex-args-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Function: ex-args->term-lst$inline

(defun ex-args->term-lst$inline (x)
  (declare (xargs :guard (ex-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-args->term-lst))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (pseudo-term-list-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: pseudo-term-listp-of-ex-args->term-lst

(defthm pseudo-term-listp-of-ex-args->term-lst
  (b* ((term-lst (ex-args->term-lst$inline x)))
    (pseudo-term-listp term-lst))
  :rule-classes :rewrite)

Theorem: ex-args->term-lst$inline-of-ex-args-fix-x

(defthm ex-args->term-lst$inline-of-ex-args-fix-x
  (equal (ex-args->term-lst$inline (ex-args-fix x))
         (ex-args->term-lst$inline x)))

Theorem: ex-args->term-lst$inline-ex-args-equiv-congruence-on-x

(defthm ex-args->term-lst$inline-ex-args-equiv-congruence-on-x
  (implies (ex-args-equiv x x-equiv)
           (equal (ex-args->term-lst$inline x)
                  (ex-args->term-lst$inline x-equiv)))
  :rule-classes :congruence)

Function: ex-args->fn-lst$inline

(defun ex-args->fn-lst$inline (x)
  (declare (xargs :guard (ex-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-args->fn-lst))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (func-alist-fix (cdr (std::da-nth 1 x))))
         :exec (cdr (std::da-nth 1 x)))))

Theorem: func-alistp-of-ex-args->fn-lst

(defthm func-alistp-of-ex-args->fn-lst
  (b* ((fn-lst (ex-args->fn-lst$inline x)))
    (func-alistp fn-lst))
  :rule-classes :rewrite)

Theorem: ex-args->fn-lst$inline-of-ex-args-fix-x

(defthm ex-args->fn-lst$inline-of-ex-args-fix-x
  (equal (ex-args->fn-lst$inline (ex-args-fix x))
         (ex-args->fn-lst$inline x)))

Theorem: ex-args->fn-lst$inline-ex-args-equiv-congruence-on-x

(defthm ex-args->fn-lst$inline-ex-args-equiv-congruence-on-x
  (implies (ex-args-equiv x x-equiv)
           (equal (ex-args->fn-lst$inline x)
                  (ex-args->fn-lst$inline x-equiv)))
  :rule-classes :congruence)

Function: ex-args->fn-lvls$inline

(defun ex-args->fn-lvls$inline (x)
  (declare (xargs :guard (ex-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-args->fn-lvls))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (sym-nat-alist-fix (cdr (std::da-nth 2 x))))
         :exec (cdr (std::da-nth 2 x)))))

Theorem: sym-nat-alistp-of-ex-args->fn-lvls

(defthm sym-nat-alistp-of-ex-args->fn-lvls
  (b* ((fn-lvls (ex-args->fn-lvls$inline x)))
    (sym-nat-alistp fn-lvls))
  :rule-classes :rewrite)

Theorem: ex-args->fn-lvls$inline-of-ex-args-fix-x

(defthm ex-args->fn-lvls$inline-of-ex-args-fix-x
  (equal (ex-args->fn-lvls$inline (ex-args-fix x))
         (ex-args->fn-lvls$inline x)))

Theorem: ex-args->fn-lvls$inline-ex-args-equiv-congruence-on-x

(defthm ex-args->fn-lvls$inline-ex-args-equiv-congruence-on-x
  (implies (ex-args-equiv x x-equiv)
           (equal (ex-args->fn-lvls$inline x)
                  (ex-args->fn-lvls$inline x-equiv)))
  :rule-classes :congruence)

Function: ex-args->wrld-fn-len$inline

(defun ex-args->wrld-fn-len$inline (x)
  (declare (xargs :guard (ex-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-args->wrld-fn-len))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (nfix (cdr (std::da-nth 3 x))))
         :exec (cdr (std::da-nth 3 x)))))

Theorem: natp-of-ex-args->wrld-fn-len

(defthm natp-of-ex-args->wrld-fn-len
  (b* ((wrld-fn-len (ex-args->wrld-fn-len$inline x)))
    (natp wrld-fn-len))
  :rule-classes :rewrite)

Theorem: ex-args->wrld-fn-len$inline-of-ex-args-fix-x

(defthm ex-args->wrld-fn-len$inline-of-ex-args-fix-x
  (equal (ex-args->wrld-fn-len$inline (ex-args-fix x))
         (ex-args->wrld-fn-len$inline x)))

Theorem: ex-args->wrld-fn-len$inline-ex-args-equiv-congruence-on-x

(defthm ex-args->wrld-fn-len$inline-ex-args-equiv-congruence-on-x
  (implies (ex-args-equiv x x-equiv)
           (equal (ex-args->wrld-fn-len$inline x)
                  (ex-args->wrld-fn-len$inline x-equiv)))
  :rule-classes :congruence)

Function: ex-args->expand-lst$inline

(defun ex-args->expand-lst$inline (x)
  (declare (xargs :guard (ex-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-args->expand-lst))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (pseudo-term-alist-fix (cdr (std::da-nth 4 x))))
         :exec (cdr (std::da-nth 4 x)))))

Theorem: pseudo-term-alistp-of-ex-args->expand-lst

(defthm pseudo-term-alistp-of-ex-args->expand-lst
  (b* ((expand-lst (ex-args->expand-lst$inline x)))
    (pseudo-term-alistp expand-lst))
  :rule-classes :rewrite)

Theorem: ex-args->expand-lst$inline-of-ex-args-fix-x

(defthm ex-args->expand-lst$inline-of-ex-args-fix-x
  (equal (ex-args->expand-lst$inline (ex-args-fix x))
         (ex-args->expand-lst$inline x)))

Theorem: ex-args->expand-lst$inline-ex-args-equiv-congruence-on-x

(defthm ex-args->expand-lst$inline-ex-args-equiv-congruence-on-x
  (implies (ex-args-equiv x x-equiv)
           (equal (ex-args->expand-lst$inline x)
                  (ex-args->expand-lst$inline x-equiv)))
  :rule-classes :congruence)

Function: ex-args

(defun ex-args (term-lst fn-lst fn-lvls wrld-fn-len expand-lst)
  (declare (xargs :guard (and (pseudo-term-listp term-lst)
                              (func-alistp fn-lst)
                              (sym-nat-alistp fn-lvls)
                              (natp wrld-fn-len)
                              (pseudo-term-alistp expand-lst))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-args))
    (declare (ignorable acl2::__function__))
    (b* ((term-lst (mbe :logic (pseudo-term-list-fix term-lst)
                        :exec term-lst))
         (fn-lst (mbe :logic (func-alist-fix fn-lst)
                      :exec fn-lst))
         (fn-lvls (mbe :logic (sym-nat-alist-fix fn-lvls)
                       :exec fn-lvls))
         (wrld-fn-len (mbe :logic (nfix wrld-fn-len)
                           :exec wrld-fn-len))
         (expand-lst (mbe :logic (pseudo-term-alist-fix expand-lst)
                          :exec expand-lst)))
      (list (cons 'term-lst term-lst)
            (cons 'fn-lst fn-lst)
            (cons 'fn-lvls fn-lvls)
            (cons 'wrld-fn-len wrld-fn-len)
            (cons 'expand-lst expand-lst)))))

Theorem: ex-args-p-of-ex-args

(defthm ex-args-p-of-ex-args
  (b* ((x (ex-args term-lst
                   fn-lst fn-lvls wrld-fn-len expand-lst)))
    (ex-args-p x))
  :rule-classes :rewrite)

Theorem: ex-args->term-lst-of-ex-args

(defthm ex-args->term-lst-of-ex-args
  (equal (ex-args->term-lst
              (ex-args term-lst
                       fn-lst fn-lvls wrld-fn-len expand-lst))
         (pseudo-term-list-fix term-lst)))

Theorem: ex-args->fn-lst-of-ex-args

(defthm ex-args->fn-lst-of-ex-args
 (equal
   (ex-args->fn-lst (ex-args term-lst
                             fn-lst fn-lvls wrld-fn-len expand-lst))
   (func-alist-fix fn-lst)))

Theorem: ex-args->fn-lvls-of-ex-args

(defthm ex-args->fn-lvls-of-ex-args
 (equal
  (ex-args->fn-lvls (ex-args term-lst
                             fn-lst fn-lvls wrld-fn-len expand-lst))
  (sym-nat-alist-fix fn-lvls)))

Theorem: ex-args->wrld-fn-len-of-ex-args

(defthm ex-args->wrld-fn-len-of-ex-args
  (equal (ex-args->wrld-fn-len
              (ex-args term-lst
                       fn-lst fn-lvls wrld-fn-len expand-lst))
         (nfix wrld-fn-len)))

Theorem: ex-args->expand-lst-of-ex-args

(defthm ex-args->expand-lst-of-ex-args
  (equal (ex-args->expand-lst
              (ex-args term-lst
                       fn-lst fn-lvls wrld-fn-len expand-lst))
         (pseudo-term-alist-fix expand-lst)))

Theorem: ex-args-of-fields

(defthm ex-args-of-fields
  (equal (ex-args (ex-args->term-lst x)
                  (ex-args->fn-lst x)
                  (ex-args->fn-lvls x)
                  (ex-args->wrld-fn-len x)
                  (ex-args->expand-lst x))
         (ex-args-fix x)))

Theorem: ex-args-fix-when-ex-args

(defthm ex-args-fix-when-ex-args
  (equal (ex-args-fix x)
         (ex-args (ex-args->term-lst x)
                  (ex-args->fn-lst x)
                  (ex-args->fn-lvls x)
                  (ex-args->wrld-fn-len x)
                  (ex-args->expand-lst x))))

Theorem: equal-of-ex-args

(defthm equal-of-ex-args
  (equal (equal (ex-args term-lst
                         fn-lst fn-lvls wrld-fn-len expand-lst)
                x)
         (and (ex-args-p x)
              (equal (ex-args->term-lst x)
                     (pseudo-term-list-fix term-lst))
              (equal (ex-args->fn-lst x)
                     (func-alist-fix fn-lst))
              (equal (ex-args->fn-lvls x)
                     (sym-nat-alist-fix fn-lvls))
              (equal (ex-args->wrld-fn-len x)
                     (nfix wrld-fn-len))
              (equal (ex-args->expand-lst x)
                     (pseudo-term-alist-fix expand-lst)))))

Theorem: ex-args-of-pseudo-term-list-fix-term-lst

(defthm ex-args-of-pseudo-term-list-fix-term-lst
  (equal (ex-args (pseudo-term-list-fix term-lst)
                  fn-lst fn-lvls wrld-fn-len expand-lst)
         (ex-args term-lst
                  fn-lst fn-lvls wrld-fn-len expand-lst)))

Theorem: ex-args-pseudo-term-list-equiv-congruence-on-term-lst

(defthm ex-args-pseudo-term-list-equiv-congruence-on-term-lst
  (implies (pseudo-term-list-equiv term-lst term-lst-equiv)
           (equal (ex-args term-lst
                           fn-lst fn-lvls wrld-fn-len expand-lst)
                  (ex-args term-lst-equiv
                           fn-lst fn-lvls wrld-fn-len expand-lst)))
  :rule-classes :congruence)

Theorem: ex-args-of-func-alist-fix-fn-lst

(defthm ex-args-of-func-alist-fix-fn-lst
  (equal (ex-args term-lst (func-alist-fix fn-lst)
                  fn-lvls wrld-fn-len expand-lst)
         (ex-args term-lst
                  fn-lst fn-lvls wrld-fn-len expand-lst)))

Theorem: ex-args-func-alist-equiv-congruence-on-fn-lst

(defthm ex-args-func-alist-equiv-congruence-on-fn-lst
  (implies (func-alist-equiv fn-lst fn-lst-equiv)
           (equal (ex-args term-lst
                           fn-lst fn-lvls wrld-fn-len expand-lst)
                  (ex-args term-lst fn-lst-equiv
                           fn-lvls wrld-fn-len expand-lst)))
  :rule-classes :congruence)

Theorem: ex-args-of-sym-nat-alist-fix-fn-lvls

(defthm ex-args-of-sym-nat-alist-fix-fn-lvls
  (equal (ex-args term-lst
                  fn-lst (sym-nat-alist-fix fn-lvls)
                  wrld-fn-len expand-lst)
         (ex-args term-lst
                  fn-lst fn-lvls wrld-fn-len expand-lst)))

Theorem: ex-args-sym-nat-alist-equiv-congruence-on-fn-lvls

(defthm ex-args-sym-nat-alist-equiv-congruence-on-fn-lvls
  (implies (sym-nat-alist-equiv fn-lvls fn-lvls-equiv)
           (equal (ex-args term-lst
                           fn-lst fn-lvls wrld-fn-len expand-lst)
                  (ex-args term-lst fn-lst
                           fn-lvls-equiv wrld-fn-len expand-lst)))
  :rule-classes :congruence)

Theorem: ex-args-of-nfix-wrld-fn-len

(defthm ex-args-of-nfix-wrld-fn-len
  (equal (ex-args term-lst
                  fn-lst fn-lvls (nfix wrld-fn-len)
                  expand-lst)
         (ex-args term-lst
                  fn-lst fn-lvls wrld-fn-len expand-lst)))

Theorem: ex-args-nat-equiv-congruence-on-wrld-fn-len

(defthm ex-args-nat-equiv-congruence-on-wrld-fn-len
  (implies (acl2::nat-equiv wrld-fn-len wrld-fn-len-equiv)
           (equal (ex-args term-lst
                           fn-lst fn-lvls wrld-fn-len expand-lst)
                  (ex-args term-lst fn-lst
                           fn-lvls wrld-fn-len-equiv expand-lst)))
  :rule-classes :congruence)

Theorem: ex-args-of-pseudo-term-alist-fix-expand-lst

(defthm ex-args-of-pseudo-term-alist-fix-expand-lst
  (equal (ex-args term-lst fn-lst fn-lvls wrld-fn-len
                  (pseudo-term-alist-fix expand-lst))
         (ex-args term-lst
                  fn-lst fn-lvls wrld-fn-len expand-lst)))

Theorem: ex-args-pseudo-term-alist-equiv-congruence-on-expand-lst

(defthm ex-args-pseudo-term-alist-equiv-congruence-on-expand-lst
  (implies (pseudo-term-alist-equiv expand-lst expand-lst-equiv)
           (equal (ex-args term-lst
                           fn-lst fn-lvls wrld-fn-len expand-lst)
                  (ex-args term-lst fn-lst
                           fn-lvls wrld-fn-len expand-lst-equiv)))
  :rule-classes :congruence)

Theorem: ex-args-fix-redef

(defthm ex-args-fix-redef
  (equal (ex-args-fix x)
         (ex-args (ex-args->term-lst x)
                  (ex-args->fn-lst x)
                  (ex-args->fn-lvls x)
                  (ex-args->wrld-fn-len x)
                  (ex-args->expand-lst x)))
  :rule-classes :definition)

Function: ex-outs-p

(defun ex-outs-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'ex-outs-p))
  (declare (ignorable acl2::__function__))
  (and
   (mbe
     :logic (and (alistp x)
                 (equal (strip-cars x)
                        '(expanded-term-lst expanded-fn-lst)))
     :exec
     (fty::alist-with-carsp x '(expanded-term-lst expanded-fn-lst)))
   (b* ((expanded-term-lst (cdr (std::da-nth 0 x)))
        (expanded-fn-lst (cdr (std::da-nth 1 x))))
     (and (pseudo-term-listp expanded-term-lst)
          (pseudo-term-alistp expanded-fn-lst))))))

Theorem: consp-when-ex-outs-p

(defthm consp-when-ex-outs-p
  (implies (ex-outs-p x) (consp x))
  :rule-classes :compound-recognizer)

Function: ex-outs-fix$inline

(defun ex-outs-fix$inline (x)
  (declare (xargs :guard (ex-outs-p x)))
  (let ((acl2::__function__ 'ex-outs-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((expanded-term-lst
                   (pseudo-term-list-fix (cdr (std::da-nth 0 x))))
              (expanded-fn-lst
                   (pseudo-term-alist-fix (cdr (std::da-nth 1 x)))))
           (list (cons 'expanded-term-lst
                       expanded-term-lst)
                 (cons 'expanded-fn-lst
                       expanded-fn-lst)))
         :exec x)))

Theorem: ex-outs-p-of-ex-outs-fix

(defthm ex-outs-p-of-ex-outs-fix
  (b* ((new-x (ex-outs-fix$inline x)))
    (ex-outs-p new-x))
  :rule-classes :rewrite)

Theorem: ex-outs-fix-when-ex-outs-p

(defthm ex-outs-fix-when-ex-outs-p
  (implies (ex-outs-p x)
           (equal (ex-outs-fix x) x)))

Function: ex-outs-equiv$inline

(defun ex-outs-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (ex-outs-p acl2::x)
                              (ex-outs-p acl2::y))))
  (equal (ex-outs-fix acl2::x)
         (ex-outs-fix acl2::y)))

Theorem: ex-outs-equiv-is-an-equivalence

(defthm ex-outs-equiv-is-an-equivalence
  (and (booleanp (ex-outs-equiv x y))
       (ex-outs-equiv x x)
       (implies (ex-outs-equiv x y)
                (ex-outs-equiv y x))
       (implies (and (ex-outs-equiv x y)
                     (ex-outs-equiv y z))
                (ex-outs-equiv x z)))
  :rule-classes (:equivalence))

Theorem: ex-outs-equiv-implies-equal-ex-outs-fix-1

(defthm ex-outs-equiv-implies-equal-ex-outs-fix-1
  (implies (ex-outs-equiv acl2::x x-equiv)
           (equal (ex-outs-fix acl2::x)
                  (ex-outs-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: ex-outs-fix-under-ex-outs-equiv

(defthm ex-outs-fix-under-ex-outs-equiv
  (ex-outs-equiv (ex-outs-fix acl2::x)
                 acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-ex-outs-fix-1-forward-to-ex-outs-equiv

(defthm equal-of-ex-outs-fix-1-forward-to-ex-outs-equiv
  (implies (equal (ex-outs-fix acl2::x) acl2::y)
           (ex-outs-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-ex-outs-fix-2-forward-to-ex-outs-equiv

(defthm equal-of-ex-outs-fix-2-forward-to-ex-outs-equiv
  (implies (equal acl2::x (ex-outs-fix acl2::y))
           (ex-outs-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: ex-outs-equiv-of-ex-outs-fix-1-forward

(defthm ex-outs-equiv-of-ex-outs-fix-1-forward
  (implies (ex-outs-equiv (ex-outs-fix acl2::x)
                          acl2::y)
           (ex-outs-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: ex-outs-equiv-of-ex-outs-fix-2-forward

(defthm ex-outs-equiv-of-ex-outs-fix-2-forward
  (implies (ex-outs-equiv acl2::x (ex-outs-fix acl2::y))
           (ex-outs-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Function: ex-outs->expanded-term-lst$inline

(defun ex-outs->expanded-term-lst$inline (x)
  (declare (xargs :guard (ex-outs-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-outs->expanded-term-lst))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (pseudo-term-list-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: pseudo-term-listp-of-ex-outs->expanded-term-lst

(defthm pseudo-term-listp-of-ex-outs->expanded-term-lst
  (b* ((expanded-term-lst (ex-outs->expanded-term-lst$inline x)))
    (pseudo-term-listp expanded-term-lst))
  :rule-classes :rewrite)

Theorem: ex-outs->expanded-term-lst$inline-of-ex-outs-fix-x

(defthm ex-outs->expanded-term-lst$inline-of-ex-outs-fix-x
  (equal (ex-outs->expanded-term-lst$inline (ex-outs-fix x))
         (ex-outs->expanded-term-lst$inline x)))

Theorem: ex-outs->expanded-term-lst$inline-ex-outs-equiv-congruence-on-x

(defthm
    ex-outs->expanded-term-lst$inline-ex-outs-equiv-congruence-on-x
  (implies (ex-outs-equiv x x-equiv)
           (equal (ex-outs->expanded-term-lst$inline x)
                  (ex-outs->expanded-term-lst$inline x-equiv)))
  :rule-classes :congruence)

Function: ex-outs->expanded-fn-lst$inline

(defun ex-outs->expanded-fn-lst$inline (x)
  (declare (xargs :guard (ex-outs-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'ex-outs->expanded-fn-lst))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (pseudo-term-alist-fix (cdr (std::da-nth 1 x))))
         :exec (cdr (std::da-nth 1 x)))))

Theorem: pseudo-term-alistp-of-ex-outs->expanded-fn-lst

(defthm pseudo-term-alistp-of-ex-outs->expanded-fn-lst
  (b* ((expanded-fn-lst (ex-outs->expanded-fn-lst$inline x)))
    (pseudo-term-alistp expanded-fn-lst))
  :rule-classes :rewrite)

Theorem: ex-outs->expanded-fn-lst$inline-of-ex-outs-fix-x

(defthm ex-outs->expanded-fn-lst$inline-of-ex-outs-fix-x
  (equal (ex-outs->expanded-fn-lst$inline (ex-outs-fix x))
         (ex-outs->expanded-fn-lst$inline x)))

Theorem: ex-outs->expanded-fn-lst$inline-ex-outs-equiv-congruence-on-x

(defthm
      ex-outs->expanded-fn-lst$inline-ex-outs-equiv-congruence-on-x
  (implies (ex-outs-equiv x x-equiv)
           (equal (ex-outs->expanded-fn-lst$inline x)
                  (ex-outs->expanded-fn-lst$inline x-equiv)))
  :rule-classes :congruence)

Function: ex-outs

(defun ex-outs (expanded-term-lst expanded-fn-lst)
 (declare (xargs :guard (and (pseudo-term-listp expanded-term-lst)
                             (pseudo-term-alistp expanded-fn-lst))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'ex-outs))
   (declare (ignorable acl2::__function__))
   (b* ((expanded-term-lst
             (mbe :logic (pseudo-term-list-fix expanded-term-lst)
                  :exec expanded-term-lst))
        (expanded-fn-lst
             (mbe :logic (pseudo-term-alist-fix expanded-fn-lst)
                  :exec expanded-fn-lst)))
     (list (cons 'expanded-term-lst
                 expanded-term-lst)
           (cons 'expanded-fn-lst
                 expanded-fn-lst)))))

Theorem: ex-outs-p-of-ex-outs

(defthm ex-outs-p-of-ex-outs
  (b* ((x (ex-outs expanded-term-lst expanded-fn-lst)))
    (ex-outs-p x))
  :rule-classes :rewrite)

Theorem: ex-outs->expanded-term-lst-of-ex-outs

(defthm ex-outs->expanded-term-lst-of-ex-outs
  (equal (ex-outs->expanded-term-lst
              (ex-outs expanded-term-lst expanded-fn-lst))
         (pseudo-term-list-fix expanded-term-lst)))

Theorem: ex-outs->expanded-fn-lst-of-ex-outs

(defthm ex-outs->expanded-fn-lst-of-ex-outs
  (equal (ex-outs->expanded-fn-lst
              (ex-outs expanded-term-lst expanded-fn-lst))
         (pseudo-term-alist-fix expanded-fn-lst)))

Theorem: ex-outs-of-fields

(defthm ex-outs-of-fields
  (equal (ex-outs (ex-outs->expanded-term-lst x)
                  (ex-outs->expanded-fn-lst x))
         (ex-outs-fix x)))

Theorem: ex-outs-fix-when-ex-outs

(defthm ex-outs-fix-when-ex-outs
  (equal (ex-outs-fix x)
         (ex-outs (ex-outs->expanded-term-lst x)
                  (ex-outs->expanded-fn-lst x))))

Theorem: equal-of-ex-outs

(defthm equal-of-ex-outs
  (equal (equal (ex-outs expanded-term-lst expanded-fn-lst)
                x)
         (and (ex-outs-p x)
              (equal (ex-outs->expanded-term-lst x)
                     (pseudo-term-list-fix expanded-term-lst))
              (equal (ex-outs->expanded-fn-lst x)
                     (pseudo-term-alist-fix expanded-fn-lst)))))

Theorem: ex-outs-of-pseudo-term-list-fix-expanded-term-lst

(defthm ex-outs-of-pseudo-term-list-fix-expanded-term-lst
  (equal (ex-outs (pseudo-term-list-fix expanded-term-lst)
                  expanded-fn-lst)
         (ex-outs expanded-term-lst expanded-fn-lst)))

Theorem: ex-outs-pseudo-term-list-equiv-congruence-on-expanded-term-lst

(defthm
     ex-outs-pseudo-term-list-equiv-congruence-on-expanded-term-lst
  (implies (pseudo-term-list-equiv expanded-term-lst
                                   expanded-term-lst-equiv)
           (equal (ex-outs expanded-term-lst expanded-fn-lst)
                  (ex-outs expanded-term-lst-equiv
                           expanded-fn-lst)))
  :rule-classes :congruence)

Theorem: ex-outs-of-pseudo-term-alist-fix-expanded-fn-lst

(defthm ex-outs-of-pseudo-term-alist-fix-expanded-fn-lst
  (equal (ex-outs expanded-term-lst
                  (pseudo-term-alist-fix expanded-fn-lst))
         (ex-outs expanded-term-lst expanded-fn-lst)))

Theorem: ex-outs-pseudo-term-alist-equiv-congruence-on-expanded-fn-lst

(defthm
      ex-outs-pseudo-term-alist-equiv-congruence-on-expanded-fn-lst
 (implies
     (pseudo-term-alist-equiv expanded-fn-lst expanded-fn-lst-equiv)
     (equal (ex-outs expanded-term-lst expanded-fn-lst)
            (ex-outs expanded-term-lst
                     expanded-fn-lst-equiv)))
 :rule-classes :congruence)

Theorem: ex-outs-fix-redef

(defthm ex-outs-fix-redef
  (equal (ex-outs-fix x)
         (ex-outs (ex-outs->expanded-term-lst x)
                  (ex-outs->expanded-fn-lst x)))
  :rule-classes :definition)

Function: sum-lvls

(defun sum-lvls (fn-lvls)
  (declare (xargs :guard (sym-nat-alistp fn-lvls)))
  (let ((acl2::__function__ 'sum-lvls))
    (declare (ignorable acl2::__function__))
    (b* ((fn-lvls (sym-nat-alist-fix fn-lvls))
         ((unless (consp fn-lvls)) 0)
         ((cons first rest) fn-lvls)
         ((cons & lvl) first))
      (+ lvl (sum-lvls rest)))))

Theorem: natp-of-sum-lvls

(defthm natp-of-sum-lvls
  (b* ((sum (sum-lvls fn-lvls)))
    (natp sum))
  :rule-classes :rewrite)

Theorem: sum-lvls-decrease-after-update

(defthm sum-lvls-decrease-after-update
  (implies (and (symbolp fn)
                (sym-nat-alistp fn-lvls)
                (consp fn-lvls)
                (assoc-equal fn fn-lvls)
                (not (equal (cdr (assoc-equal fn fn-lvls))
                            0)))
           (< (sum-lvls (update-fn-lvls fn fn-lvls))
              (sum-lvls fn-lvls))))

Function: expand-measure

(defun expand-measure (expand-args)
  (declare (xargs :guard (ex-args-p expand-args)))
  (let ((acl2::__function__ 'expand-measure))
    (declare (ignorable acl2::__function__))
    (b* ((expand-args (ex-args-fix expand-args))
         ((ex-args a) expand-args)
         (lvl-sum (sum-lvls a.fn-lvls)))
      (list a.wrld-fn-len
            lvl-sum (acl2-count a.term-lst)))))

Theorem: nat-listp-of-expand-measure

(defthm nat-listp-of-expand-measure
  (b* ((m (expand-measure expand-args)))
    (nat-listp m))
  :rule-classes :rewrite)

Theorem: pseudo-term-list-of-cdar-of-ex-args->term-lst

(defthm pseudo-term-list-of-cdar-of-ex-args->term-lst
  (implies
       (and (ex-args-p expand-args)
            (consp (ex-args->term-lst expand-args))
            (consp (car (ex-args->term-lst expand-args)))
            (not (equal (caar (ex-args->term-lst expand-args))
                        'quote)))
       (pseudo-term-listp (cdar (ex-args->term-lst expand-args)))))

Theorem: pseudo-term-listp-of-cdr-of-ex-args->term-lst

(defthm pseudo-term-listp-of-cdr-of-ex-args->term-lst
  (implies
       (and (ex-args-p expand-args)
            (consp (ex-args->term-lst expand-args)))
       (pseudo-term-listp (cdr (ex-args->term-lst expand-args)))))

Theorem: symbolp-of-car-of-ex-args->term-lst

(defthm symbolp-of-car-of-ex-args->term-lst
  (implies (and (ex-args-p expand-args)
                (consp (ex-args->term-lst expand-args))
                (not (consp (car (ex-args->term-lst expand-args)))))
           (symbolp (car (ex-args->term-lst expand-args)))))

Theorem: pseudo-termp-of-car-of-ex-args->term-lst

(defthm pseudo-termp-of-car-of-ex-args->term-lst
  (implies (and (ex-args-p expand-args)
                (consp (ex-args->term-lst expand-args)))
           (pseudo-termp (car (ex-args->term-lst expand-args)))))

Theorem: len-equal-of-formals-of-pseudo-lambdap-and-actuals-of-pseudo-termp

(defthm
 len-equal-of-formals-of-pseudo-lambdap-and-actuals-of-pseudo-termp
 (implies
  (and (ex-args-p expand-args)
       (pseudo-termp (car (ex-args->term-lst expand-args)))
       (pseudo-lambdap (car (car (ex-args->term-lst expand-args)))))
  (equal (len (cadr (car (car (ex-args->term-lst expand-args)))))
         (len (cdr (car (ex-args->term-lst expand-args)))))))

Theorem: symbolp-of-caar-of-ex-args->term-lst

(defthm symbolp-of-caar-of-ex-args->term-lst
 (implies
  (and
   (ex-args-p expand-args)
   (consp (ex-args->term-lst expand-args))
   (not (symbolp (car (ex-args->term-lst expand-args))))
   (not
      (pseudo-lambdap (car (car (ex-args->term-lst expand-args))))))
  (symbolp (car (car (ex-args->term-lst expand-args))))))

Theorem: not-cddr-of-car-of-pseudo-term-list-fix-of-expand-args->term-lst

(defthm
   not-cddr-of-car-of-pseudo-term-list-fix-of-expand-args->term-lst
 (implies (and (consp (ex-args->term-lst expand-args))
               (consp (car (ex-args->term-lst expand-args)))
               (not (symbolp (car (ex-args->term-lst expand-args))))
               (equal (car (car (ex-args->term-lst expand-args)))
                      'quote))
          (not (cddr (car (ex-args->term-lst expand-args))))))

Theorem: consp-cdr-of-car-of-pseudo-term-list-fix-of-expand-args->term-lst

(defthm
  consp-cdr-of-car-of-pseudo-term-list-fix-of-expand-args->term-lst
 (implies (and (consp (ex-args->term-lst expand-args))
               (consp (car (ex-args->term-lst expand-args)))
               (not (symbolp (car (ex-args->term-lst expand-args))))
               (equal (car (car (ex-args->term-lst expand-args)))
                      'quote))
          (consp (cdr (car (ex-args->term-lst expand-args))))))

Theorem: pseudo-term-listp-of-pseudo-lambdap-of-cdar-ex-args->term-lst

(defthm
      pseudo-term-listp-of-pseudo-lambdap-of-cdar-ex-args->term-lst
  (implies
       (and (ex-args-p expand-args)
            (consp (ex-args->term-lst expand-args))
            (consp (car (ex-args->term-lst expand-args)))
            (not (equal (caar (ex-args->term-lst expand-args))
                        'quote)))
       (pseudo-term-listp (cdar (ex-args->term-lst expand-args)))))

Theorem: integerp-of-cdr-of-assoc-equal-of-ex-args->fn-lvls-of-ex-args-p

(defthm
    integerp-of-cdr-of-assoc-equal-of-ex-args->fn-lvls-of-ex-args-p
  (implies (and (ex-args-p x)
                (assoc-equal foo (ex-args->fn-lvls x)))
           (integerp (cdr (assoc-equal foo (ex-args->fn-lvls x))))))

Theorem: non-neg-of-cdr-of-assoc-equal-of-ex-args->fn-lvls-of-ex-args-p

(defthm
     non-neg-of-cdr-of-assoc-equal-of-ex-args->fn-lvls-of-ex-args-p
  (implies (and (ex-args-p x)
                (assoc-equal foo (ex-args->fn-lvls x)))
           (<= 0
               (cdr (assoc-equal foo (ex-args->fn-lvls x))))))

Theorem: consp-of-assoc-equal-of-ex-args->fn-lvls-of-ex-args-p

(defthm consp-of-assoc-equal-of-ex-args->fn-lvls-of-ex-args-p
  (implies (and (ex-args-p x)
                (assoc-equal foo (ex-args->fn-lvls x)))
           (consp (assoc-equal foo (ex-args->fn-lvls x)))))

Theorem: last-<=

(defthm last-<=
  (<= (acl2-count (last x))
      (acl2-count x)))

Theorem: last-pseudo-term-list-is-pseudo-term-list

(defthm last-pseudo-term-list-is-pseudo-term-list
  (implies (pseudo-term-listp x)
           (pseudo-term-listp (last x))))

Function: expand

(defun expand (expand-args fty-info abs state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (ex-args-p expand-args)
                             (fty-info-alist-p fty-info)
                             (symbol-listp abs))))
 (let ((acl2::__function__ 'expand))
  (declare (ignorable acl2::__function__))
  (b*
   ((expand-args (ex-args-fix expand-args))
    (fty-info (fty-info-alist-fix fty-info))
    ((ex-args a) expand-args)
    ((unless (consp a.term-lst))
     (make-ex-outs :expanded-term-lst nil
                   :expanded-fn-lst a.expand-lst))
    ((cons term rest) a.term-lst)
    ((if (symbolp term))
     (b* ((rest-res (expand (change-ex-args a :term-lst rest)
                            fty-info abs state))
          ((ex-outs o) rest-res))
       (make-ex-outs
            :expanded-term-lst (cons term o.expanded-term-lst)
            :expanded-fn-lst o.expanded-fn-lst)))
    ((if (equal (car term) 'quote))
     (b* ((rest-res (expand (change-ex-args a :term-lst rest)
                            fty-info abs state))
          ((ex-outs o) rest-res))
       (make-ex-outs
            :expanded-term-lst (cons term o.expanded-term-lst)
            :expanded-fn-lst o.expanded-fn-lst)))
    ((cons fn-call fn-actuals) term)
    ((if (pseudo-lambdap fn-call))
     (b*
      ((lambda-formals (lambda-formals fn-call))
       (body-res
        (expand
             (change-ex-args a
                             :term-lst (list (lambda-body fn-call)))
             fty-info abs state))
       ((ex-outs b) body-res)
       (lambda-body (car b.expanded-term-lst))
       (actuals-res
            (expand (change-ex-args a
                                    :term-lst fn-actuals
                                    :expand-lst b.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs ac) actuals-res)
       (lambda-actuals ac.expanded-term-lst)
       ((unless (mbt (equal (len lambda-formals)
                            (len lambda-actuals))))
        (make-ex-outs :expanded-term-lst a.term-lst
                      :expanded-fn-lst a.expand-lst))
       (lambda-fn
          (cons (cons 'lambda
                      (cons lambda-formals (cons lambda-body 'nil)))
                lambda-actuals))
       (rest-res
            (expand (change-ex-args a
                                    :term-lst rest
                                    :expand-lst ac.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs r) rest-res))
      (make-ex-outs
           :expanded-term-lst (cons lambda-fn r.expanded-term-lst)
           :expanded-fn-lst r.expanded-fn-lst)))
    ((unless (mbt (symbolp fn-call)))
     (make-ex-outs :expanded-term-lst a.term-lst
                   :expanded-fn-lst a.expand-lst))
    (fn (hons-get fn-call a.fn-lst))
    ((unless fn)
     (b*
      (((unless (function-symbolp fn-call (w state)))
        (prog2$ (er hard? 'smt-goal-generator=>expand
                    "Should be a function call: ~q0"
                    fn-call)
                (make-ex-outs :expanded-term-lst a.term-lst
                              :expanded-fn-lst a.expand-lst)))
       (basic-function (member-equal fn-call *smt-basics*))
       (flex? (fncall-of-flextype fn-call fty-info))
       (abs? (member-equal fn-call abs))
       (lvl-item (assoc-equal fn-call a.fn-lvls))
       (extract-res (meta-extract-formula fn-call state))
       ((if (equal fn-call 'return-last))
        (b*
         ((actuals-res
               (expand (change-ex-args a
                                       :term-lst (last fn-actuals))
                       fty-info abs state))
          ((ex-outs ac) actuals-res)
          (rest-res
             (expand (change-ex-args a
                                     :term-lst rest
                                     :expand-lst ac.expanded-fn-lst)
                     fty-info abs state))
          ((ex-outs r) rest-res))
         (make-ex-outs
              :expanded-term-lst (cons (car ac.expanded-term-lst)
                                       r.expanded-term-lst)
              :expanded-fn-lst r.expanded-fn-lst)))
       ((if (or basic-function
                flex? abs? (<= a.wrld-fn-len 0)
                (and lvl-item (zp (cdr lvl-item)))
                (equal extract-res ''t)))
        (b*
         ((actuals-res
               (expand (change-ex-args a :term-lst fn-actuals)
                       fty-info abs state))
          ((ex-outs ac) actuals-res)
          (rest-res
             (expand (change-ex-args a
                                     :term-lst rest
                                     :expand-lst ac.expanded-fn-lst)
                     fty-info abs state))
          ((ex-outs r) rest-res))
         (make-ex-outs :expanded-term-lst
                       (cons (cons fn-call ac.expanded-term-lst)
                             r.expanded-term-lst)
                       :expanded-fn-lst r.expanded-fn-lst)))
       (formals (formals fn-call (w state)))
       ((unless (symbol-listp formals))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "formals get a list that's not a symbol-listp for ~q0, the formals are ~q1"
          fn-call formals)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst a.expand-lst)))
       ((unless (true-listp extract-res))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "meta-extract-formula returning a non-true-listp for ~q0The extracted result is ~q1"
          fn-call extract-res)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst a.expand-lst)))
       (body (nth 2 extract-res))
       ((unless (pseudo-termp body))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "meta-extract-formula returning a non-pseudo-term for ~q0The body is ~q1"
          fn-call body)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst a.expand-lst)))
       (updated-expand-lst (if (assoc-equal term a.expand-lst)
                               a.expand-lst
                             (cons (cons term term) a.expand-lst)))
       (body-res
        (expand
         (change-ex-args a
                         :term-lst (list body)
                         :fn-lvls (cons (cons fn-call '0) a.fn-lvls)
                         :wrld-fn-len (1- a.wrld-fn-len)
                         :expand-lst updated-expand-lst)
         fty-info abs state))
       ((ex-outs b) body-res)
       (expanded-lambda-body (car b.expanded-term-lst))
       (expanded-lambda
            (cons 'lambda
                  (cons formals
                        (cons expanded-lambda-body 'nil))))
       (actuals-res
            (expand (change-ex-args a
                                    :term-lst fn-actuals
                                    :expand-lst b.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs ac) actuals-res)
       (expanded-term-list ac.expanded-term-lst)
       ((unless (equal (len formals)
                       (len expanded-term-list)))
        (prog2$
         (er
          hard? 'smt-goal-generator=>expand
          "You called your function with the wrong number of actuals: ~q0"
          term)
         (make-ex-outs :expanded-term-lst a.term-lst
                       :expanded-fn-lst ac.expanded-fn-lst)))
       (rest-res
            (expand (change-ex-args a
                                    :term-lst rest
                                    :expand-lst ac.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs r) rest-res))
      (make-ex-outs :expanded-term-lst
                    (cons (cons expanded-lambda expanded-term-list)
                          r.expanded-term-lst)
                    :expanded-fn-lst r.expanded-fn-lst)))
    (lvl-item (assoc-equal fn-call a.fn-lvls))
    ((unless lvl-item)
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "Function ~q0 exists in the definition list but not in the levels list?"
       fn-call)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst a.expand-lst)))
    ((if (zp (cdr lvl-item)))
     (b*
      ((actuals-res (expand (change-ex-args a :term-lst fn-actuals)
                            fty-info abs state))
       ((ex-outs ac) actuals-res)
       (rest-res
            (expand (change-ex-args a
                                    :term-lst rest
                                    :expand-lst ac.expanded-fn-lst)
                    fty-info abs state))
       ((ex-outs r) rest-res))
      (make-ex-outs
        :expanded-term-lst (cons (cons fn-call ac.expanded-term-lst)
                                 r.expanded-term-lst)
        :expanded-fn-lst r.expanded-fn-lst)))
    (new-fn-lvls (update-fn-lvls fn-call a.fn-lvls))
    ((func f) (cdr fn))
    (extract-res (meta-extract-formula fn-call state))
    ((unless (true-listp extract-res))
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "meta-extract-formula returning a non-true-listp for ~q0The extracted result is ~q1"
       fn-call extract-res)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst a.expand-lst)))
    (body (nth 2 extract-res))
    ((unless (pseudo-termp body))
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "meta-extract-formula returning a non-pseudo-term for ~q0The body is ~q1"
       fn-call body)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst a.expand-lst)))
    (updated-expand-lst (if (assoc-equal term a.expand-lst)
                            a.expand-lst
                          (cons (cons term term) a.expand-lst)))
    (formals f.flattened-formals)
    (body-res
         (expand (change-ex-args a
                                 :term-lst (list body)
                                 :fn-lvls new-fn-lvls
                                 :expand-lst updated-expand-lst)
                 fty-info abs state))
    ((ex-outs b) body-res)
    (expanded-lambda-body (car b.expanded-term-lst))
    (expanded-lambda (cons 'lambda
                           (cons formals
                                 (cons expanded-lambda-body 'nil))))
    (actuals-res
         (expand (change-ex-args a
                                 :term-lst fn-actuals
                                 :expand-lst b.expanded-fn-lst)
                 fty-info abs state))
    ((ex-outs ac) actuals-res)
    (expanded-term-list ac.expanded-term-lst)
    ((unless (equal (len formals)
                    (len expanded-term-list)))
     (prog2$
      (er
       hard? 'smt-goal-generator=>expand
       "You called your function with the wrong number of actuals: ~q0"
       term)
      (make-ex-outs :expanded-term-lst a.term-lst
                    :expanded-fn-lst ac.expanded-fn-lst)))
    (rest-res
         (expand (change-ex-args a
                                 :term-lst rest
                                 :expand-lst ac.expanded-fn-lst)
                 fty-info abs state))
    ((ex-outs r) rest-res))
   (make-ex-outs :expanded-term-lst
                 (cons (cons expanded-lambda expanded-term-list)
                       r.expanded-term-lst)
                 :expanded-fn-lst r.expanded-fn-lst))))

Theorem: ex-outs-p-of-expand

(defthm ex-outs-p-of-expand
  (b* ((expanded-result (expand expand-args fty-info abs state)))
    (ex-outs-p expanded-result))
  :rule-classes :rewrite)

Theorem: pseudo-term-alistp-of-expand

(defthm pseudo-term-alistp-of-expand
 (b* ((expanded-result (expand expand-args fty-info abs state)))
  (implies
   (ex-args-p expand-args)
   (pseudo-term-alistp (ex-outs->expanded-fn-lst expanded-result))))
 :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-expand

(defthm pseudo-term-listp-of-expand
  (b* ((expanded-result (expand expand-args fty-info abs state)))
    (implies (ex-args-p expand-args)
             (pseudo-term-listp
                  (ex-outs->expanded-term-lst expanded-result))))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-car-of-expand

(defthm pseudo-termp-of-car-of-expand
  (b* ((expanded-result (expand expand-args fty-info abs state)))
    (implies
         (ex-args-p expand-args)
         (pseudo-termp
              (car (ex-outs->expanded-term-lst expanded-result)))))
  :rule-classes :rewrite)

Theorem: len-of-expand

(defthm len-of-expand
 (b* ((expanded-result (expand expand-args fty-info abs state)))
  (implies (ex-args-p expand-args)
           (equal (len (ex-outs->expanded-term-lst expanded-result))
                  (len (ex-args->term-lst expand-args)))))
 :rule-classes :rewrite)

Subtopics

Ex-args

Argument list for function expand

Expand

Expand-measure

ACL2::measure function for proving termination of function expand.

Ex-outs

Outputs for function expand