• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
      • Z3-installation
      • Smt-hint
      • Tutorial
      • Status
      • Developer
        • Verified
        • Trusted
          • Translation-datatypes
          • Smt-run
          • Smt-prove
          • Smt-write
          • Smt-trusted-cp
          • Z3-py
            • Smt-translator
              • Paragraphp
            • Smt-translate-fty
            • Smt-names
            • Smt-recover-types
            • Smt-pretty-print
            • Smt-header
            • Smt-translate-abstract-sort
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Bitcoin
    • Riscv
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Bigmems
    • Builtins
    • Execloader
    • Aleo
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Z3-py

Smt-translator

SMT-translator does the LISP to Python translation.

Definitions and Theorems

Function: smt-numberp

(defun smt-numberp (sym)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'smt-numberp))
    (declare (ignorable acl2::__function__))
    (if (or (rationalp sym)
            (integerp sym)
            (real/rationalp sym))
        t
      nil)))

Theorem: booleanp-of-smt-numberp

(defthm booleanp-of-smt-numberp
  (b* ((is? (smt-numberp sym)))
    (booleanp is?))
  :rule-classes :rewrite)

Function: smt-number-fix

(defun smt-number-fix (num)
  (declare (xargs :guard (smt-numberp num)))
  (let ((acl2::__function__ 'smt-number-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic (if (smt-numberp num) num 0)
         :exec num)))

Theorem: smt-numberp-of-smt-number-fix

(defthm smt-numberp-of-smt-number-fix
  (b* ((fixed (smt-number-fix num)))
    (smt-numberp fixed))
  :rule-classes :rewrite)

Function: smt-number-equiv$inline

(defun smt-number-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (smt-numberp acl2::x)
                              (smt-numberp acl2::y))))
  (equal (smt-number-fix acl2::x)
         (smt-number-fix acl2::y)))

Theorem: smt-number-equiv-is-an-equivalence

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

Theorem: smt-number-equiv-implies-equal-smt-number-fix-1

(defthm smt-number-equiv-implies-equal-smt-number-fix-1
  (implies (smt-number-equiv acl2::x x-equiv)
           (equal (smt-number-fix acl2::x)
                  (smt-number-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: smt-number-fix-under-smt-number-equiv

(defthm smt-number-fix-under-smt-number-equiv
  (smt-number-equiv (smt-number-fix acl2::x)
                    acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Function: translate-function

(defun translate-function (opr)
  (declare (xargs :guard (symbolp opr)))
  (let ((acl2::__function__ 'translate-function))
    (declare (ignorable acl2::__function__))
    (b* ((fn-sig (cdr (assoc-equal opr *smt-functions*)))
         ((if (equal fn-sig nil))
          (prog2$ (er hard?
                      'smt-translator=>translate-function
                      "Not a basic SMT function: ~q0" opr)
                  (mv "" 0)))
         ((cons translated-fn nargs) fn-sig))
      (mv translated-fn nargs))))

Theorem: stringp-of-translate-function.translated

(defthm stringp-of-translate-function.translated
  (b* (((mv ?translated ?nargs)
        (translate-function opr)))
    (stringp translated))
  :rule-classes :rewrite)

Theorem: natp-of-translate-function.nargs

(defthm natp-of-translate-function.nargs
  (b* (((mv ?translated ?nargs)
        (translate-function opr)))
    (natp nargs))
  :rule-classes :rewrite)

Theorem: wordp-of-translate-function

(defthm wordp-of-translate-function
  (b* (((mv fn &) (translate-function x)))
    (wordp fn)))

Function: translate-number

(defun translate-number (num)
  (declare (xargs :guard (smt-numberp num)))
  (let ((acl2::__function__ 'translate-number))
    (declare (ignorable acl2::__function__))
    (b* ((num (smt-number-fix num))
         ((if (and (rationalp num)
                   (not (integerp num))))
          (cons '"_SMT_.Qx("
                (cons (numerator num)
                      (cons '","
                            (cons (denominator num) '(")")))))))
      (list num))))

Theorem: paragraphp-of-translate-number

(defthm paragraphp-of-translate-number
  (b* ((translated (translate-number num)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: symbol-string-alistp

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

Theorem: symbol-string-alistp-of-revappend

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

Theorem: symbol-string-alistp-of-remove

(defthm symbol-string-alistp-of-remove
  (implies (symbol-string-alistp acl2::x)
           (symbol-string-alistp (remove acl2::a acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-last

(defthm symbol-string-alistp-of-last
  (implies (symbol-string-alistp (double-rewrite acl2::x))
           (symbol-string-alistp (last acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-nthcdr

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

Theorem: symbol-string-alistp-of-butlast

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

Theorem: symbol-string-alistp-of-update-nth

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

Theorem: symbol-string-alistp-of-repeat

(defthm symbol-string-alistp-of-repeat
  (iff (symbol-string-alistp (acl2::repeat acl2::n acl2::x))
       (or (and (consp acl2::x)
                (symbolp (car acl2::x))
                (stringp (cdr acl2::x)))
           (zp acl2::n)))
  :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-take

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

Theorem: symbol-string-alistp-of-union-equal

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

Theorem: symbol-string-alistp-of-intersection-equal-2

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

Theorem: symbol-string-alistp-of-intersection-equal-1

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

Theorem: symbol-string-alistp-of-set-difference-equal

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

Theorem: symbol-string-alistp-when-subsetp-equal

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

Theorem: symbol-string-alistp-of-rcons

(defthm symbol-string-alistp-of-rcons
  (iff (symbol-string-alistp (acl2::rcons acl2::a acl2::x))
       (and (and (consp acl2::a)
                 (symbolp (car acl2::a))
                 (stringp (cdr acl2::a)))
            (symbol-string-alistp (acl2::list-fix acl2::x))))
  :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-append

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

Theorem: symbol-string-alistp-of-rev

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

Theorem: symbol-string-alistp-of-duplicated-members

(defthm symbol-string-alistp-of-duplicated-members
 (implies (symbol-string-alistp acl2::x)
          (symbol-string-alistp (acl2::duplicated-members acl2::x)))
 :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-difference

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

Theorem: symbol-string-alistp-of-intersect-2

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

Theorem: symbol-string-alistp-of-intersect-1

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

Theorem: symbol-string-alistp-of-union

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

Theorem: symbol-string-alistp-of-mergesort

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

Theorem: symbol-string-alistp-of-delete

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

Theorem: symbol-string-alistp-of-insert

(defthm symbol-string-alistp-of-insert
  (iff (symbol-string-alistp (set::insert acl2::a acl2::x))
       (and (symbol-string-alistp (set::sfix acl2::x))
            (and (consp acl2::a)
                 (symbolp (car acl2::a))
                 (stringp (cdr acl2::a)))))
  :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-sfix

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

Theorem: symbol-string-alistp-of-list-fix

(defthm symbol-string-alistp-of-list-fix
  (implies (symbol-string-alistp acl2::x)
           (symbol-string-alistp (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-symbol-string-alistp-compound-recognizer

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

Theorem: symbol-string-alistp-when-not-consp

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

Theorem: symbol-string-alistp-of-cdr-when-symbol-string-alistp

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

Theorem: symbol-string-alistp-of-cons

(defthm symbol-string-alistp-of-cons
  (equal (symbol-string-alistp (cons acl2::a acl2::x))
         (and (and (consp acl2::a)
                   (symbolp (car acl2::a))
                   (stringp (cdr acl2::a)))
              (symbol-string-alistp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-make-fal

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

Theorem: stringp-of-cdr-when-member-equal-of-symbol-string-alistp

(defthm stringp-of-cdr-when-member-equal-of-symbol-string-alistp
  (and (implies (and (symbol-string-alistp acl2::x)
                     (member-equal acl2::a acl2::x))
                (stringp (cdr acl2::a)))
       (implies (and (member-equal acl2::a acl2::x)
                     (symbol-string-alistp acl2::x))
                (stringp (cdr acl2::a))))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-car-when-member-equal-of-symbol-string-alistp

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

Theorem: consp-when-member-equal-of-symbol-string-alistp

(defthm consp-when-member-equal-of-symbol-string-alistp
  (implies (and (symbol-string-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)
                                     (symbol-string-alistp acl2::x)
                                   'nil)
                                 (consp acl2::a)))))

Theorem: symbol-string-alistp-of-remove-assoc

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

Theorem: symbol-string-alistp-of-put-assoc

(defthm symbol-string-alistp-of-put-assoc
  (implies (and (symbol-string-alistp acl2::x))
           (iff (symbol-string-alistp
                     (put-assoc-equal acl2::name acl2::val acl2::x))
                (and (symbolp acl2::name)
                     (stringp acl2::val))))
  :rule-classes ((:rewrite)))

Theorem: symbol-string-alistp-of-fast-alist-clean

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

Theorem: symbol-string-alistp-of-hons-shrink-alist

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

Theorem: symbol-string-alistp-of-hons-acons

(defthm symbol-string-alistp-of-hons-acons
  (equal (symbol-string-alistp (hons-acons acl2::a acl2::n acl2::x))
         (and (symbolp acl2::a)
              (stringp acl2::n)
              (symbol-string-alistp acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: stringp-of-cdr-of-hons-assoc-equal-when-symbol-string-alistp

(defthm stringp-of-cdr-of-hons-assoc-equal-when-symbol-string-alistp
  (implies (symbol-string-alistp acl2::x)
           (iff (stringp (cdr (hons-assoc-equal acl2::k acl2::x)))
                (or (hons-assoc-equal acl2::k acl2::x)
                    (stringp nil))))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-symbol-string-alistp-rewrite

(defthm alistp-when-symbol-string-alistp-rewrite
  (implies (symbol-string-alistp acl2::x)
           (alistp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-symbol-string-alistp

(defthm alistp-when-symbol-string-alistp
  (implies (symbol-string-alistp acl2::x)
           (alistp acl2::x))
  :rule-classes :tau-system)

Theorem: stringp-of-cdar-when-symbol-string-alistp

(defthm stringp-of-cdar-when-symbol-string-alistp
  (implies (symbol-string-alistp acl2::x)
           (iff (stringp (cdar acl2::x))
                (or (consp acl2::x) (stringp nil))))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-caar-when-symbol-string-alistp

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

Function: symbol-string-alist-fix$inline

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

Theorem: symbol-string-alistp-of-symbol-string-alist-fix

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

Theorem: symbol-string-alist-fix-when-symbol-string-alistp

(defthm symbol-string-alist-fix-when-symbol-string-alistp
  (implies (symbol-string-alistp x)
           (equal (symbol-string-alist-fix x) x)))

Function: symbol-string-alist-equiv$inline

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

Theorem: symbol-string-alist-equiv-is-an-equivalence

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

Theorem: symbol-string-alist-equiv-implies-equal-symbol-string-alist-fix-1

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

Theorem: symbol-string-alist-fix-under-symbol-string-alist-equiv

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

Theorem: equal-of-symbol-string-alist-fix-1-forward-to-symbol-string-alist-equiv

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

Theorem: equal-of-symbol-string-alist-fix-2-forward-to-symbol-string-alist-equiv

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

Theorem: symbol-string-alist-equiv-of-symbol-string-alist-fix-1-forward

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

Theorem: symbol-string-alist-equiv-of-symbol-string-alist-fix-2-forward

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

Theorem: cons-of-symbol-fix-k-under-symbol-string-alist-equiv

(defthm cons-of-symbol-fix-k-under-symbol-string-alist-equiv
  (symbol-string-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-symbol-string-alist-equiv

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

Theorem: cons-of-str-fix-v-under-symbol-string-alist-equiv

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

Theorem: cons-streqv-congruence-on-v-under-symbol-string-alist-equiv

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

Theorem: cons-of-symbol-string-alist-fix-y-under-symbol-string-alist-equiv

(defthm
  cons-of-symbol-string-alist-fix-y-under-symbol-string-alist-equiv
 (symbol-string-alist-equiv (cons acl2::x
                                  (symbol-string-alist-fix acl2::y))
                            (cons acl2::x acl2::y)))

Theorem: cons-symbol-string-alist-equiv-congruence-on-y-under-symbol-string-alist-equiv

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

Theorem: symbol-string-alist-fix-of-acons

(defthm symbol-string-alist-fix-of-acons
  (equal (symbol-string-alist-fix (cons (cons acl2::a acl2::b) x))
         (cons (cons (symbol-fix acl2::a)
                     (str-fix acl2::b))
               (symbol-string-alist-fix x))))

Theorem: symbol-string-alist-fix-of-append

(defthm symbol-string-alist-fix-of-append
  (equal (symbol-string-alist-fix (append std::a std::b))
         (append (symbol-string-alist-fix std::a)
                 (symbol-string-alist-fix std::b))))

Theorem: consp-car-of-symbol-string-alist-fix

(defthm consp-car-of-symbol-string-alist-fix
  (equal (consp (car (symbol-string-alist-fix x)))
         (consp (symbol-string-alist-fix x))))

Function: te-args-p

(defun te-args-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'te-args-p))
  (declare (ignorable acl2::__function__))
  (and
    (mbe :logic
         (and (alistp x)
              (equal (strip-cars x)
                     '(expr-lst fn-lst fty-info symbol-index
                                symbol-list avoid-list symbol-map)))
         :exec (fty::alist-with-carsp
                    x
                    '(expr-lst fn-lst fty-info symbol-index
                               symbol-list avoid-list symbol-map)))
    (b* ((expr-lst (cdr (std::da-nth 0 x)))
         (fn-lst (cdr (std::da-nth 1 x)))
         (fty-info (cdr (std::da-nth 2 x)))
         (symbol-index (cdr (std::da-nth 3 x)))
         (symbol-list (cdr (std::da-nth 4 x)))
         (avoid-list (cdr (std::da-nth 5 x)))
         (symbol-map (cdr (std::da-nth 6 x))))
      (and (pseudo-term-listp expr-lst)
           (func-alistp fn-lst)
           (fty-info-alist-p fty-info)
           (natp symbol-index)
           (string-listp symbol-list)
           (symbol-listp avoid-list)
           (symbol-string-alistp symbol-map))))))

Theorem: consp-when-te-args-p

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

Function: te-args-fix$inline

(defun te-args-fix$inline (x)
 (declare (xargs :guard (te-args-p x)))
 (let ((acl2::__function__ 'te-args-fix))
  (declare (ignorable acl2::__function__))
  (mbe
   :logic
   (b*
    ((expr-lst (pseudo-term-list-fix (cdr (std::da-nth 0 x))))
     (fn-lst (func-alist-fix (cdr (std::da-nth 1 x))))
     (fty-info (fty-info-alist-fix (cdr (std::da-nth 2 x))))
     (symbol-index (nfix (cdr (std::da-nth 3 x))))
     (symbol-list (str::string-list-fix (cdr (std::da-nth 4 x))))
     (avoid-list (symbol-list-fix (cdr (std::da-nth 5 x))))
     (symbol-map (symbol-string-alist-fix (cdr (std::da-nth 6 x)))))
    (list (cons 'expr-lst expr-lst)
          (cons 'fn-lst fn-lst)
          (cons 'fty-info fty-info)
          (cons 'symbol-index symbol-index)
          (cons 'symbol-list symbol-list)
          (cons 'avoid-list avoid-list)
          (cons 'symbol-map symbol-map)))
   :exec x)))

Theorem: te-args-p-of-te-args-fix

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

Theorem: te-args-fix-when-te-args-p

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

Function: te-args-equiv$inline

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

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

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

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

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

Theorem: te-args-fix-under-te-args-equiv

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

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

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

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

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

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

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

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

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

Function: te-args->expr-lst$inline

(defun te-args->expr-lst$inline (x)
  (declare (xargs :guard (te-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'te-args->expr-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-te-args->expr-lst

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

Theorem: te-args->expr-lst$inline-of-te-args-fix-x

(defthm te-args->expr-lst$inline-of-te-args-fix-x
  (equal (te-args->expr-lst$inline (te-args-fix x))
         (te-args->expr-lst$inline x)))

Theorem: te-args->expr-lst$inline-te-args-equiv-congruence-on-x

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

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

(defun te-args->fn-lst$inline (x)
  (declare (xargs :guard (te-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'te-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-te-args->fn-lst

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

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

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

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

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

Function: te-args->fty-info$inline

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

Theorem: fty-info-alist-p-of-te-args->fty-info

(defthm fty-info-alist-p-of-te-args->fty-info
  (b* ((fty-info (te-args->fty-info$inline x)))
    (fty-info-alist-p fty-info))
  :rule-classes :rewrite)

Theorem: te-args->fty-info$inline-of-te-args-fix-x

(defthm te-args->fty-info$inline-of-te-args-fix-x
  (equal (te-args->fty-info$inline (te-args-fix x))
         (te-args->fty-info$inline x)))

Theorem: te-args->fty-info$inline-te-args-equiv-congruence-on-x

(defthm te-args->fty-info$inline-te-args-equiv-congruence-on-x
  (implies (te-args-equiv x x-equiv)
           (equal (te-args->fty-info$inline x)
                  (te-args->fty-info$inline x-equiv)))
  :rule-classes :congruence)

Function: te-args->symbol-index$inline

(defun te-args->symbol-index$inline (x)
  (declare (xargs :guard (te-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'te-args->symbol-index))
    (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-te-args->symbol-index

(defthm natp-of-te-args->symbol-index
  (b* ((symbol-index (te-args->symbol-index$inline x)))
    (natp symbol-index))
  :rule-classes :rewrite)

Theorem: te-args->symbol-index$inline-of-te-args-fix-x

(defthm te-args->symbol-index$inline-of-te-args-fix-x
  (equal (te-args->symbol-index$inline (te-args-fix x))
         (te-args->symbol-index$inline x)))

Theorem: te-args->symbol-index$inline-te-args-equiv-congruence-on-x

(defthm te-args->symbol-index$inline-te-args-equiv-congruence-on-x
  (implies (te-args-equiv x x-equiv)
           (equal (te-args->symbol-index$inline x)
                  (te-args->symbol-index$inline x-equiv)))
  :rule-classes :congruence)

Function: te-args->symbol-list$inline

(defun te-args->symbol-list$inline (x)
  (declare (xargs :guard (te-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'te-args->symbol-list))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (str::string-list-fix (cdr (std::da-nth 4 x))))
         :exec (cdr (std::da-nth 4 x)))))

Theorem: string-listp-of-te-args->symbol-list

(defthm string-listp-of-te-args->symbol-list
  (b* ((symbol-list (te-args->symbol-list$inline x)))
    (string-listp symbol-list))
  :rule-classes :rewrite)

Theorem: te-args->symbol-list$inline-of-te-args-fix-x

(defthm te-args->symbol-list$inline-of-te-args-fix-x
  (equal (te-args->symbol-list$inline (te-args-fix x))
         (te-args->symbol-list$inline x)))

Theorem: te-args->symbol-list$inline-te-args-equiv-congruence-on-x

(defthm te-args->symbol-list$inline-te-args-equiv-congruence-on-x
  (implies (te-args-equiv x x-equiv)
           (equal (te-args->symbol-list$inline x)
                  (te-args->symbol-list$inline x-equiv)))
  :rule-classes :congruence)

Function: te-args->avoid-list$inline

(defun te-args->avoid-list$inline (x)
  (declare (xargs :guard (te-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'te-args->avoid-list))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (symbol-list-fix (cdr (std::da-nth 5 x))))
         :exec (cdr (std::da-nth 5 x)))))

Theorem: symbol-listp-of-te-args->avoid-list

(defthm symbol-listp-of-te-args->avoid-list
  (b* ((avoid-list (te-args->avoid-list$inline x)))
    (symbol-listp avoid-list))
  :rule-classes :rewrite)

Theorem: te-args->avoid-list$inline-of-te-args-fix-x

(defthm te-args->avoid-list$inline-of-te-args-fix-x
  (equal (te-args->avoid-list$inline (te-args-fix x))
         (te-args->avoid-list$inline x)))

Theorem: te-args->avoid-list$inline-te-args-equiv-congruence-on-x

(defthm te-args->avoid-list$inline-te-args-equiv-congruence-on-x
  (implies (te-args-equiv x x-equiv)
           (equal (te-args->avoid-list$inline x)
                  (te-args->avoid-list$inline x-equiv)))
  :rule-classes :congruence)

Function: te-args->symbol-map$inline

(defun te-args->symbol-map$inline (x)
  (declare (xargs :guard (te-args-p x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'te-args->symbol-map))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x)))
           (symbol-string-alist-fix (cdr (std::da-nth 6 x))))
         :exec (cdr (std::da-nth 6 x)))))

Theorem: symbol-string-alistp-of-te-args->symbol-map

(defthm symbol-string-alistp-of-te-args->symbol-map
  (b* ((symbol-map (te-args->symbol-map$inline x)))
    (symbol-string-alistp symbol-map))
  :rule-classes :rewrite)

Theorem: te-args->symbol-map$inline-of-te-args-fix-x

(defthm te-args->symbol-map$inline-of-te-args-fix-x
  (equal (te-args->symbol-map$inline (te-args-fix x))
         (te-args->symbol-map$inline x)))

Theorem: te-args->symbol-map$inline-te-args-equiv-congruence-on-x

(defthm te-args->symbol-map$inline-te-args-equiv-congruence-on-x
  (implies (te-args-equiv x x-equiv)
           (equal (te-args->symbol-map$inline x)
                  (te-args->symbol-map$inline x-equiv)))
  :rule-classes :congruence)

Function: te-args

(defun te-args (expr-lst fn-lst fty-info symbol-index
                         symbol-list avoid-list symbol-map)
 (declare (xargs :guard (and (pseudo-term-listp expr-lst)
                             (func-alistp fn-lst)
                             (fty-info-alist-p fty-info)
                             (natp symbol-index)
                             (string-listp symbol-list)
                             (symbol-listp avoid-list)
                             (symbol-string-alistp symbol-map))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'te-args))
   (declare (ignorable acl2::__function__))
   (b* ((expr-lst (mbe :logic (pseudo-term-list-fix expr-lst)
                       :exec expr-lst))
        (fn-lst (mbe :logic (func-alist-fix fn-lst)
                     :exec fn-lst))
        (fty-info (mbe :logic (fty-info-alist-fix fty-info)
                       :exec fty-info))
        (symbol-index (mbe :logic (nfix symbol-index)
                           :exec symbol-index))
        (symbol-list (mbe :logic (str::string-list-fix symbol-list)
                          :exec symbol-list))
        (avoid-list (mbe :logic (symbol-list-fix avoid-list)
                         :exec avoid-list))
        (symbol-map (mbe :logic (symbol-string-alist-fix symbol-map)
                         :exec symbol-map)))
     (list (cons 'expr-lst expr-lst)
           (cons 'fn-lst fn-lst)
           (cons 'fty-info fty-info)
           (cons 'symbol-index symbol-index)
           (cons 'symbol-list symbol-list)
           (cons 'avoid-list avoid-list)
           (cons 'symbol-map symbol-map)))))

Theorem: te-args-p-of-te-args

(defthm te-args-p-of-te-args
  (b* ((x (te-args expr-lst fn-lst fty-info symbol-index
                   symbol-list avoid-list symbol-map)))
    (te-args-p x))
  :rule-classes :rewrite)

Theorem: te-args->expr-lst-of-te-args

(defthm te-args->expr-lst-of-te-args
 (equal
   (te-args->expr-lst (te-args expr-lst fn-lst fty-info symbol-index
                               symbol-list avoid-list symbol-map))
   (pseudo-term-list-fix expr-lst)))

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

(defthm te-args->fn-lst-of-te-args
 (equal
     (te-args->fn-lst (te-args expr-lst fn-lst fty-info symbol-index
                               symbol-list avoid-list symbol-map))
     (func-alist-fix fn-lst)))

Theorem: te-args->fty-info-of-te-args

(defthm te-args->fty-info-of-te-args
 (equal
   (te-args->fty-info (te-args expr-lst fn-lst fty-info symbol-index
                               symbol-list avoid-list symbol-map))
   (fty-info-alist-fix fty-info)))

Theorem: te-args->symbol-index-of-te-args

(defthm te-args->symbol-index-of-te-args
  (equal (te-args->symbol-index
              (te-args expr-lst fn-lst fty-info symbol-index
                       symbol-list avoid-list symbol-map))
         (nfix symbol-index)))

Theorem: te-args->symbol-list-of-te-args

(defthm te-args->symbol-list-of-te-args
  (equal (te-args->symbol-list
              (te-args expr-lst fn-lst fty-info symbol-index
                       symbol-list avoid-list symbol-map))
         (str::string-list-fix symbol-list)))

Theorem: te-args->avoid-list-of-te-args

(defthm te-args->avoid-list-of-te-args
  (equal (te-args->avoid-list
              (te-args expr-lst fn-lst fty-info symbol-index
                       symbol-list avoid-list symbol-map))
         (symbol-list-fix avoid-list)))

Theorem: te-args->symbol-map-of-te-args

(defthm te-args->symbol-map-of-te-args
  (equal (te-args->symbol-map
              (te-args expr-lst fn-lst fty-info symbol-index
                       symbol-list avoid-list symbol-map))
         (symbol-string-alist-fix symbol-map)))

Theorem: te-args-of-fields

(defthm te-args-of-fields
  (equal (te-args (te-args->expr-lst x)
                  (te-args->fn-lst x)
                  (te-args->fty-info x)
                  (te-args->symbol-index x)
                  (te-args->symbol-list x)
                  (te-args->avoid-list x)
                  (te-args->symbol-map x))
         (te-args-fix x)))

Theorem: te-args-fix-when-te-args

(defthm te-args-fix-when-te-args
  (equal (te-args-fix x)
         (te-args (te-args->expr-lst x)
                  (te-args->fn-lst x)
                  (te-args->fty-info x)
                  (te-args->symbol-index x)
                  (te-args->symbol-list x)
                  (te-args->avoid-list x)
                  (te-args->symbol-map x))))

Theorem: equal-of-te-args

(defthm equal-of-te-args
  (equal (equal (te-args expr-lst fn-lst fty-info symbol-index
                         symbol-list avoid-list symbol-map)
                x)
         (and (te-args-p x)
              (equal (te-args->expr-lst x)
                     (pseudo-term-list-fix expr-lst))
              (equal (te-args->fn-lst x)
                     (func-alist-fix fn-lst))
              (equal (te-args->fty-info x)
                     (fty-info-alist-fix fty-info))
              (equal (te-args->symbol-index x)
                     (nfix symbol-index))
              (equal (te-args->symbol-list x)
                     (str::string-list-fix symbol-list))
              (equal (te-args->avoid-list x)
                     (symbol-list-fix avoid-list))
              (equal (te-args->symbol-map x)
                     (symbol-string-alist-fix symbol-map)))))

Theorem: te-args-of-pseudo-term-list-fix-expr-lst

(defthm te-args-of-pseudo-term-list-fix-expr-lst
  (equal (te-args (pseudo-term-list-fix expr-lst)
                  fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)
         (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)))

Theorem: te-args-pseudo-term-list-equiv-congruence-on-expr-lst

(defthm te-args-pseudo-term-list-equiv-congruence-on-expr-lst
  (implies (pseudo-term-list-equiv expr-lst expr-lst-equiv)
           (equal (te-args expr-lst fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)
                  (te-args expr-lst-equiv
                           fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)))
  :rule-classes :congruence)

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

(defthm te-args-of-func-alist-fix-fn-lst
  (equal (te-args expr-lst (func-alist-fix fn-lst)
                  fty-info symbol-index
                  symbol-list avoid-list symbol-map)
         (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)))

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

(defthm te-args-func-alist-equiv-congruence-on-fn-lst
  (implies (func-alist-equiv fn-lst fn-lst-equiv)
           (equal (te-args expr-lst fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)
                  (te-args expr-lst
                           fn-lst-equiv fty-info symbol-index
                           symbol-list avoid-list symbol-map)))
  :rule-classes :congruence)

Theorem: te-args-of-fty-info-alist-fix-fty-info

(defthm te-args-of-fty-info-alist-fix-fty-info
  (equal (te-args expr-lst
                  fn-lst (fty-info-alist-fix fty-info)
                  symbol-index
                  symbol-list avoid-list symbol-map)
         (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)))

Theorem: te-args-fty-info-alist-equiv-congruence-on-fty-info

(defthm te-args-fty-info-alist-equiv-congruence-on-fty-info
  (implies (fty-info-alist-equiv fty-info fty-info-equiv)
           (equal (te-args expr-lst fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)
                  (te-args expr-lst
                           fn-lst fty-info-equiv symbol-index
                           symbol-list avoid-list symbol-map)))
  :rule-classes :congruence)

Theorem: te-args-of-nfix-symbol-index

(defthm te-args-of-nfix-symbol-index
  (equal (te-args expr-lst
                  fn-lst fty-info (nfix symbol-index)
                  symbol-list avoid-list symbol-map)
         (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)))

Theorem: te-args-nat-equiv-congruence-on-symbol-index

(defthm te-args-nat-equiv-congruence-on-symbol-index
  (implies (acl2::nat-equiv symbol-index symbol-index-equiv)
           (equal (te-args expr-lst fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)
                  (te-args expr-lst
                           fn-lst fty-info symbol-index-equiv
                           symbol-list avoid-list symbol-map)))
  :rule-classes :congruence)

Theorem: te-args-of-string-list-fix-symbol-list

(defthm te-args-of-string-list-fix-symbol-list
  (equal (te-args expr-lst fn-lst fty-info symbol-index
                  (str::string-list-fix symbol-list)
                  avoid-list symbol-map)
         (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)))

Theorem: te-args-string-list-equiv-congruence-on-symbol-list

(defthm te-args-string-list-equiv-congruence-on-symbol-list
  (implies (str::string-list-equiv symbol-list symbol-list-equiv)
           (equal (te-args expr-lst fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)
                  (te-args expr-lst fn-lst
                           fty-info symbol-index symbol-list-equiv
                           avoid-list symbol-map)))
  :rule-classes :congruence)

Theorem: te-args-of-symbol-list-fix-avoid-list

(defthm te-args-of-symbol-list-fix-avoid-list
  (equal (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list (symbol-list-fix avoid-list)
                  symbol-map)
         (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)))

Theorem: te-args-symbol-list-equiv-congruence-on-avoid-list

(defthm te-args-symbol-list-equiv-congruence-on-avoid-list
  (implies (acl2::symbol-list-equiv avoid-list avoid-list-equiv)
           (equal (te-args expr-lst fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)
                  (te-args expr-lst
                           fn-lst fty-info symbol-index symbol-list
                           avoid-list-equiv symbol-map)))
  :rule-classes :congruence)

Theorem: te-args-of-symbol-string-alist-fix-symbol-map

(defthm te-args-of-symbol-string-alist-fix-symbol-map
  (equal (te-args expr-lst fn-lst fty-info
                  symbol-index symbol-list avoid-list
                  (symbol-string-alist-fix symbol-map))
         (te-args expr-lst fn-lst fty-info symbol-index
                  symbol-list avoid-list symbol-map)))

Theorem: te-args-symbol-string-alist-equiv-congruence-on-symbol-map

(defthm te-args-symbol-string-alist-equiv-congruence-on-symbol-map
  (implies (symbol-string-alist-equiv symbol-map symbol-map-equiv)
           (equal (te-args expr-lst fn-lst fty-info symbol-index
                           symbol-list avoid-list symbol-map)
                  (te-args expr-lst
                           fn-lst fty-info symbol-index symbol-list
                           avoid-list symbol-map-equiv)))
  :rule-classes :congruence)

Theorem: te-args-fix-redef

(defthm te-args-fix-redef
  (equal (te-args-fix x)
         (te-args (te-args->expr-lst x)
                  (te-args->fn-lst x)
                  (te-args->fty-info x)
                  (te-args->symbol-index x)
                  (te-args->symbol-list x)
                  (te-args->avoid-list x)
                  (te-args->symbol-map x)))
  :rule-classes :definition)

Function: map-translated-actuals

(defun map-translated-actuals (actuals)
  (declare (xargs :guard (paragraphp actuals)))
  (let ((acl2::__function__ 'map-translated-actuals))
    (declare (ignorable acl2::__function__))
    (b* ((actuals (paragraph-fix actuals))
         ((unless (consp actuals)) actuals)
         ((unless (consp (cdr actuals))) actuals)
         ((cons first rest) actuals)
         (mapped-rest (map-translated-actuals rest)))
      (cons first (cons #\, mapped-rest)))))

Theorem: paragraphp-of-map-translated-actuals

(defthm paragraphp-of-map-translated-actuals
  (b* ((mapped (map-translated-actuals actuals)))
    (paragraphp mapped))
  :rule-classes :rewrite)

Function: translate-fty-special

(defun translate-fty-special (fn-call fn-actuals fty-info)
 (declare (xargs :guard (and (symbolp fn-call)
                             (pseudo-term-listp fn-actuals)
                             (fty-info-alist-p fty-info))))
 (let ((acl2::__function__ 'translate-fty-special))
  (declare (ignorable acl2::__function__))
  (b*
   ((fn-call (symbol-fix fn-call))
    (fn-actuals (pseudo-term-list-fix fn-actuals))
    (fty-info (fty-info-alist-fix fty-info))
    ((if (and (and (car fn-actuals)
                   (null (cdr fn-actuals)))
              (consp (car fn-actuals))
              (equal (caar fn-actuals) 'magic-fix)
              (consp (cadar fn-actuals))
              (equal (car (cadar fn-actuals)) 'quote)
              (symbolp (cadr (cadar fn-actuals)))))
     (if
      (equal fn-call 'consp)
      (mv
       (list
          (downcase-string
               (concatenate
                    'string
                    (lisp-to-python-names (cadr (cadar fn-actuals)))
                    "_" (translate-symbol fn-call))))
       ''t)
      (mv
       (list
          (downcase-string
               (concatenate
                    'string
                    (lisp-to-python-names (cadr (cadar fn-actuals)))
                    "." (translate-symbol fn-call))))
       (car fn-actuals))))
    (fixed
     (cond
      ((or (equal fn-call 'car)
           (equal fn-call 'cdr)
           (equal fn-call 'consp))
       (b*
        (((unless (and (car fn-actuals)
                       (null (cdr fn-actuals))))
          (er hard?
              'smt-translator=>translate-fty-special
              "Wrong ~
         number of arguments for ~p0: ~p1~%"
              fn-call fn-actuals)))
        (car fn-actuals)))
      ((or (equal fn-call 'cons)
           (equal fn-call 'assoc-equal))
       (b*
        (((unless (and (cadr fn-actuals)
                       (null (cddr fn-actuals))))
          (er hard?
              'smt-translator=>translate-fty-special
              "Wrong ~
         number of arguments for ~p0: ~p1~%"
              fn-call fn-actuals)))
        (cadr fn-actuals)))
      ((equal fn-call 'acons)
       (b*
        (((unless (and (caddr fn-actuals)
                       (null (cdddr fn-actuals))))
          (er hard?
              'smt-translator=>translate-fty-special
              "Wrong ~
         number of arguments for ~p0: ~p1~%"
              fn-call fn-actuals)))
        (caddr fn-actuals)))
      (t (er hard?
             'smt-translator=>translate-fty-special
             "Impossible path:
                                 ~q0"
             fn-call))))
    ((unless (and (consp fixed)
                  (car fixed)
                  (cadr fixed)
                  (symbolp (car fixed))))
     (prog2$ (er hard?
                 'smt-translator=>translate-fty-special
                 "Not fixed1:
                                 ~q0"
                 fixed)
             (mv nil ''t)))
    ((mv fixing? &)
     (fixing-of-flextype (car fixed)
                         fty-info))
    ((unless fixing?)
     (prog2$ (er hard?
                 'smt-translator=>translate-fty-special
                 "Not fixed2:
                                 ~q0"
                 (car fixed))
             (mv nil ''t)))
    ((unless (pseudo-termp (cadr fixed)))
     (prog2$
        (er hard?
            'smt-translator=>translate-fty-special
            "not ~
                               pseudo-termp: ~q0"
            (cadr fixed))
        (mv nil ''t)))
    (smt-precond (if (equal fn-call 'car)
                     (cons 'consp (cons (cadr fixed) 'nil))
                   ''t)))
   (if (or (equal fn-call 'acons)
           (equal fn-call 'assoc-equal)
           (equal fn-call 'consp))
       (mv (list (downcase-string
                      (concatenate 'string
                                   (translate-symbol fixing?)
                                   "_" (translate-symbol fn-call))))
           ''t)
     (mv (list (downcase-string
                    (concatenate 'string
                                 (translate-symbol fixing?)
                                 "." (translate-symbol fn-call))))
         smt-precond)))))

Theorem: paragraphp-of-translate-fty-special.translated

(defthm paragraphp-of-translate-fty-special.translated
  (b* (((mv ?translated ?smt-precond)
        (translate-fty-special fn-call fn-actuals fty-info)))
    (paragraphp translated))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-translate-fty-special.smt-precond

(defthm pseudo-termp-of-translate-fty-special.smt-precond
  (b* (((mv ?translated ?smt-precond)
        (translate-fty-special fn-call fn-actuals fty-info)))
    (pseudo-termp smt-precond))
  :rule-classes :rewrite)

Function: translate-field-accessor

(defun translate-field-accessor (fty-name fn-call)
 (declare (xargs :guard (and (symbolp fty-name)
                             (symbolp fn-call))))
 (let ((acl2::__function__ 'translate-field-accessor))
  (declare (ignorable acl2::__function__))
  (b* ((fty-name (symbol-fix fty-name))
       (fn-call (symbol-fix fn-call))
       (fty-name-str (symbol-name fty-name))
       (fn-call-str (symbol-name fn-call))
       ((unless (<= (+ 2 (length fty-name-str))
                    (length fn-call-str)))
        (mv (er hard?
                'smt-translator=>translate-field-accessor
                "Something is ~
             wrong1: ~p0 and ~p1"
                fty-name-str fn-call-str)
            ''t))
       (pos-prefix (search fty-name-str fn-call-str
                           :test 'equal))
       ((unless (equal pos-prefix 0))
        (mv (er hard?
                'smt-translator=>translate-field-accessor
                "Something is ~
             wrong2: ~p0 and ~p1"
                fty-name-str fn-call-str)
            ''t))
       (pos1 (length fty-name-str))
       (pos-infix (search "->" fn-call-str :test 'equal))
       ((unless (equal pos1 pos-infix))
        (mv (er hard?
                'smt-translator=>translate-field-accessor
                "Something is ~
             wrong3: ~p0 and ~p1"
                fty-name-str fn-call-str)
            ''t))
       (pos-suffix (+ 2 pos1))
       (pos2 (search "$INLINE" fn-call-str
                     :from-end t
                     :test 'equal))
       ((unless (and (natp pos2)
                     (<= pos-suffix pos2)
                     (<= pos2 (length fn-call-str))))
        (mv (er hard?
                'smt-translator=>translate-field-accessor
                "Something is ~
             wrong4: ~p0 and ~p1"
                fty-name-str fn-call-str)
            ''t))
       (suffix (subseq fn-call-str pos-suffix pos2))
       ((unless (stringp suffix))
        (mv (er hard?
                'smt-translator=>translate-field-accessor
                "Something is ~
             wrong5: ~p0 and ~p1"
                fty-name-str fn-call-str)
            ''t)))
    (mv (list (downcase-string
                   (concatenate 'string
                                (lisp-to-python-names fty-name-str)
                                "." (lisp-to-python-names suffix))))
        ''t))))

Theorem: paragraphp-of-translate-field-accessor.translated

(defthm paragraphp-of-translate-field-accessor.translated
  (b* (((mv ?translated ?smt-precond)
        (translate-field-accessor fty-name fn-call)))
    (paragraphp translated))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-translate-field-accessor.smt-precond

(defthm pseudo-termp-of-translate-field-accessor.smt-precond
  (b* (((mv ?translated ?smt-precond)
        (translate-field-accessor fty-name fn-call)))
    (pseudo-termp smt-precond))
  :rule-classes :rewrite)

Function: translate-fty

(defun translate-fty (fn-call fn-actuals fty-info)
 (declare (xargs :guard (and (symbolp fn-call)
                             (pseudo-term-listp fn-actuals)
                             (fty-info-alist-p fty-info))))
 (declare (xargs :guard (or (fncall-of-flextype-special fn-call)
                            (assoc-equal fn-call fty-info))))
 (let ((acl2::__function__ 'translate-fty))
  (declare (ignorable acl2::__function__))
  (b*
   ((fn-call (symbol-fix fn-call))
    (special? (fncall-of-flextype-special fn-call))
    ((if special?)
     (translate-fty-special fn-call fn-actuals fty-info))
    (item (assoc-equal fn-call fty-info))
    (fty-name (fty-info->name (cdr item)))
    (fty-type (fty-info->type (cdr item)))
    (option? (fncall-of-flextype-option fn-call fty-info))
    ((if (and option? (equal fty-type :constructor)))
     (mv (list (concatenate 'string
                            (translate-symbol fty-name)
                            ".some"))
         ''t))
    ((if (and option? (equal fty-type :field)))
     (mv (list (concatenate 'string
                            (translate-symbol fty-name)
                            ".val"))
         ''t))
    ((unless (or (equal fty-type :field)
                 (equal fty-type :constructor)))
     (mv
      (er
       hard? 'smt-translator=>translate-fty
       "Unexpected fty function ~
                         found: ~p0 of ~p1~%"
       fn-call fty-type)
      ''t))
    ((if (equal fty-type :constructor))
     (mv (list (concatenate 'string
                            (translate-symbol fty-name)
                            "." (translate-symbol fn-call)))
         ''t)))
   (translate-field-accessor fty-name fn-call))))

Theorem: paragraphp-of-translate-fty.translated

(defthm paragraphp-of-translate-fty.translated
  (b* (((mv ?translated ?smt-precond)
        (translate-fty fn-call fn-actuals fty-info)))
    (paragraphp translated))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-translate-fty.smt-precond

(defthm pseudo-termp-of-translate-fty.smt-precond
  (b* (((mv ?translated ?smt-precond)
        (translate-fty fn-call fn-actuals fty-info)))
    (pseudo-termp smt-precond))
  :rule-classes :rewrite)

Function: generate-symbol-enumeration

(defun generate-symbol-enumeration (symbol-index)
  (declare (xargs :guard (natp symbol-index)))
  (let ((acl2::__function__ 'generate-symbol-enumeration))
    (declare (ignorable acl2::__function__))
    (b* ((symbol-index (nfix symbol-index))
         (new-sym (concatenate 'string
                               "gensym_"
                               (nat-to-dec-string symbol-index))))
      new-sym)))

Theorem: stringp-of-generate-symbol-enumeration

(defthm stringp-of-generate-symbol-enumeration
  (b* ((new-sym (generate-symbol-enumeration symbol-index)))
    (stringp new-sym))
  :rule-classes :rewrite)

Function: translate-quote

(defun translate-quote (expr)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'translate-quote))
    (declare (ignorable acl2::__function__))
    (b* (((unless (or (symbolp expr)
                      (smt-numberp expr)
                      (booleanp expr)))
          (er hard? 'smt-translator=>translate-quote
              "Atom not ~
                       supported: ~q0"
              expr)))
      (cond ((booleanp expr)
             (translate-bool expr nil))
            ((smt-numberp expr)
             (translate-number expr))
            (t (translate-symbol expr))))))

Theorem: paragraphp-of-translate-quote

(defthm paragraphp-of-translate-quote
  (b* ((translated-quote (translate-quote expr)))
    (paragraphp translated-quote))
  :rule-classes :rewrite)

Theorem: stringp-of-translated-quote-when-symbolp

(defthm stringp-of-translated-quote-when-symbolp
  (b* ((translated-quote (translate-quote expr)))
    (implies (and (symbolp expr)
                  (not (booleanp expr)))
             (stringp translated-quote)))
  :rule-classes :rewrite)

Function: translate-expression

(defun translate-expression (args)
 (declare (xargs :guard (te-args-p args)))
 (let ((acl2::__function__ 'translate-expression))
  (declare (ignorable acl2::__function__))
  (b*
   ((args (te-args-fix args))
    ((te-args a) args)
    ((unless (consp a.expr-lst))
     (mv nil ''t
         a.symbol-list
         a.symbol-index a.symbol-map))
    ((cons expr rest) a.expr-lst)
    ((mv translated-rest
         smt-precond-rest symbols-rest
         symbol-index-rest symbol-map-rest)
     (translate-expression (change-te-args a :expr-lst rest)))
    ((if (symbolp expr))
     (mv (cons (translate-symbol expr)
               translated-rest)
         smt-precond-rest symbols-rest
         symbol-index-rest symbol-map-rest))
    ((if (equal (car expr) 'quote))
     (b*
      ((the-sym (cadr expr))
       ((unless (and (symbolp the-sym)
                     (not (booleanp the-sym))))
        (mv (cons (translate-quote the-sym)
                  translated-rest)
            smt-precond-rest symbols-rest
            symbol-index-rest symbol-map-rest))
       ((unless (mbt (symbol-string-alistp symbol-map-rest)))
        (mv (er hard?
                'smt-translator=>translate-expression
                "Can't reach ~
                      this branch~%")
            nil nil 0 nil))
       (exist-map? (cdr (assoc-equal the-sym symbol-map-rest)))
       ((if exist-map?)
        (mv (cons exist-map? translated-rest)
            smt-precond-rest
            (cons exist-map? symbols-rest)
            symbol-index-rest symbol-map-rest))
       (exist-sym? (member-equal the-sym a.avoid-list))
       (gen-sym
         (if exist-sym? (generate-symbol-enumeration a.symbol-index)
           (translate-symbol the-sym))))
      (mv (cons gen-sym translated-rest)
          smt-precond-rest
          (cons gen-sym symbols-rest)
          (if exist-sym? (1+ symbol-index-rest)
            symbol-index-rest)
          (if exist-map? symbol-map-rest
            (acons the-sym gen-sym symbol-map-rest)))))
    ((cons fn-call fn-actuals) expr)
    ((if (pseudo-lambdap fn-call))
     (b*
      ((formals (lambda-formals fn-call))
       ((unless (and (symbol-listp formals)
                     (equal (len formals) (len fn-actuals))
                     (pseudo-term-listp fn-actuals)))
        (mv (er hard?
                'smt-translator=>translate-expression
                "bad lambda: ~q0" fn-call)
            nil nil 0 nil))
       (body (lambda-body fn-call))
       (lambda-sym (car fn-call))
       ((mv translated-lambda &)
        (translate-function lambda-sym))
       (translated-formals (translate-symbol-lst formals))
       ((mv translated-body
            smt-precond-1 symbol-list-1
            symbol-index-1 symbol-map-1)
        (translate-expression
             (change-te-args a
                             :expr-lst (list body)
                             :symbol-list symbols-rest
                             :symbol-index symbol-index-rest
                             :symbol-map symbol-map-rest)))
       ((mv translated-actuals
            smt-precond-2 symbol-list-2
            symbol-index-2 symbol-map-2)
        (translate-expression
             (change-te-args a
                             :expr-lst fn-actuals
                             :symbol-list symbol-list-1
                             :symbol-index symbol-index-1
                             :symbol-map symbol-map-1)))
       (translated-lambda-whole
        (cons
         '#\(
         (cons
          translated-lambda
          (cons
           '#\Space
           (cons
            translated-formals
            (cons
             '#\:
             (cons
              translated-body
              (cons
               '#\)
               (cons
                   '#\(
                   (cons (map-translated-actuals translated-actuals)
                         '(#\)))))))))))))
      (mv
       (cons translated-lambda-whole translated-rest)
       (cons
        'if
        (cons
         (cons
          'if
          (cons
               (cons (cons 'lambda
                           (cons formals (cons smt-precond-1 'nil)))
                     fn-actuals)
               (cons smt-precond-2 '('nil))))
         (cons smt-precond-rest '('nil))))
       symbol-list-2
       symbol-index-2 symbol-map-2)))
    ((if (equal fn-call 'magic-fix))
     (b*
      (((unless (and (consp fn-actuals)
                     (consp (cdr fn-actuals))
                     (null (cddr fn-actuals))))
        (mv
         (er
          hard?
          'smt-translator=>translate-expression
          "Wrong ~
         number of arguments for magic-fix function: ~q0"
          expr)
         nil nil 0 nil))
       (the-type (car fn-actuals))
       (the-nil (cadr fn-actuals))
       ((if (and (consp the-nil)
                 (equal (car the-nil) 'quote)
                 (consp (cdr the-nil))
                 (equal (cadr the-nil) nil)
                 (consp the-type)
                 (equal (car the-type) 'quote)
                 (consp (cdr the-type))
                 (symbolp (cadr the-type))))
        (mv (cons (translate-bool nil (cadr the-type))
                  translated-rest)
            smt-precond-rest symbols-rest
            symbol-index-rest symbol-map-rest))
       ((mv translated-actuals
            smt-precond-1 symbol-list-1
            symbol-index-1 symbol-map-1)
        (translate-expression
             (change-te-args a
                             :expr-lst (cdr fn-actuals)
                             :symbol-list symbols-rest
                             :symbol-index symbol-index-rest
                             :symbol-map symbol-map-rest))))
      (mv (cons translated-actuals translated-rest)
          (cons 'if
                (cons smt-precond-1
                      (cons smt-precond-rest '('nil))))
          symbol-list-1
          symbol-index-1 symbol-map-1)))
    ((mv fixing? guards)
     (fixing-of-flextype fn-call a.fty-info))
    ((if fixing?)
     (b*
      (((unless (and (consp fn-actuals)
                     (car fn-actuals)
                     (null (cdr fn-actuals))))
        (mv
         (er
          hard?
          'smt-translator=>translate-expression
          "Wrong ~
         number of arguments for a fixing function: ~q0"
          expr)
         nil nil 0 nil))
       (fixed (car fn-actuals))
       ((unless (and (consp guards)
                     (car guards)
                     (null (cdr guards))
                     (not (equal (car guards) 'quote))))
        (mv (er hard?
                'smt-translator=>translate-expression
                "bad guards :
       ~q0" guards)
            nil nil 0 nil))
       ((if (and (consp fixed)
                 (equal (car fixed) 'quote)
                 (consp (cdr fixed))
                 (equal (cadr fixed) nil)))
        (mv (cons (translate-bool nil fixing?)
                  translated-rest)
            (cons 'if
                  (cons (cons (car guards) (cons fixed 'nil))
                        (cons smt-precond-rest '('nil))))
            symbols-rest
            symbol-index-rest symbol-map-rest))
       ((mv translated-actuals
            smt-precond-1 symbol-list-1
            symbol-index-1 symbol-map-1)
        (translate-expression
             (change-te-args a
                             :expr-lst fn-actuals
                             :symbol-list symbols-rest
                             :symbol-index symbol-index-rest
                             :symbol-map symbol-map-rest))))
      (mv
       (cons translated-actuals translated-rest)
       (cons 'if
             (cons (cons 'if
                         (cons (cons (car guards) (cons fixed 'nil))
                               (cons smt-precond-1 '('nil))))
                   (cons smt-precond-rest '('nil))))
       symbol-list-1
       symbol-index-1 symbol-map-1)))
    (fty? (fncall-of-flextype fn-call a.fty-info))
    ((if fty?)
     (b*
      (((mv translated-fn-call fty-smt-precond)
        (translate-fty fn-call fn-actuals a.fty-info))
       ((mv translated-actuals
            smt-precond-1 symbol-list-1
            symbol-index-1 symbol-map-1)
        (translate-expression
             (change-te-args a
                             :expr-lst fn-actuals
                             :symbol-list symbols-rest
                             :symbol-index symbol-index-rest
                             :symbol-map symbol-map-rest)))
       (translated-expr
        (cons
             translated-fn-call
             (cons '#\(
                   (cons (map-translated-actuals translated-actuals)
                         '(#\)))))))
      (mv (cons translated-expr translated-rest)
          (cons 'if
                (cons (cons 'if
                            (cons fty-smt-precond
                                  (cons smt-precond-1 '('nil))))
                      (cons smt-precond-rest '('nil))))
          symbol-list-1
          symbol-index-1 symbol-map-1)))
    ((unless (mbt (symbolp fn-call)))
     (mv nil ''t nil 0 nil))
    (fn (hons-get fn-call a.fn-lst))
    ((if fn)
     (b*
      (((mv translated-actuals
            smt-precond-1 symbol-list-1
            symbol-index-1 symbol-map-1)
        (translate-expression
             (change-te-args a
                             :expr-lst fn-actuals
                             :symbol-list symbols-rest
                             :symbol-index symbol-index-rest
                             :symbol-map symbol-map-rest)))
       (translated-fn-call
        (cons
             (translate-symbol fn-call)
             (cons '#\(
                   (cons (map-translated-actuals translated-actuals)
                         '(#\)))))))
      (mv (cons translated-fn-call translated-rest)
          (cons 'if
                (cons smt-precond-1
                      (cons smt-precond-rest '('nil))))
          symbol-list-1
          symbol-index-1 symbol-map-1)))
    ((mv fn nargs)
     (translate-function fn-call))
    ((if (zp nargs))
     (mv (cons (cons fn '(#\( #\)))
               translated-rest)
         smt-precond-rest symbols-rest
         symbol-index-rest symbol-map-rest))
    ((if (equal fn-call 'if))
     (b*
      (((unless (and (consp fn-actuals)
                     (car fn-actuals)
                     (consp (cdr fn-actuals))
                     (cadr fn-actuals)
                     (consp (cddr fn-actuals))
                     (caddr fn-actuals)
                     (null (cdddr fn-actuals))))
        (mv
         (er hard?
             'smt-translator=>translate-expression
             "fn-actuals ~
       for if should be of length 3: ~q0"
             fn-actuals)
         nil nil 0 nil))
       ((mv translated-car-actual
            smt-precond-if symbol-list-1
            symbol-index-1 symbol-map-1)
        (translate-expression
             (change-te-args a
                             :expr-lst (list (car fn-actuals))
                             :symbol-list symbols-rest
                             :symbol-index symbol-index-rest
                             :symbol-map symbol-map-rest)))
       ((mv translated-cadr-actual
            smt-precond-then symbol-list-2
            symbol-index-2 symbol-map-2)
        (translate-expression
             (change-te-args a
                             :expr-lst (list (cadr fn-actuals))
                             :symbol-list symbol-list-1
                             :symbol-index symbol-index-1
                             :symbol-map symbol-map-1)))
       ((mv translated-caddr-actual
            smt-precond-else symbol-list-3
            symbol-index-3 symbol-map-3)
        (translate-expression
             (change-te-args a
                             :expr-lst (list (caddr fn-actuals))
                             :symbol-list symbol-list-2
                             :symbol-index symbol-index-2
                             :symbol-map symbol-map-2)))
       (translated-actuals
            (cons translated-car-actual
                  (cons translated-cadr-actual
                        (cons translated-caddr-actual 'nil))))
       ((unless (and (pseudo-termp (car fn-actuals))
                     (pseudo-termp (cadr fn-actuals))
                     (pseudo-termp (caddr fn-actuals))))
        (mv (er hard?
                'smt-translator=>translate-expression
                "pseudo-termp
       ensured: ~q0"
                fn-actuals)
            nil nil 0 nil))
       (smt-precond
        (cons
         'if
         (cons
             smt-precond-if
             (cons (cons 'if
                         (cons (car fn-actuals)
                               (cons smt-precond-then
                                     (cons smt-precond-else 'nil))))
                   '('nil))))))
      (mv
       (cons
        (cons
             fn
             (cons '#\(
                   (cons (map-translated-actuals translated-actuals)
                         '(#\)))))
        translated-rest)
       (cons 'if
             (cons smt-precond
                   (cons smt-precond-rest '('nil))))
       symbol-list-3
       symbol-index-3 symbol-map-3)))
    ((mv translated-actuals
         smt-precond-1 symbol-list-1
         symbol-index-1 symbol-map-1)
     (translate-expression
          (change-te-args a
                          :expr-lst fn-actuals
                          :symbol-list symbols-rest
                          :symbol-index symbol-index-rest
                          :symbol-map symbol-map-rest))))
   (mv
    (cons
       (cons fn
             (cons '#\(
                   (cons (map-translated-actuals translated-actuals)
                         '(#\)))))
       translated-rest)
    (cons 'if
          (cons smt-precond-1
                (cons smt-precond-rest '('nil))))
    symbol-list-1
    symbol-index-1 symbol-map-1))))

Theorem: paragraphp-of-translate-expression.translated

(defthm paragraphp-of-translate-expression.translated
  (b* (((mv ?translated ?smt-precond
            ?symbols ?symbol-index ?symbol-map)
        (translate-expression args)))
    (paragraphp translated))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-translate-expression.smt-precond

(defthm pseudo-termp-of-translate-expression.smt-precond
  (b* (((mv ?translated ?smt-precond
            ?symbols ?symbol-index ?symbol-map)
        (translate-expression args)))
    (pseudo-termp smt-precond))
  :rule-classes :rewrite)

Theorem: string-listp-of-translate-expression.symbols

(defthm string-listp-of-translate-expression.symbols
  (b* (((mv ?translated ?smt-precond
            ?symbols ?symbol-index ?symbol-map)
        (translate-expression args)))
    (string-listp symbols))
  :rule-classes :rewrite)

Theorem: natp-of-translate-expression.symbol-index

(defthm natp-of-translate-expression.symbol-index
  (b* (((mv ?translated ?smt-precond
            ?symbols ?symbol-index ?symbol-map)
        (translate-expression args)))
    (natp symbol-index))
  :rule-classes :rewrite)

Theorem: symbol-string-alistp-of-translate-expression.symbol-map

(defthm symbol-string-alistp-of-translate-expression.symbol-map
  (b* (((mv ?translated ?smt-precond
            ?symbols ?symbol-index ?symbol-map)
        (translate-expression args)))
    (symbol-string-alistp symbol-map))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-cdr-of-te-args->expr-lst

(defthm pseudo-term-listp-of-cdr-of-te-args->expr-lst
  (implies (and (te-args-p x)
                (consp (te-args->expr-lst x)))
           (pseudo-term-listp (cdr (te-args->expr-lst x)))))

Theorem: consp-of-car-of-te-args->expr-lst

(defthm consp-of-car-of-te-args->expr-lst
  (implies (and (te-args-p args)
                (consp (te-args->expr-lst args))
                (not (symbolp (car (te-args->expr-lst args)))))
           (consp (car (te-args->expr-lst args)))))

Theorem: not-cdr-of-car-of-quote-ex-args->expr-lst

(defthm not-cdr-of-car-of-quote-ex-args->expr-lst
  (implies (and (te-args-p args)
                (consp (te-args->expr-lst args))
                (not (symbolp (car (te-args->expr-lst args))))
                (equal (car (car (te-args->expr-lst args)))
                       'quote)
                (not (consp (cdr (car (te-args->expr-lst args))))))
           (not (cdr (car (te-args->expr-lst args))))))

Theorem: symbolp-of-caaar-of-te-args->expr-lst

(defthm symbolp-of-caaar-of-te-args->expr-lst
  (implies
       (and (te-args-p args)
            (consp (te-args->expr-lst args))
            (not (symbolp (car (te-args->expr-lst args))))
            (not (equal (car (car (te-args->expr-lst args)))
                        'quote))
            (pseudo-lambdap (car (car (te-args->expr-lst args)))))
       (symbolp (car (car (car (te-args->expr-lst args)))))))

Theorem: symbolp-of-caar-te-args->expr-lst

(defthm symbolp-of-caar-te-args->expr-lst
 (implies
   (and (te-args-p args)
        (consp (te-args->expr-lst args))
        (not (symbolp (car (te-args->expr-lst args))))
        (not (pseudo-lambdap (car (car (te-args->expr-lst args))))))
   (symbolp (car (car (te-args->expr-lst args))))))

Theorem: symbol-listp-of-cadaar-of-te-args->expr-lst

(defthm symbol-listp-of-cadaar-of-te-args->expr-lst
  (implies
       (and (te-args-p args)
            (consp (te-args->expr-lst args))
            (not (symbolp (car (te-args->expr-lst args))))
            (not (equal (car (car (te-args->expr-lst args)))
                        'quote))
            (pseudo-lambdap (car (car (te-args->expr-lst args)))))
       (symbol-listp (cadr (car (car (te-args->expr-lst args)))))))

Theorem: pseudo-termp-of-caddaar-of-te-args->expr-lst

(defthm pseudo-termp-of-caddaar-of-te-args->expr-lst
  (implies
       (and (te-args-p args)
            (consp (te-args->expr-lst args))
            (not (symbolp (car (te-args->expr-lst args))))
            (not (equal (car (car (te-args->expr-lst args)))
                        'quote))
            (pseudo-lambdap (car (car (te-args->expr-lst args)))))
       (pseudo-termp (caddr (car (car (te-args->expr-lst args)))))))

Theorem: pseudo-term-listp-of-cdar-te-args->expr-lst

(defthm pseudo-term-listp-of-cdar-te-args->expr-lst
  (implies
       (and (te-args-p args)
            (consp (te-args->expr-lst args))
            (not (symbolp (car (te-args->expr-lst args))))
            (not (equal (car (car (te-args->expr-lst args)))
                        'quote))
            (pseudo-lambdap (car (car (te-args->expr-lst args)))))
       (pseudo-term-listp (cdr (car (te-args->expr-lst args))))))

Theorem: pseudo-term-listp-of-cdar-of-te-args->expr-lst

(defthm pseudo-term-listp-of-cdar-of-te-args->expr-lst
 (implies
   (and (te-args-p args)
        (consp (te-args->expr-lst args))
        (not (symbolp (car (te-args->expr-lst args))))
        (not (equal (car (car (te-args->expr-lst args)))
                    'quote))
        (not (pseudo-lambdap (car (car (te-args->expr-lst args))))))
   (pseudo-term-listp (cdr (car (te-args->expr-lst args))))))

Theorem: crock-pseudo-term-listp

(defthm crock-pseudo-term-listp
  (implies
       (pseudo-term-listp (cdr (car (te-args->expr-lst args))))
       (pseudo-term-listp (cddr (car (te-args->expr-lst args))))))

Theorem: pseudo-term-listp-of-cddar-of-te-args->expr-lst

(defthm pseudo-term-listp-of-cddar-of-te-args->expr-lst
 (implies
   (and (te-args-p args)
        (consp (te-args->expr-lst args))
        (not (symbolp (car (te-args->expr-lst args))))
        (not (equal (car (car (te-args->expr-lst args)))
                    'quote))
        (not (pseudo-lambdap (car (car (te-args->expr-lst args))))))
   (pseudo-term-listp (cddr (car (te-args->expr-lst args))))))

Theorem: not-cdaar-te-args->expr-lst

(defthm not-cdaar-te-args->expr-lst
 (implies
      (and (te-args-p args)
           (consp (te-args->expr-lst args))
           (not (symbolp (car (te-args->expr-lst args))))
           (not (equal (car (car (te-args->expr-lst args)))
                       'quote))
           (pseudo-lambdap (car (car (te-args->expr-lst args))))
           (not (consp (cdr (car (car (te-args->expr-lst args)))))))
      (not (cdr (car (car (te-args->expr-lst args)))))))

Theorem: not-cddaar-of-te-args->expr-lst

(defthm not-cddaar-of-te-args->expr-lst
 (implies
     (and (te-args-p args)
          (consp (te-args->expr-lst args))
          (not (symbolp (car (te-args->expr-lst args))))
          (not (equal (car (car (te-args->expr-lst args)))
                      'quote))
          (pseudo-lambdap (car (car (te-args->expr-lst args))))
          (not (consp (cddr (car (car (te-args->expr-lst args)))))))
     (not (cddr (car (car (te-args->expr-lst args)))))))

Theorem: not-caar-of-te-args->expr-lst

(defthm not-caar-of-te-args->expr-lst
 (implies (and (te-args-p args)
               (consp (te-args->expr-lst args))
               (not (symbolp (car (te-args->expr-lst args))))
               (not (equal (car (car (te-args->expr-lst args)))
                           'quote))
               (pseudo-lambdap (car (car (te-args->expr-lst args))))
               (not (consp (car (car (te-args->expr-lst args))))))
          (not (car (car (te-args->expr-lst args))))))

Theorem: consp-of-pseudo-lambdap

(defthm consp-of-pseudo-lambdap
  (implies (pseudo-lambdap x) (consp x)))

Theorem: symbol-string-alistp-is-true-listp

(defthm symbol-string-alistp-is-true-listp
  (implies (and (symbol-string-alistp alist)
                (not (consp (assoc-equal key alist))))
           (not (assoc-equal key alist))))

Function: translate-declaration

(defun translate-declaration (name type fty-info int-to-rat)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp type)
                             (fty-info-alist-p fty-info)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-declaration))
  (declare (ignorable acl2::__function__))
  (b*
   ((name (symbol-fix name))
    (type (symbol-fix type))
    (translated-name (translate-symbol name))
    (fty-item (assoc-equal type fty-info))
    (type (if fty-item (fty-info->name (cdr fty-item))
            type))
    (translated-type (translate-type type int-to-rat 'common-type)))
   (cons
    translated-name
    (cons
     '=
     (cons
      '"z3.Const"
      (cons
       '#\(
       (cons
         '#\'
         (cons translated-name
               (cons '#\'
                     (cons '#\,
                           (cons '#\Space
                                 (cons translated-type
                                       '(#\) #\Newline))))))))))))))

Theorem: paragraphp-of-translate-declaration

(defthm paragraphp-of-translate-declaration
  (b* ((translated
            (translate-declaration name type fty-info int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-type-decl-list

(defun translate-type-decl-list
       (type-decl-lst fty-info acc int-to-rat)
 (declare (xargs :guard (and (decl-listp type-decl-lst)
                             (fty-info-alist-p fty-info)
                             (paragraphp acc)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-type-decl-list))
   (declare (ignorable acl2::__function__))
   (b*
    ((type-decl-lst (decl-list-fix type-decl-lst))
     (acc (paragraph-fix acc))
     ((unless (consp type-decl-lst)) acc)
     ((cons first rest) type-decl-lst)
     ((decl d) first)
     ((hint-pair h) d.type)
     (translated-type-decl
          (translate-declaration d.name h.thm fty-info int-to-rat)))
    (translate-type-decl-list
         rest
         fty-info (cons translated-type-decl acc)
         int-to-rat))))

Theorem: paragraphp-of-translate-type-decl-list

(defthm paragraphp-of-translate-type-decl-list
  (b* ((translated (translate-type-decl-list
                        type-decl-lst fty-info acc int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-theorem

(defun translate-theorem (theorem fn-lst fty-info acc)
 (declare (xargs :guard (and (pseudo-termp theorem)
                             (func-alistp fn-lst)
                             (fty-info-alist-p fty-info)
                             (symbol-listp acc))))
 (let ((acl2::__function__ 'translate-theorem))
  (declare (ignorable acl2::__function__))
  (b*
   ((theorem (pseudo-term-fix theorem))
    ((mv translated-theorem-body
         smt-precond symbols & &)
     (with-fast-alists
        (fn-lst)
        (translate-expression (make-te-args :expr-lst (list theorem)
                                            :fn-lst fn-lst
                                            :fty-info fty-info
                                            :symbol-index 0
                                            :symbol-list nil
                                            :avoid-list acc))))
    (theorem-assign
         (cons '"theorem = "
               (cons translated-theorem-body '(#\Newline))))
    (prove-theorem '("_SMT_.prove(theorem)" #\Newline)))
   (mv (cons theorem-assign
             (cons prove-theorem 'nil))
       smt-precond symbols))))

Theorem: paragraphp-of-translate-theorem.translated

(defthm paragraphp-of-translate-theorem.translated
  (b* (((mv ?translated ?smt-precond ?symbols)
        (translate-theorem theorem fn-lst fty-info acc)))
    (paragraphp translated))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-translate-theorem.smt-precond

(defthm pseudo-termp-of-translate-theorem.smt-precond
  (b* (((mv ?translated ?smt-precond ?symbols)
        (translate-theorem theorem fn-lst fty-info acc)))
    (pseudo-termp smt-precond))
  :rule-classes :rewrite)

Theorem: string-listp-of-translate-theorem.symbols

(defthm string-listp-of-translate-theorem.symbols
  (b* (((mv ?translated ?smt-precond ?symbols)
        (translate-theorem theorem fn-lst fty-info acc)))
    (string-listp symbols))
  :rule-classes :rewrite)

Function: translate-uninterpreted-arguments

(defun translate-uninterpreted-arguments
       (type args fty-info int-to-rat)
  (declare (xargs :guard (and (symbolp type)
                              (decl-listp args)
                              (fty-info-alist-p fty-info)
                              (booleanp int-to-rat))))
  (let ((acl2::__function__ 'translate-uninterpreted-arguments))
    (declare (ignorable acl2::__function__))
    (b* ((type (symbol-fix type))
         (args (decl-list-fix args))
         ((unless (consp args)) nil)
         ((cons first rest) args)
         ((decl d) first)
         ((hint-pair h) d.type)
         (fty-item (assoc-equal h.thm fty-info))
         (type-name (if fty-item (fty-info->name (cdr fty-item))
                      h.thm))
         (translated-type
              (translate-type type-name int-to-rat 'uninterpreted)))
      (cons (cons '#\,
                  (cons '#\Space
                        (cons translated-type 'nil)))
            (translate-uninterpreted-arguments
                 type rest fty-info int-to-rat)))))

Theorem: paragraphp-of-translate-uninterpreted-arguments

(defthm paragraphp-of-translate-uninterpreted-arguments
  (b* ((translated (translate-uninterpreted-arguments
                        type args fty-info int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-uninterpreted-decl

(defun translate-uninterpreted-decl (fn fty-info int-to-rat)
 (declare (xargs :guard (and (func-p fn)
                             (fty-info-alist-p fty-info)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-uninterpreted-decl))
  (declare (ignorable acl2::__function__))
  (b*
   ((fn (func-fix fn))
    ((func f) fn)
    (name f.name)
    (translated-formals (translate-uninterpreted-arguments
                             'formals
                             f.formals fty-info int-to-rat))
    ((if (> (len f.returns) 1))
     (er hard?
         'smt-translator=>translate-uninterpreted-decl
         "Currently, ~
            mv returns are not supported."))
    (translated-returns (translate-uninterpreted-arguments
                             'returns
                             f.returns fty-info int-to-rat)))
   (cons
      (translate-symbol name)
      (cons '"= z3.Function("
            (cons '#\'
                  (cons name
                        (cons '#\'
                              (cons translated-formals
                                    (cons translated-returns
                                          '(")" #\Newline)))))))))))

Theorem: paragraphp-of-translate-uninterpreted-decl

(defthm paragraphp-of-translate-uninterpreted-decl
  (b* ((translated
            (translate-uninterpreted-decl fn fty-info int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-uninterpreted-decl-lst

(defun translate-uninterpreted-decl-lst
       (fn-lst fty-info acc int-to-rat)
 (declare (xargs :guard (and (func-alistp fn-lst)
                             (fty-info-alist-p fty-info)
                             (paragraphp acc)
                             (booleanp int-to-rat))))
 (let ((acl2::__function__ 'translate-uninterpreted-decl-lst))
  (declare (ignorable acl2::__function__))
  (b*
   ((fn-lst (func-alist-fix fn-lst))
    (acc (paragraph-fix acc))
    ((unless (consp fn-lst)) acc)
    ((cons first rest) fn-lst)
    (first-decl (translate-uninterpreted-decl (cdr first)
                                              fty-info int-to-rat)))
   (translate-uninterpreted-decl-lst
        rest fty-info (cons first-decl acc)
        int-to-rat))))

Theorem: paragraphp-of-translate-uninterpreted-decl-lst

(defthm paragraphp-of-translate-uninterpreted-decl-lst
  (b* ((translated (translate-uninterpreted-decl-lst
                        fn-lst fty-info acc int-to-rat)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-symbol-declare

(defun translate-symbol-declare (symbols)
  (declare (xargs :guard (string-listp symbols)))
  (let ((acl2::__function__ 'translate-symbol-declare))
    (declare (ignorable acl2::__function__))
    (b* ((symbols (str::string-list-fix symbols))
         ((unless (consp symbols)) nil)
         ((cons first rest) symbols))
      (cons (cons first
                  (cons '" = Symbol_z3.intern('"
                        (cons first '("')" #\Newline))))
            (translate-symbol-declare rest)))))

Theorem: paragraphp-of-translate-symbol-declare

(defthm paragraphp-of-translate-symbol-declare
  (b* ((translated (translate-symbol-declare symbols)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: translate-symbol-enumeration

(defun translate-symbol-enumeration (symbols)
  (declare (xargs :guard (string-listp symbols)))
  (let ((acl2::__function__ 'translate-symbol-enumeration))
    (declare (ignorable acl2::__function__))
    (b* ((datatype-line '("Symbol_z3 = _SMT_.Symbol()" #\Newline))
         (declarations (translate-symbol-declare symbols)))
      (cons datatype-line declarations))))

Theorem: paragraphp-of-translate-symbol-enumeration

(defthm paragraphp-of-translate-symbol-enumeration
  (b* ((translated (translate-symbol-enumeration symbols)))
    (paragraphp translated))
  :rule-classes :rewrite)

Function: smt-translation

(defun smt-translation (term smtlink-hint state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp term)
                             (smtlink-hint-p smtlink-hint))))
 (let ((acl2::__function__ 'smt-translation))
  (declare (ignorable acl2::__function__))
  (b*
   ((term (pseudo-term-fix term))
    (smtlink-hint (smtlink-hint-fix smtlink-hint))
    ((smtlink-hint h) smtlink-hint)
    (fn-alst (make-alist-fn-lst h.functions))
    ((mv decl-list theorem)
     (smt-extract term h.fty-info h.abs))
    ((mv fn-decl-list type-decl-list)
     (recover-type-hyp decl-list
                       fn-alst h.fty-info h.abs nil state))
    ((unless (and (func-alistp fn-decl-list)
                  (decl-listp type-decl-list)))
     (mv
      (er
       hard? 'translator=>smt-translation
       "returned values from ~
    recover-type-hyp is not of the right type!~%")
      nil))
    (acc (all-vars1 term nil))
    ((unless (symbol-listp acc))
     (mv
      (er
       hard? 'translator=>smt-translation
       "returned values from ~
    acl2::all-vars1 is not of type symbol-listp!~%")
      nil))
    ((mv translated-theorem smt-precond symbols)
     (translate-theorem theorem fn-decl-list h.fty-info acc))
    (pretty-translated-theorem
         (pretty-print-theorem translated-theorem 160))
    (symbols (remove-duplicates-equal symbols))
    (translated-uninterpreted-decls
         (with-fast-alist fn-decl-list
                          (translate-uninterpreted-decl-lst
                               fn-decl-list
                               h.fty-info pretty-translated-theorem
                               h.int-to-rat)))
    (translated-theorem-with-type-decls
         (translate-type-decl-list type-decl-list h.fty-info
                                   translated-uninterpreted-decls
                                   h.int-to-rat))
    (translated-abs-types (translate-abstract-types h.abs))
    (translated-fty-types
         (translate-fty-types h.fty-types h.int-to-rat))
    (translated-theorem-with-fty-type-decls
         (append translated-abs-types
                 (append translated-fty-types
                         translated-theorem-with-type-decls)))
    (translated-symbol (translate-symbol-enumeration symbols)))
   (mv (cons translated-symbol
             translated-theorem-with-fty-type-decls)
       smt-precond))))

Subtopics

Paragraphp

A paragraph is made up of lists of words. Notice a single word is also counted as a paragraphp.