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

• Verified

Fty-support

Supports for ftytypes

Definitions and Theorems

Function: flexprod-field-p

(defun fty::flexprod-field-p (acl2::x)
 (declare (xargs :guard t))
 (and
    (consp acl2::x)
    (eq (car acl2::x) :field)
    (alistp (cdr acl2::x))
    (consp (cdr acl2::x))
    (let ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
          (fty::acc-body (cdr (assoc 'fty::acc-body (cdr acl2::x))))
          (fty::acc-name (cdr (assoc 'fty::acc-name (cdr acl2::x))))
          (type (cdr (assoc 'type (cdr acl2::x))))
          (fix (cdr (assoc 'fix (cdr acl2::x))))
          (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
          (fty::reqfix (cdr (assoc 'fty::reqfix (cdr acl2::x))))
          (fty::reqfix-vars (cdr (assoc 'fty::reqfix-vars
                                        (cdr acl2::x))))
          (default (cdr (assoc 'default (cdr acl2::x))))
          (doc (cdr (assoc 'doc (cdr acl2::x))))
          (fty::rule-classes (cdr (assoc 'fty::rule-classes
                                         (cdr acl2::x))))
          (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
          (fty::shared (cdr (assoc 'fty::shared (cdr acl2::x)))))
      (declare (ignorable fty::name
                          fty::acc-body fty::acc-name type fix
                          fty::equiv fty::reqfix fty::reqfix-vars
                          default doc fty::rule-classes
                          fty::recp fty::shared))
      t)))

Function: flexprod-field-p

(defun fty::flexprod-field-p (acl2::x)
 (declare (xargs :guard t))
 (and
    (consp acl2::x)
    (eq (car acl2::x) :field)
    (alistp (cdr acl2::x))
    (consp (cdr acl2::x))
    (let ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
          (fty::acc-body (cdr (assoc 'fty::acc-body (cdr acl2::x))))
          (fty::acc-name (cdr (assoc 'fty::acc-name (cdr acl2::x))))
          (type (cdr (assoc 'type (cdr acl2::x))))
          (fix (cdr (assoc 'fix (cdr acl2::x))))
          (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
          (fty::reqfix (cdr (assoc 'fty::reqfix (cdr acl2::x))))
          (fty::reqfix-vars (cdr (assoc 'fty::reqfix-vars
                                        (cdr acl2::x))))
          (default (cdr (assoc 'default (cdr acl2::x))))
          (doc (cdr (assoc 'doc (cdr acl2::x))))
          (fty::rule-classes (cdr (assoc 'fty::rule-classes
                                         (cdr acl2::x))))
          (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
          (fty::shared (cdr (assoc 'fty::shared (cdr acl2::x)))))
      (declare (ignorable fty::name
                          fty::acc-body fty::acc-name type fix
                          fty::equiv fty::reqfix fty::reqfix-vars
                          default doc fty::rule-classes
                          fty::recp fty::shared))
      t)))

Function: flexprod-field->acc-name$inline

(defun fty::flexprod-field->acc-name$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-field-p acl2::x)))
  (cdr (assoc 'fty::acc-name (cdr acl2::x))))

Function: flexprod-field->acc-name$inline

(defun fty::flexprod-field->acc-name$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-field-p acl2::x)))
  (cdr (assoc 'fty::acc-name (cdr acl2::x))))

Function: flexprod-field->type$inline

(defun fty::flexprod-field->type$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-field-p acl2::x)))
  (cdr (assoc 'type (cdr acl2::x))))

Function: flexprod-field->type$inline

(defun fty::flexprod-field->type$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-field-p acl2::x)))
  (cdr (assoc 'type (cdr acl2::x))))

Function: flexprod-field->name$inline

(defun fty::flexprod-field->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-field-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexprod-field->name$inline

(defun fty::flexprod-field->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-field-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexprod-p

(defun fty::flexprod-p (acl2::x)
 (declare (xargs :guard t))
 (and
   (consp acl2::x)
   (eq (car acl2::x) :prod)
   (alistp (cdr acl2::x))
   (consp (cdr acl2::x))
   (let
     ((fty::kind (cdr (assoc 'fty::kind (cdr acl2::x))))
      (cond (cdr (assoc 'cond (cdr acl2::x))))
      (guard (cdr (assoc 'guard (cdr acl2::x))))
      (fty::shape (cdr (assoc 'fty::shape (cdr acl2::x))))
      (require (cdr (assoc 'require (cdr acl2::x))))
      (fty::fields (cdr (assoc 'fty::fields (cdr acl2::x))))
      (fty::type-name (cdr (assoc 'fty::type-name (cdr acl2::x))))
      (fty::ctor-name (cdr (assoc 'fty::ctor-name (cdr acl2::x))))
      (fty::ctor-macro (cdr (assoc 'fty::ctor-macro (cdr acl2::x))))
      (fty::ctor-body (cdr (assoc 'fty::ctor-body (cdr acl2::x))))
      (fty::remake-name (cdr (assoc 'fty::remake-name
                                    (cdr acl2::x))))
      (fty::remake-body (cdr (assoc 'fty::remake-body
                                    (cdr acl2::x))))
      (fty::short (cdr (assoc 'fty::short (cdr acl2::x))))
      (fty::long (cdr (assoc 'fty::long (cdr acl2::x))))
      (inline (cdr (assoc 'inline (cdr acl2::x))))
      (fty::extra-binder-names (cdr (assoc 'fty::extra-binder-names
                                           (cdr acl2::x))))
      (fty::count-incr (cdr (assoc 'fty::count-incr (cdr acl2::x))))
      (fty::no-ctor-macros (cdr (assoc 'fty::no-ctor-macros
                                       (cdr acl2::x)))))
     (declare (ignorable fty::kind cond guard fty::shape
                         require fty::fields fty::type-name
                         fty::ctor-name fty::ctor-macro
                         fty::ctor-body fty::remake-name
                         fty::remake-body fty::short
                         fty::long inline fty::extra-binder-names
                         fty::count-incr fty::no-ctor-macros))
     t)))

Function: flexprod-p

(defun fty::flexprod-p (acl2::x)
 (declare (xargs :guard t))
 (and
   (consp acl2::x)
   (eq (car acl2::x) :prod)
   (alistp (cdr acl2::x))
   (consp (cdr acl2::x))
   (let
     ((fty::kind (cdr (assoc 'fty::kind (cdr acl2::x))))
      (cond (cdr (assoc 'cond (cdr acl2::x))))
      (guard (cdr (assoc 'guard (cdr acl2::x))))
      (fty::shape (cdr (assoc 'fty::shape (cdr acl2::x))))
      (require (cdr (assoc 'require (cdr acl2::x))))
      (fty::fields (cdr (assoc 'fty::fields (cdr acl2::x))))
      (fty::type-name (cdr (assoc 'fty::type-name (cdr acl2::x))))
      (fty::ctor-name (cdr (assoc 'fty::ctor-name (cdr acl2::x))))
      (fty::ctor-macro (cdr (assoc 'fty::ctor-macro (cdr acl2::x))))
      (fty::ctor-body (cdr (assoc 'fty::ctor-body (cdr acl2::x))))
      (fty::remake-name (cdr (assoc 'fty::remake-name
                                    (cdr acl2::x))))
      (fty::remake-body (cdr (assoc 'fty::remake-body
                                    (cdr acl2::x))))
      (fty::short (cdr (assoc 'fty::short (cdr acl2::x))))
      (fty::long (cdr (assoc 'fty::long (cdr acl2::x))))
      (inline (cdr (assoc 'inline (cdr acl2::x))))
      (fty::extra-binder-names (cdr (assoc 'fty::extra-binder-names
                                           (cdr acl2::x))))
      (fty::count-incr (cdr (assoc 'fty::count-incr (cdr acl2::x))))
      (fty::no-ctor-macros (cdr (assoc 'fty::no-ctor-macros
                                       (cdr acl2::x)))))
     (declare (ignorable fty::kind cond guard fty::shape
                         require fty::fields fty::type-name
                         fty::ctor-name fty::ctor-macro
                         fty::ctor-body fty::remake-name
                         fty::remake-body fty::short
                         fty::long inline fty::extra-binder-names
                         fty::count-incr fty::no-ctor-macros))
     t)))

Function: flexprod->type-name$inline

(defun fty::flexprod->type-name$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-p acl2::x)))
  (cdr (assoc 'fty::type-name (cdr acl2::x))))

Function: flexprod->type-name$inline

(defun fty::flexprod->type-name$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-p acl2::x)))
  (cdr (assoc 'fty::type-name (cdr acl2::x))))

Function: flexprod->kind$inline

(defun fty::flexprod->kind$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-p acl2::x)))
  (cdr (assoc 'fty::kind (cdr acl2::x))))

Function: flexprod->kind$inline

(defun fty::flexprod->kind$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-p acl2::x)))
  (cdr (assoc 'fty::kind (cdr acl2::x))))

Function: flexsum-p

(defun fty::flexsum-p (acl2::x)
 (declare (xargs :guard t))
 (and
   (consp acl2::x)
   (eq (car acl2::x) :sum)
   (alistp (cdr acl2::x))
   (consp (cdr acl2::x))
   (let
     ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
      (fty::pred (cdr (assoc 'fty::pred (cdr acl2::x))))
      (fix (cdr (assoc 'fix (cdr acl2::x))))
      (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
      (fty::kind (cdr (assoc 'fty::kind (cdr acl2::x))))
      (fty::kind-body (cdr (assoc 'fty::kind-body (cdr acl2::x))))
      (count (cdr (assoc 'count (cdr acl2::x))))
      (case (cdr (assoc 'case (cdr acl2::x))))
      (fty::prods (cdr (assoc 'fty::prods (cdr acl2::x))))
      (fty::measure (cdr (assoc 'fty::measure (cdr acl2::x))))
      (fty::shape (cdr (assoc 'fty::shape (cdr acl2::x))))
      (fty::xvar (cdr (assoc 'fty::xvar (cdr acl2::x))))
      (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
      (fty::orig-prods (cdr (assoc 'fty::orig-prods (cdr acl2::x))))
      (inline (cdr (assoc 'inline (cdr acl2::x))))
      (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
      (fty::typemacro (cdr (assoc 'fty::typemacro (cdr acl2::x)))))
     (declare (ignorable fty::name fty::pred fix fty::equiv
                         fty::kind fty::kind-body count
                         case fty::prods fty::measure fty::shape
                         fty::xvar fty::kwd-alist fty::orig-prods
                         inline fty::recp fty::typemacro))
     t)))

Function: flexsum-p

(defun fty::flexsum-p (acl2::x)
 (declare (xargs :guard t))
 (and
   (consp acl2::x)
   (eq (car acl2::x) :sum)
   (alistp (cdr acl2::x))
   (consp (cdr acl2::x))
   (let
     ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
      (fty::pred (cdr (assoc 'fty::pred (cdr acl2::x))))
      (fix (cdr (assoc 'fix (cdr acl2::x))))
      (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
      (fty::kind (cdr (assoc 'fty::kind (cdr acl2::x))))
      (fty::kind-body (cdr (assoc 'fty::kind-body (cdr acl2::x))))
      (count (cdr (assoc 'count (cdr acl2::x))))
      (case (cdr (assoc 'case (cdr acl2::x))))
      (fty::prods (cdr (assoc 'fty::prods (cdr acl2::x))))
      (fty::measure (cdr (assoc 'fty::measure (cdr acl2::x))))
      (fty::shape (cdr (assoc 'fty::shape (cdr acl2::x))))
      (fty::xvar (cdr (assoc 'fty::xvar (cdr acl2::x))))
      (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
      (fty::orig-prods (cdr (assoc 'fty::orig-prods (cdr acl2::x))))
      (inline (cdr (assoc 'inline (cdr acl2::x))))
      (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
      (fty::typemacro (cdr (assoc 'fty::typemacro (cdr acl2::x)))))
     (declare (ignorable fty::name fty::pred fix fty::equiv
                         fty::kind fty::kind-body count
                         case fty::prods fty::measure fty::shape
                         fty::xvar fty::kwd-alist fty::orig-prods
                         inline fty::recp fty::typemacro))
     t)))

Function: flexsum->fix$inline

(defun fty::flexsum->fix$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fix (cdr acl2::x))))

Function: flexsum->fix$inline

(defun fty::flexsum->fix$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fix (cdr acl2::x))))

Function: flexsum->pred$inline

(defun fty::flexsum->pred$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fty::pred (cdr acl2::x))))

Function: flexsum->pred$inline

(defun fty::flexsum->pred$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fty::pred (cdr acl2::x))))

Function: flexsum->name$inline

(defun fty::flexsum->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexsum->name$inline

(defun fty::flexsum->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexlist-p

(defun fty::flexlist-p (acl2::x)
 (declare (xargs :guard t))
 (and
   (consp acl2::x)
   (eq (car acl2::x) :list)
   (alistp (cdr acl2::x))
   (consp (cdr acl2::x))
   (let
     ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
      (fty::pred (cdr (assoc 'fty::pred (cdr acl2::x))))
      (fix (cdr (assoc 'fix (cdr acl2::x))))
      (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
      (count (cdr (assoc 'count (cdr acl2::x))))
      (fty::elt-type (cdr (assoc 'fty::elt-type (cdr acl2::x))))
      (fty::elt-fix (cdr (assoc 'fty::elt-fix (cdr acl2::x))))
      (fty::elt-equiv (cdr (assoc 'fty::elt-equiv (cdr acl2::x))))
      (fty::measure (cdr (assoc 'fty::measure (cdr acl2::x))))
      (fty::xvar (cdr (assoc 'fty::xvar (cdr acl2::x))))
      (fty::non-emptyp (cdr (assoc 'fty::non-emptyp (cdr acl2::x))))
      (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
      (true-listp (cdr (assoc 'true-listp (cdr acl2::x))))
      (fty::elementp-of-nil (cdr (assoc 'fty::elementp-of-nil
                                        (cdr acl2::x))))
      (fty::cheap (cdr (assoc 'fty::cheap (cdr acl2::x))))
      (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
      (fty::already-definedp (cdr (assoc 'fty::already-definedp
                                         (cdr acl2::x))))
      (fty::fix-already-definedp
           (cdr (assoc 'fty::fix-already-definedp
                       (cdr acl2::x)))))
     (declare (ignorable fty::name fty::pred
                         fix fty::equiv count fty::elt-type
                         fty::elt-fix fty::elt-equiv
                         fty::measure fty::xvar fty::non-emptyp
                         fty::kwd-alist true-listp
                         fty::elementp-of-nil fty::cheap
                         fty::recp fty::already-definedp
                         fty::fix-already-definedp))
     t)))

Function: flexlist-p

(defun fty::flexlist-p (acl2::x)
 (declare (xargs :guard t))
 (and
   (consp acl2::x)
   (eq (car acl2::x) :list)
   (alistp (cdr acl2::x))
   (consp (cdr acl2::x))
   (let
     ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
      (fty::pred (cdr (assoc 'fty::pred (cdr acl2::x))))
      (fix (cdr (assoc 'fix (cdr acl2::x))))
      (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
      (count (cdr (assoc 'count (cdr acl2::x))))
      (fty::elt-type (cdr (assoc 'fty::elt-type (cdr acl2::x))))
      (fty::elt-fix (cdr (assoc 'fty::elt-fix (cdr acl2::x))))
      (fty::elt-equiv (cdr (assoc 'fty::elt-equiv (cdr acl2::x))))
      (fty::measure (cdr (assoc 'fty::measure (cdr acl2::x))))
      (fty::xvar (cdr (assoc 'fty::xvar (cdr acl2::x))))
      (fty::non-emptyp (cdr (assoc 'fty::non-emptyp (cdr acl2::x))))
      (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
      (true-listp (cdr (assoc 'true-listp (cdr acl2::x))))
      (fty::elementp-of-nil (cdr (assoc 'fty::elementp-of-nil
                                        (cdr acl2::x))))
      (fty::cheap (cdr (assoc 'fty::cheap (cdr acl2::x))))
      (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
      (fty::already-definedp (cdr (assoc 'fty::already-definedp
                                         (cdr acl2::x))))
      (fty::fix-already-definedp
           (cdr (assoc 'fty::fix-already-definedp
                       (cdr acl2::x)))))
     (declare (ignorable fty::name fty::pred
                         fix fty::equiv count fty::elt-type
                         fty::elt-fix fty::elt-equiv
                         fty::measure fty::xvar fty::non-emptyp
                         fty::kwd-alist true-listp
                         fty::elementp-of-nil fty::cheap
                         fty::recp fty::already-definedp
                         fty::fix-already-definedp))
     t)))

Function: flexlist->fix$inline

(defun fty::flexlist->fix$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fix (cdr acl2::x))))

Function: flexlist->fix$inline

(defun fty::flexlist->fix$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fix (cdr acl2::x))))

Function: flexlist->pred$inline

(defun fty::flexlist->pred$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fty::pred (cdr acl2::x))))

Function: flexlist->pred$inline

(defun fty::flexlist->pred$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fty::pred (cdr acl2::x))))

Function: flexlist->name$inline

(defun fty::flexlist->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexlist->name$inline

(defun fty::flexlist->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexlist->true-listp$inline

(defun fty::flexlist->true-listp$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'true-listp (cdr acl2::x))))

Function: flexlist->true-listp$inline

(defun fty::flexlist->true-listp$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'true-listp (cdr acl2::x))))

Function: flexlist->elt-type$inline

(defun fty::flexlist->elt-type$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fty::elt-type (cdr acl2::x))))

Function: flexlist->elt-type$inline

(defun fty::flexlist->elt-type$inline (acl2::x)
  (declare (xargs :guard (fty::flexlist-p acl2::x)))
  (cdr (assoc 'fty::elt-type (cdr acl2::x))))

Function: flexalist-p

(defun fty::flexalist-p (acl2::x)
 (declare (xargs :guard t))
 (and
  (consp acl2::x)
  (eq (car acl2::x) :alist)
  (alistp (cdr acl2::x))
  (consp (cdr acl2::x))
  (let ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
        (fty::pred (cdr (assoc 'fty::pred (cdr acl2::x))))
        (fix (cdr (assoc 'fix (cdr acl2::x))))
        (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
        (count (cdr (assoc 'count (cdr acl2::x))))
        (fty::key-type (cdr (assoc 'fty::key-type (cdr acl2::x))))
        (fty::key-fix (cdr (assoc 'fty::key-fix (cdr acl2::x))))
        (fty::key-equiv (cdr (assoc 'fty::key-equiv (cdr acl2::x))))
        (fty::val-type (cdr (assoc 'fty::val-type (cdr acl2::x))))
        (fty::val-fix (cdr (assoc 'fty::val-fix (cdr acl2::x))))
        (fty::val-equiv (cdr (assoc 'fty::val-equiv (cdr acl2::x))))
        (fty::strategy (cdr (assoc 'fty::strategy (cdr acl2::x))))
        (fty::measure (cdr (assoc 'fty::measure (cdr acl2::x))))
        (fty::xvar (cdr (assoc 'fty::xvar (cdr acl2::x))))
        (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
        (fty::keyp-of-nil (cdr (assoc 'fty::keyp-of-nil
                                      (cdr acl2::x))))
        (fty::valp-of-nil (cdr (assoc 'fty::valp-of-nil
                                      (cdr acl2::x))))
        (true-listp (cdr (assoc 'true-listp (cdr acl2::x))))
        (fty::unique-keys (cdr (assoc 'fty::unique-keys
                                      (cdr acl2::x))))
        (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
        (fty::already-definedp (cdr (assoc 'fty::already-definedp
                                           (cdr acl2::x))))
        (fty::fix-already-definedp
             (cdr (assoc 'fty::fix-already-definedp
                         (cdr acl2::x)))))
    (declare (ignorable fty::name fty::pred
                        fix fty::equiv count fty::key-type
                        fty::key-fix fty::key-equiv
                        fty::val-type fty::val-fix
                        fty::val-equiv fty::strategy
                        fty::measure fty::xvar fty::kwd-alist
                        fty::keyp-of-nil fty::valp-of-nil
                        true-listp fty::unique-keys
                        fty::recp fty::already-definedp
                        fty::fix-already-definedp))
    t)))

Function: flexalist-p

(defun fty::flexalist-p (acl2::x)
 (declare (xargs :guard t))
 (and
  (consp acl2::x)
  (eq (car acl2::x) :alist)
  (alistp (cdr acl2::x))
  (consp (cdr acl2::x))
  (let ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
        (fty::pred (cdr (assoc 'fty::pred (cdr acl2::x))))
        (fix (cdr (assoc 'fix (cdr acl2::x))))
        (fty::equiv (cdr (assoc 'fty::equiv (cdr acl2::x))))
        (count (cdr (assoc 'count (cdr acl2::x))))
        (fty::key-type (cdr (assoc 'fty::key-type (cdr acl2::x))))
        (fty::key-fix (cdr (assoc 'fty::key-fix (cdr acl2::x))))
        (fty::key-equiv (cdr (assoc 'fty::key-equiv (cdr acl2::x))))
        (fty::val-type (cdr (assoc 'fty::val-type (cdr acl2::x))))
        (fty::val-fix (cdr (assoc 'fty::val-fix (cdr acl2::x))))
        (fty::val-equiv (cdr (assoc 'fty::val-equiv (cdr acl2::x))))
        (fty::strategy (cdr (assoc 'fty::strategy (cdr acl2::x))))
        (fty::measure (cdr (assoc 'fty::measure (cdr acl2::x))))
        (fty::xvar (cdr (assoc 'fty::xvar (cdr acl2::x))))
        (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
        (fty::keyp-of-nil (cdr (assoc 'fty::keyp-of-nil
                                      (cdr acl2::x))))
        (fty::valp-of-nil (cdr (assoc 'fty::valp-of-nil
                                      (cdr acl2::x))))
        (true-listp (cdr (assoc 'true-listp (cdr acl2::x))))
        (fty::unique-keys (cdr (assoc 'fty::unique-keys
                                      (cdr acl2::x))))
        (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x))))
        (fty::already-definedp (cdr (assoc 'fty::already-definedp
                                           (cdr acl2::x))))
        (fty::fix-already-definedp
             (cdr (assoc 'fty::fix-already-definedp
                         (cdr acl2::x)))))
    (declare (ignorable fty::name fty::pred
                        fix fty::equiv count fty::key-type
                        fty::key-fix fty::key-equiv
                        fty::val-type fty::val-fix
                        fty::val-equiv fty::strategy
                        fty::measure fty::xvar fty::kwd-alist
                        fty::keyp-of-nil fty::valp-of-nil
                        true-listp fty::unique-keys
                        fty::recp fty::already-definedp
                        fty::fix-already-definedp))
    t)))

Function: flexalist->fix$inline

(defun fty::flexalist->fix$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fix (cdr acl2::x))))

Function: flexalist->fix$inline

(defun fty::flexalist->fix$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fix (cdr acl2::x))))

Function: flexalist->pred$inline

(defun fty::flexalist->pred$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::pred (cdr acl2::x))))

Function: flexalist->pred$inline

(defun fty::flexalist->pred$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::pred (cdr acl2::x))))

Function: flexalist->name$inline

(defun fty::flexalist->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexalist->name$inline

(defun fty::flexalist->name$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::name (cdr acl2::x))))

Function: flexalist->true-listp$inline

(defun fty::flexalist->true-listp$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'true-listp (cdr acl2::x))))

Function: flexalist->true-listp$inline

(defun fty::flexalist->true-listp$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'true-listp (cdr acl2::x))))

Function: flexalist->key-type$inline

(defun fty::flexalist->key-type$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::key-type (cdr acl2::x))))

Function: flexalist->key-type$inline

(defun fty::flexalist->key-type$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::key-type (cdr acl2::x))))

Function: flexalist->val-type$inline

(defun fty::flexalist->val-type$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::val-type (cdr acl2::x))))

Function: flexalist->val-type$inline

(defun fty::flexalist->val-type$inline (acl2::x)
  (declare (xargs :guard (fty::flexalist-p acl2::x)))
  (cdr (assoc 'fty::val-type (cdr acl2::x))))

Function: flexprod->fields$inline

(defun fty::flexprod->fields$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-p acl2::x)))
  (cdr (assoc 'fty::fields (cdr acl2::x))))

Function: flexprod->fields$inline

(defun fty::flexprod->fields$inline (acl2::x)
  (declare (xargs :guard (fty::flexprod-p acl2::x)))
  (cdr (assoc 'fty::fields (cdr acl2::x))))

Function: flexsum->prods$inline

(defun fty::flexsum->prods$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fty::prods (cdr acl2::x))))

Function: flexsum->prods$inline

(defun fty::flexsum->prods$inline (acl2::x)
  (declare (xargs :guard (fty::flexsum-p acl2::x)))
  (cdr (assoc 'fty::prods (cdr acl2::x))))

Function: flextypes-p

(defun fty::flextypes-p (acl2::x)
 (declare (xargs :guard t))
 (and
  (consp acl2::x)
  (eq (car acl2::x) :flextypes)
  (alistp (cdr acl2::x))
  (consp (cdr acl2::x))
  (let ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
        (fty::types (cdr (assoc 'fty::types (cdr acl2::x))))
        (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
        (fty::no-count (cdr (assoc 'fty::no-count (cdr acl2::x))))
        (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x)))))
    (declare (ignorable fty::name fty::types
                        fty::kwd-alist fty::no-count fty::recp))
    t)))

Function: flextypes-p

(defun fty::flextypes-p (acl2::x)
 (declare (xargs :guard t))
 (and
  (consp acl2::x)
  (eq (car acl2::x) :flextypes)
  (alistp (cdr acl2::x))
  (consp (cdr acl2::x))
  (let ((fty::name (cdr (assoc 'fty::name (cdr acl2::x))))
        (fty::types (cdr (assoc 'fty::types (cdr acl2::x))))
        (fty::kwd-alist (cdr (assoc 'fty::kwd-alist (cdr acl2::x))))
        (fty::no-count (cdr (assoc 'fty::no-count (cdr acl2::x))))
        (fty::recp (cdr (assoc 'fty::recp (cdr acl2::x)))))
    (declare (ignorable fty::name fty::types
                        fty::kwd-alist fty::no-count fty::recp))
    t)))

Function: flextypes->types$inline

(defun fty::flextypes->types$inline (acl2::x)
  (declare (xargs :guard (fty::flextypes-p acl2::x)))
  (cdr (assoc 'fty::types (cdr acl2::x))))

Function: flextypes->types$inline

(defun fty::flextypes->types$inline (acl2::x)
  (declare (xargs :guard (fty::flextypes-p acl2::x)))
  (cdr (assoc 'fty::types (cdr acl2::x))))

Function: fty-info-p

(defun fty-info-p (x)
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'fty-info-p))
  (declare (ignorable acl2::__function__))
  (and
   (mbe
     :logic (and (alistp x)
                 (equal (strip-cars x)
                        '(name category type guards returns)))
     :exec
     (fty::alist-with-carsp x '(name category type guards returns)))
   (b* ((name (cdr (std::da-nth 0 x)))
        (category (cdr (std::da-nth 1 x)))
        (type (cdr (std::da-nth 2 x)))
        (guards (cdr (std::da-nth 3 x)))
        (returns (cdr (std::da-nth 4 x))))
     (and (symbolp name)
          (symbolp category)
          (symbolp type)
          (symbol-listp guards)
          (symbolp returns))))))

Theorem: consp-when-fty-info-p

(defthm consp-when-fty-info-p
  (implies (fty-info-p x) (consp x))
  :rule-classes :compound-recognizer)

Function: fty-info-fix$inline

(defun fty-info-fix$inline (x)
  (declare (xargs :guard (fty-info-p x)))
  (let ((acl2::__function__ 'fty-info-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((name (symbol-fix (cdr (std::da-nth 0 x))))
              (category (symbol-fix (cdr (std::da-nth 1 x))))
              (type (symbol-fix (cdr (std::da-nth 2 x))))
              (guards (symbol-list-fix (cdr (std::da-nth 3 x))))
              (returns (symbol-fix (cdr (std::da-nth 4 x)))))
           (list (cons 'name name)
                 (cons 'category category)
                 (cons 'type type)
                 (cons 'guards guards)
                 (cons 'returns returns)))
         :exec x)))

Theorem: fty-info-p-of-fty-info-fix

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

Theorem: fty-info-fix-when-fty-info-p

(defthm fty-info-fix-when-fty-info-p
  (implies (fty-info-p x)
           (equal (fty-info-fix x) x)))

Function: fty-info-equiv$inline

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

Theorem: fty-info-equiv-is-an-equivalence

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

Theorem: fty-info-equiv-implies-equal-fty-info-fix-1

(defthm fty-info-equiv-implies-equal-fty-info-fix-1
  (implies (fty-info-equiv acl2::x x-equiv)
           (equal (fty-info-fix acl2::x)
                  (fty-info-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: fty-info-fix-under-fty-info-equiv

(defthm fty-info-fix-under-fty-info-equiv
  (fty-info-equiv (fty-info-fix acl2::x)
                  acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-fty-info-fix-1-forward-to-fty-info-equiv

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

Theorem: equal-of-fty-info-fix-2-forward-to-fty-info-equiv

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

Theorem: fty-info-equiv-of-fty-info-fix-1-forward

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

Theorem: fty-info-equiv-of-fty-info-fix-2-forward

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

Function: fty-info->name$inline

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

Theorem: symbolp-of-fty-info->name

(defthm symbolp-of-fty-info->name
  (b* ((name (fty-info->name$inline x)))
    (symbolp name))
  :rule-classes :rewrite)

Theorem: fty-info->name$inline-of-fty-info-fix-x

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

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

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

Function: fty-info->category$inline

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

Theorem: symbolp-of-fty-info->category

(defthm symbolp-of-fty-info->category
  (b* ((category (fty-info->category$inline x)))
    (symbolp category))
  :rule-classes :rewrite)

Theorem: fty-info->category$inline-of-fty-info-fix-x

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

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

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

Function: fty-info->type$inline

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

Theorem: symbolp-of-fty-info->type

(defthm symbolp-of-fty-info->type
  (b* ((type (fty-info->type$inline x)))
    (symbolp type))
  :rule-classes :rewrite)

Theorem: fty-info->type$inline-of-fty-info-fix-x

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

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

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

Function: fty-info->guards$inline

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

Theorem: symbol-listp-of-fty-info->guards

(defthm symbol-listp-of-fty-info->guards
  (b* ((guards (fty-info->guards$inline x)))
    (symbol-listp guards))
  :rule-classes :rewrite)

Theorem: fty-info->guards$inline-of-fty-info-fix-x

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

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

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

Function: fty-info->returns$inline

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

Theorem: symbolp-of-fty-info->returns

(defthm symbolp-of-fty-info->returns
  (b* ((returns (fty-info->returns$inline x)))
    (symbolp returns))
  :rule-classes :rewrite)

Theorem: fty-info->returns$inline-of-fty-info-fix-x

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

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

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

Function: fty-info

(defun fty-info (name category type guards returns)
  (declare (xargs :guard (and (symbolp name)
                              (symbolp category)
                              (symbolp type)
                              (symbol-listp guards)
                              (symbolp returns))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-info))
    (declare (ignorable acl2::__function__))
    (b* ((name (mbe :logic (symbol-fix name)
                    :exec name))
         (category (mbe :logic (symbol-fix category)
                        :exec category))
         (type (mbe :logic (symbol-fix type)
                    :exec type))
         (guards (mbe :logic (symbol-list-fix guards)
                      :exec guards))
         (returns (mbe :logic (symbol-fix returns)
                       :exec returns)))
      (list (cons 'name name)
            (cons 'category category)
            (cons 'type type)
            (cons 'guards guards)
            (cons 'returns returns)))))

Theorem: fty-info-p-of-fty-info

(defthm fty-info-p-of-fty-info
  (b* ((x (fty-info name category type guards returns)))
    (fty-info-p x))
  :rule-classes :rewrite)

Theorem: fty-info->name-of-fty-info

(defthm fty-info->name-of-fty-info
  (equal
       (fty-info->name (fty-info name category type guards returns))
       (symbol-fix name)))

Theorem: fty-info->category-of-fty-info

(defthm fty-info->category-of-fty-info
 (equal
   (fty-info->category (fty-info name category type guards returns))
   (symbol-fix category)))

Theorem: fty-info->type-of-fty-info

(defthm fty-info->type-of-fty-info
  (equal
       (fty-info->type (fty-info name category type guards returns))
       (symbol-fix type)))

Theorem: fty-info->guards-of-fty-info

(defthm fty-info->guards-of-fty-info
 (equal
     (fty-info->guards (fty-info name category type guards returns))
     (symbol-list-fix guards)))

Theorem: fty-info->returns-of-fty-info

(defthm fty-info->returns-of-fty-info
 (equal
    (fty-info->returns (fty-info name category type guards returns))
    (symbol-fix returns)))

Theorem: fty-info-of-fields

(defthm fty-info-of-fields
  (equal (fty-info (fty-info->name x)
                   (fty-info->category x)
                   (fty-info->type x)
                   (fty-info->guards x)
                   (fty-info->returns x))
         (fty-info-fix x)))

Theorem: fty-info-fix-when-fty-info

(defthm fty-info-fix-when-fty-info
  (equal (fty-info-fix x)
         (fty-info (fty-info->name x)
                   (fty-info->category x)
                   (fty-info->type x)
                   (fty-info->guards x)
                   (fty-info->returns x))))

Theorem: equal-of-fty-info

(defthm equal-of-fty-info
  (equal (equal (fty-info name category type guards returns)
                x)
         (and (fty-info-p x)
              (equal (fty-info->name x)
                     (symbol-fix name))
              (equal (fty-info->category x)
                     (symbol-fix category))
              (equal (fty-info->type x)
                     (symbol-fix type))
              (equal (fty-info->guards x)
                     (symbol-list-fix guards))
              (equal (fty-info->returns x)
                     (symbol-fix returns)))))

Theorem: fty-info-of-symbol-fix-name

(defthm fty-info-of-symbol-fix-name
  (equal (fty-info (symbol-fix name)
                   category type guards returns)
         (fty-info name category type guards returns)))

Theorem: fty-info-symbol-equiv-congruence-on-name

(defthm fty-info-symbol-equiv-congruence-on-name
  (implies (acl2::symbol-equiv name name-equiv)
           (equal (fty-info name category type guards returns)
                  (fty-info name-equiv
                            category type guards returns)))
  :rule-classes :congruence)

Theorem: fty-info-of-symbol-fix-category

(defthm fty-info-of-symbol-fix-category
  (equal (fty-info name (symbol-fix category)
                   type guards returns)
         (fty-info name category type guards returns)))

Theorem: fty-info-symbol-equiv-congruence-on-category

(defthm fty-info-symbol-equiv-congruence-on-category
  (implies (acl2::symbol-equiv category category-equiv)
           (equal (fty-info name category type guards returns)
                  (fty-info name
                            category-equiv type guards returns)))
  :rule-classes :congruence)

Theorem: fty-info-of-symbol-fix-type

(defthm fty-info-of-symbol-fix-type
  (equal (fty-info name category (symbol-fix type)
                   guards returns)
         (fty-info name category type guards returns)))

Theorem: fty-info-symbol-equiv-congruence-on-type

(defthm fty-info-symbol-equiv-congruence-on-type
  (implies (acl2::symbol-equiv type type-equiv)
           (equal (fty-info name category type guards returns)
                  (fty-info name
                            category type-equiv guards returns)))
  :rule-classes :congruence)

Theorem: fty-info-of-symbol-list-fix-guards

(defthm fty-info-of-symbol-list-fix-guards
  (equal (fty-info name
                   category type (symbol-list-fix guards)
                   returns)
         (fty-info name category type guards returns)))

Theorem: fty-info-symbol-list-equiv-congruence-on-guards

(defthm fty-info-symbol-list-equiv-congruence-on-guards
  (implies (acl2::symbol-list-equiv guards guards-equiv)
           (equal (fty-info name category type guards returns)
                  (fty-info name
                            category type guards-equiv returns)))
  :rule-classes :congruence)

Theorem: fty-info-of-symbol-fix-returns

(defthm fty-info-of-symbol-fix-returns
  (equal (fty-info name category
                   type guards (symbol-fix returns))
         (fty-info name category type guards returns)))

Theorem: fty-info-symbol-equiv-congruence-on-returns

(defthm fty-info-symbol-equiv-congruence-on-returns
  (implies (acl2::symbol-equiv returns returns-equiv)
           (equal (fty-info name category type guards returns)
                  (fty-info name
                            category type guards returns-equiv)))
  :rule-classes :congruence)

Theorem: fty-info-fix-redef

(defthm fty-info-fix-redef
  (equal (fty-info-fix x)
         (fty-info (fty-info->name x)
                   (fty-info->category x)
                   (fty-info->type x)
                   (fty-info->guards x)
                   (fty-info->returns x)))
  :rule-classes :definition)

Function: fty-info-alist-p

(defun fty-info-alist-p (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-info-alist-p))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        (eq x nil)
      (and (consp (car x))
           (symbolp (caar x))
           (fty-info-p (cdar x))
           (fty-info-alist-p (cdr x))))))

Theorem: fty-info-alist-p-of-append

(defthm fty-info-alist-p-of-append
  (equal (fty-info-alist-p (append acl2::a acl2::b))
         (and (fty-info-alist-p (acl2::list-fix acl2::a))
              (fty-info-alist-p acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-rev

(defthm fty-info-alist-p-of-rev
  (equal (fty-info-alist-p (acl2::rev acl2::x))
         (fty-info-alist-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-list-fix

(defthm fty-info-alist-p-of-list-fix
  (implies (fty-info-alist-p acl2::x)
           (fty-info-alist-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-fty-info-alist-p-compound-recognizer

(defthm true-listp-when-fty-info-alist-p-compound-recognizer
  (implies (fty-info-alist-p acl2::x)
           (true-listp acl2::x))
  :rule-classes :compound-recognizer)

Theorem: fty-info-alist-p-when-not-consp

(defthm fty-info-alist-p-when-not-consp
  (implies (not (consp acl2::x))
           (equal (fty-info-alist-p acl2::x)
                  (not acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-cdr-when-fty-info-alist-p

(defthm fty-info-alist-p-of-cdr-when-fty-info-alist-p
  (implies (fty-info-alist-p (double-rewrite acl2::x))
           (fty-info-alist-p (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-cons

(defthm fty-info-alist-p-of-cons
  (equal (fty-info-alist-p (cons acl2::a acl2::x))
         (and (and (consp acl2::a)
                   (symbolp (car acl2::a))
                   (fty-info-p (cdr acl2::a)))
              (fty-info-alist-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-remove-assoc

(defthm fty-info-alist-p-of-remove-assoc
  (implies
       (fty-info-alist-p acl2::x)
       (fty-info-alist-p (remove-assoc-equal acl2::name acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-put-assoc

(defthm fty-info-alist-p-of-put-assoc
 (implies
  (and (fty-info-alist-p acl2::x))
  (iff
   (fty-info-alist-p (put-assoc-equal acl2::name acl2::val acl2::x))
   (and (symbolp acl2::name)
        (fty-info-p acl2::val))))
 :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-fast-alist-clean

(defthm fty-info-alist-p-of-fast-alist-clean
  (implies (fty-info-alist-p acl2::x)
           (fty-info-alist-p (fast-alist-clean acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-hons-shrink-alist

(defthm fty-info-alist-p-of-hons-shrink-alist
  (implies (and (fty-info-alist-p acl2::x)
                (fty-info-alist-p acl2::y))
           (fty-info-alist-p (hons-shrink-alist acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-alist-p-of-hons-acons

(defthm fty-info-alist-p-of-hons-acons
  (equal (fty-info-alist-p (hons-acons acl2::a acl2::n acl2::x))
         (and (symbolp acl2::a)
              (fty-info-p acl2::n)
              (fty-info-alist-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-info-p-of-cdr-of-hons-assoc-equal-when-fty-info-alist-p

(defthm fty-info-p-of-cdr-of-hons-assoc-equal-when-fty-info-alist-p
 (implies (fty-info-alist-p acl2::x)
          (iff (fty-info-p (cdr (hons-assoc-equal acl2::k acl2::x)))
               (or (hons-assoc-equal acl2::k acl2::x)
                   (fty-info-p nil))))
 :rule-classes ((:rewrite)))

Theorem: alistp-when-fty-info-alist-p-rewrite

(defthm alistp-when-fty-info-alist-p-rewrite
  (implies (fty-info-alist-p acl2::x)
           (alistp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-fty-info-alist-p

(defthm alistp-when-fty-info-alist-p
  (implies (fty-info-alist-p acl2::x)
           (alistp acl2::x))
  :rule-classes :tau-system)

Theorem: fty-info-p-of-cdar-when-fty-info-alist-p

(defthm fty-info-p-of-cdar-when-fty-info-alist-p
  (implies (fty-info-alist-p acl2::x)
           (iff (fty-info-p (cdar acl2::x))
                (or (consp acl2::x) (fty-info-p nil))))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-caar-when-fty-info-alist-p

(defthm symbolp-of-caar-when-fty-info-alist-p
  (implies (fty-info-alist-p acl2::x)
           (iff (symbolp (caar acl2::x))
                (or (consp acl2::x) (symbolp nil))))
  :rule-classes ((:rewrite)))

Function: fty-info-alist-fix$inline

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

Theorem: fty-info-alist-p-of-fty-info-alist-fix

(defthm fty-info-alist-p-of-fty-info-alist-fix
  (b* ((fty::newx (fty-info-alist-fix$inline x)))
    (fty-info-alist-p fty::newx))
  :rule-classes :rewrite)

Theorem: fty-info-alist-fix-when-fty-info-alist-p

(defthm fty-info-alist-fix-when-fty-info-alist-p
  (implies (fty-info-alist-p x)
           (equal (fty-info-alist-fix x) x)))

Function: fty-info-alist-equiv$inline

(defun fty-info-alist-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (fty-info-alist-p acl2::x)
                              (fty-info-alist-p acl2::y))))
  (equal (fty-info-alist-fix acl2::x)
         (fty-info-alist-fix acl2::y)))

Theorem: fty-info-alist-equiv-is-an-equivalence

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

Theorem: fty-info-alist-equiv-implies-equal-fty-info-alist-fix-1

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

Theorem: fty-info-alist-fix-under-fty-info-alist-equiv

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

Theorem: equal-of-fty-info-alist-fix-1-forward-to-fty-info-alist-equiv

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

Theorem: equal-of-fty-info-alist-fix-2-forward-to-fty-info-alist-equiv

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

Theorem: fty-info-alist-equiv-of-fty-info-alist-fix-1-forward

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

Theorem: fty-info-alist-equiv-of-fty-info-alist-fix-2-forward

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

Theorem: cons-of-symbol-fix-k-under-fty-info-alist-equiv

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

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

Theorem: cons-of-fty-info-fix-v-under-fty-info-alist-equiv

(defthm cons-of-fty-info-fix-v-under-fty-info-alist-equiv
  (fty-info-alist-equiv (cons (cons acl2::k (fty-info-fix acl2::v))
                              acl2::x)
                        (cons (cons acl2::k acl2::v) acl2::x)))

Theorem: cons-fty-info-equiv-congruence-on-v-under-fty-info-alist-equiv

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

Theorem: cons-of-fty-info-alist-fix-y-under-fty-info-alist-equiv

(defthm cons-of-fty-info-alist-fix-y-under-fty-info-alist-equiv
  (fty-info-alist-equiv (cons acl2::x (fty-info-alist-fix acl2::y))
                        (cons acl2::x acl2::y)))

Theorem: cons-fty-info-alist-equiv-congruence-on-y-under-fty-info-alist-equiv

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

Theorem: fty-info-alist-fix-of-acons

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

Theorem: fty-info-alist-fix-of-append

(defthm fty-info-alist-fix-of-append
  (equal (fty-info-alist-fix (append std::a std::b))
         (append (fty-info-alist-fix std::a)
                 (fty-info-alist-fix std::b))))

Theorem: consp-car-of-fty-info-alist-fix

(defthm consp-car-of-fty-info-alist-fix
  (equal (consp (car (fty-info-alist-fix x)))
         (consp (fty-info-alist-fix x))))

Function: make-inline

(defun make-inline (name)
  (declare (xargs :guard (symbolp name)))
  (let ((acl2::__function__ 'make-inline))
    (declare (ignorable acl2::__function__))
    (b* ((name (symbol-fix name))
         (name-str (symbol-name name))
         (pkg-str (symbol-package-name name))
         (inlined-name (concatenate 'string
                                    name-str "$INLINE")))
      (intern$ inlined-name pkg-str))))

Theorem: symbolp-of-make-inline

(defthm symbolp-of-make-inline
  (b* ((i (make-inline name)))
    (symbolp i))
  :rule-classes :rewrite)

Function: generate-field-acc

(defun generate-field-acc (name pred field acc)
  (declare (xargs :guard (and (symbolp name)
                              (symbolp pred)
                              (fty::flexprod-field-p field)
                              (fty-info-alist-p acc))))
  (let ((acl2::__function__ 'generate-field-acc))
    (declare (ignorable acl2::__function__))
    (b* ((acc (fty-info-alist-fix acc))
         ((unless (fty::flexprod-field-p field))
          acc)
         (name (symbol-fix name))
         (pred (symbol-fix pred))
         (field-acc (fty::flexprod-field->acc-name field))
         ((unless (symbolp field-acc))
          (prog2$ (er hard? 'fty=>generate-field-acc
                      "Should be a symbolp: ~q0" field-acc)
                  acc))
         (field-type (fty::flexprod-field->type field))
         ((unless (symbolp field-type))
          (prog2$ (er hard? 'fty=>generate-field-acc
                      "Should be a symbolp: ~q0" field-type)
                  acc)))
      (acons (make-inline field-acc)
             (make-fty-info :name name
                            :category :prod
                            :type :field
                            :guards (list pred)
                            :returns field-type)
             acc))))

Theorem: fty-info-alist-p-of-generate-field-acc

(defthm fty-info-alist-p-of-generate-field-acc
  (b* ((alst (generate-field-acc name pred field acc)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: generate-field-acc-lst

(defun generate-field-acc-lst (name pred fields acc)
  (declare (xargs :guard (and (symbolp name)
                              (symbolp pred)
                              (fty-info-alist-p acc))))
  (let ((acl2::__function__ 'generate-field-acc-lst))
    (declare (ignorable acl2::__function__))
    (b* ((acc (fty-info-alist-fix acc))
         ((unless (consp fields)) acc)
         ((cons first rest) fields)
         ((unless (fty::flexprod-field-p first))
          (generate-field-acc-lst name pred rest acc)))
      (generate-field-acc-lst
           name pred rest
           (generate-field-acc name pred first acc)))))

Theorem: fty-info-alist-p-of-generate-field-acc-lst

(defthm fty-info-alist-p-of-generate-field-acc-lst
  (b* ((alst (generate-field-acc-lst name pred fields acc)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: generate-field-type-lst

(defun generate-field-type-lst (fields)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'generate-field-type-lst))
    (declare (ignorable acl2::__function__))
    (b* (((unless (consp fields)) nil)
         ((cons first rest) fields)
         ((unless (fty::flexprod-field-p first))
          (generate-field-type-lst rest))
         (type (fty::flexprod-field->type first))
         ((unless (symbolp type))
          (er hard? 'fty=>generate-field-type-lst
              "Should be a symbolp: ~q0" type)))
      (cons type (generate-field-type-lst rest)))))

Theorem: symbol-listp-of-generate-field-type-lst

(defthm symbol-listp-of-generate-field-type-lst
  (b* ((g (generate-field-type-lst fields)))
    (symbol-listp g))
  :rule-classes :rewrite)

Function: generate-prod

(defun generate-prod (name pred fix prod acc)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp pred)
                             (symbolp fix)
                             (fty::flexprod-p prod)
                             (fty-info-alist-p acc))))
 (let ((acl2::__function__ 'generate-prod))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-info-alist-fix acc))
    ((unless (fty::flexprod-p prod)) acc)
    (name (symbol-fix name))
    (pred (symbol-fix pred))
    (fix (symbol-fix fix))
    (fields (fty::flexprod->fields prod))
    (acc-p (acons pred
                  (make-fty-info :name name
                                 :category :prod
                                 :type :recognizer
                                 :guards nil
                                 :returns 'booleanp)
                  acc))
    (acc-fix (acons (make-inline fix)
                    (make-fty-info :name name
                                   :category :prod
                                   :type :fix
                                   :guards (list pred)
                                   :returns pred)
                    acc-p))
    (acc-const
      (acons name
             (make-fty-info :name name
                            :category :prod
                            :type :constructor
                            :guards (generate-field-type-lst fields)
                            :returns pred)
             acc-fix)))
   (generate-field-acc-lst name pred fields acc-const))))

Theorem: fty-info-alist-p-of-generate-prod

(defthm fty-info-alist-p-of-generate-prod
  (b* ((alst (generate-prod name pred fix prod acc)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: generate-option

(defun generate-option (name pred fix prod acc)
  (declare (xargs :guard (and (symbolp name)
                              (symbolp pred)
                              (symbolp fix)
                              (fty::flexprod-p prod)
                              (fty-info-alist-p acc))))
  (let ((acl2::__function__ 'generate-option))
    (declare (ignorable acl2::__function__))
    (b* ((name (symbol-fix name))
         (pred (symbol-fix pred))
         (fix (symbol-fix fix))
         (acc (fty-info-alist-fix acc))
         ((unless (fty::flexprod-p prod)) acc)
         (fields (fty::flexprod->fields prod))
         ((unless (and (consp fields)
                       (null (cdr fields))))
          (prog2$ (er hard? 'fty=>generate-option
                      "fields incorrect for option some type: ~q0"
                      fields)
                  acc))
         (some-name (fty::flexprod->type-name prod))
         ((unless (symbolp some-name))
          (prog2$ (er hard? 'fty=>generate-option
                      "Should be a symbolp: ~q0" some-name)
                  acc))
         (field (car fields))
         ((unless (fty::flexprod-field-p field))
          (prog2$ (er hard? 'fty=>generate-option
                      "needs to be a field: ~q0" field)
                  acc))
         (accessor (fty::flexprod-field->acc-name field))
         ((unless (symbolp accessor))
          (prog2$ (er hard? 'fty=>generate-option
                      "Should be a symbolp: ~q0" accessor)
                  acc))
         (acc-type (fty::flexprod-field->type field))
         ((unless (symbolp acc-type))
          (prog2$ (er hard? 'fty=>generate-option
                      "Should be a symbolp: ~q0" acc-type)
                  acc))
         (acc-p (acons pred
                       (make-fty-info :name name
                                      :category :option
                                      :type :recognizer
                                      :guards nil
                                      :returns 'booleanp)
                       acc))
         (acc-some (acons some-name
                          (make-fty-info :name name
                                         :category :option
                                         :type :constructor
                                         :guards (list acc-type)
                                         :returns pred)
                          acc-p))
         (acc-some-val (acons (make-inline accessor)
                              (make-fty-info :name name
                                             :category :option
                                             :type :field
                                             :guards (list pred)
                                             :returns acc-type)
                              acc-some)))
      (acons (make-inline fix)
             (make-fty-info :name name
                            :category :option
                            :type :fix
                            :guards (list pred)
                            :returns pred)
             acc-some-val))))

Theorem: fty-info-alist-p-of-generate-option

(defthm fty-info-alist-p-of-generate-option
  (b* ((alst (generate-option name pred fix prod acc)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: generate-flexsum

(defun generate-flexsum (type acc)
  (declare (xargs :guard (and (fty::flexsum-p type)
                              (fty-info-alist-p acc))))
  (let ((acl2::__function__ 'generate-flexsum))
    (declare (ignorable acl2::__function__))
    (b* ((acc (fty-info-alist-fix acc))
         ((unless (fty::flexsum-p type)) acc)
         (prods (fty::flexsum->prods type))
         ((unless (consp prods))
          (prog2$ (cw "Warning: empty defprod ~q0" prods)
                  acc))
         (name (fty::flexsum->name type))
         ((unless (symbolp name))
          (prog2$ (er hard? 'fty=>generate-flexsum
                      "Should be a symbolp: ~q0" name)
                  acc))
         (pred (fty::flexsum->pred type))
         ((unless (symbolp pred))
          (prog2$ (er hard? 'fty=>generate-flexsum
                      "Should be a symbolp: ~q0" pred)
                  acc))
         (fix (fty::flexsum->fix type))
         ((unless (symbolp fix))
          (prog2$ (er hard? 'fty=>generate-flexsum
                      "Should be a symbolp: ~q0" fix)
                  acc))
         ((unless (or (equal (len prods) 1)
                      (equal (len prods) 2)))
          (prog2$ (cw "Warning: tagsum not supported ~q0"
                      prods)
                  acc)))
      (cond ((and (equal (len prods) 1)
                  (fty::flexprod-p (car prods)))
             (generate-prod name pred fix (car prods)
                            acc))
            ((and (equal (len prods) 2)
                  (fty::flexprod-p (car prods))
                  (fty::flexprod-p (cadr prods))
                  (and (equal (fty::flexprod->kind (car prods))
                              :none)
                       (equal (fty::flexprod->kind (cadr prods))
                              :some)))
             (generate-option name pred fix (cadr prods)
                              acc))
            ((and (equal (len prods) 2)
                  (fty::flexprod-p (car prods))
                  (fty::flexprod-p (cadr prods))
                  (and (equal (fty::flexprod->kind (cadr prods))
                              :none)
                       (equal (fty::flexprod->kind (car prods))
                              :some)))
             (generate-option name pred fix (car prods)
                              acc))
            (t acc)))))

Theorem: fty-info-alist-p-of-generate-flexsum

(defthm fty-info-alist-p-of-generate-flexsum
  (b* ((alst (generate-flexsum type acc)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: generate-flexlist

(defun generate-flexlist (flexlst acc)
 (declare (xargs :guard (and (fty::flexlist-p flexlst)
                             (fty-info-alist-p acc))))
 (let ((acl2::__function__ 'generate-flexlist))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-info-alist-fix acc))
    ((unless (fty::flexlist-p flexlst)) acc)
    ((unless (fty::flexlist->true-listp flexlst))
     (prog2$
      (er
       hard? 'fty=>generate-flexlist
       "Smtlink only supports ~
                             deflist that are true-listp. This one is not a ~
                             true-listp : ~q0"
       flexlst)
      acc))
    (name (fty::flexlist->name flexlst))
    ((unless (symbolp name))
     (prog2$ (er hard? 'fty=>generate-flexlist
                 "Should be a symbolp: ~q0" name)
             acc))
    (pred (fty::flexlist->pred flexlst))
    ((unless (symbolp pred))
     (prog2$ (er hard? 'fty=>generate-flexlist
                 "Should be a symbolp: ~q0" pred)
             acc))
    (fix (fty::flexlist->fix flexlst))
    ((unless (symbolp fix))
     (prog2$ (er hard? 'fty=>generate-flexlist
                 "Should be a symbolp: ~q0" fix)
             acc))
    (acc-p (acons pred
                  (make-fty-info :name name
                                 :category :list
                                 :type :recognizer
                                 :guards nil
                                 :returns 'booleanp)
                  acc)))
   (acons (make-inline fix)
          (make-fty-info :name name
                         :category :list
                         :type :fix
                         :guards (list pred)
                         :returns pred)
          acc-p))))

Theorem: fty-info-alist-p-of-generate-flexlist

(defthm fty-info-alist-p-of-generate-flexlist
  (b* ((alst (generate-flexlist flexlst acc)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: generate-flexalist

(defun generate-flexalist (flexalst acc)
 (declare (xargs :guard (and (fty::flexalist-p flexalst)
                             (fty-info-alist-p acc))))
 (let ((acl2::__function__ 'generate-flexalist))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-info-alist-fix acc))
    ((unless (fty::flexalist-p flexalst))
     acc)
    ((unless (fty::flexalist->true-listp flexalst))
     (prog2$
      (er
       hard? 'fty=>generate-flexalist
       "Smtlink only supports ~
                             deflist that are true-listp. This one is not a ~
                             true-listp : ~q0"
       flexalst)
      acc))
    (name (fty::flexalist->name flexalst))
    ((unless (symbolp name))
     (prog2$ (er hard? 'fty=>generate-flexalist
                 "Should be a symbolp: ~q0" name)
             acc))
    (pred (fty::flexalist->pred flexalst))
    ((unless (symbolp pred))
     (prog2$ (er hard? 'fty=>generate-flexalist
                 "Should be a symbolp: ~q0" pred)
             acc))
    (fix (fty::flexalist->fix flexalst))
    ((unless (symbolp fix))
     (prog2$ (er hard? 'fty=>generate-flexalist
                 "Should be a symbolp: ~q0" fix)
             acc))
    (acc-p (acons pred
                  (make-fty-info :name name
                                 :category :alist
                                 :type :recognizer
                                 :guards nil
                                 :returns 'booleanp)
                  acc)))
   (acons (make-inline fix)
          (make-fty-info :name name
                         :category :alist
                         :type :fix
                         :guards (list pred)
                         :returns pred)
          acc-p))))

Theorem: fty-info-alist-p-of-generate-flexalist

(defthm fty-info-alist-p-of-generate-flexalist
  (b* ((alst (generate-flexalist flexalst acc)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: generate-fty-info-alist-rec

(defun generate-fty-info-alist-rec (fty acc flextypes-table)
 (declare (xargs :guard (and (symbol-listp fty)
                             (fty-info-alist-p acc)
                             (alistp flextypes-table))))
 (let ((acl2::__function__ 'generate-fty-info-alist-rec))
  (declare (ignorable acl2::__function__))
  (b*
   ((fty (symbol-list-fix fty))
    (acc (fty-info-alist-fix acc))
    ((unless (consp fty)) acc)
    ((cons first rest) fty)
    (flextypes-table (acl2::alist-fix flextypes-table))
    (exist? (assoc-equal first flextypes-table))
    ((unless exist?)
     (prog2$ (cw "Warning: fty type not found ~q0" first)
             acc))
    (agg (cdr exist?))
    ((unless (fty::flextypes-p agg))
     (prog2$ (er hard? 'fty=>generate-fty-info-alist-rec
                 "Should be a flextypes, but ~
  found ~q0"
                 agg)
             acc))
    (types (fty::flextypes->types agg))
    ((if (or (atom types) (> (len types) 1)))
     (prog2$
      (er
       hard? 'fty=>generate-fty-info-alist-rec
       "Possible recursive types ~
    found, not supported in Smtlink yet.")
      acc))
    (type (car types)))
   (cond
    ((fty::flexsum-p type)
     (generate-fty-info-alist-rec rest (generate-flexsum type acc)
                                  flextypes-table))
    ((fty::flexlist-p type)
     (generate-fty-info-alist-rec rest (generate-flexlist type acc)
                                  flextypes-table))
    ((fty::flexalist-p type)
     (generate-fty-info-alist-rec rest (generate-flexalist type acc)
                                  flextypes-table))
    (t (generate-fty-info-alist-rec rest acc flextypes-table))))))

Theorem: fty-info-alist-p-of-generate-fty-info-alist-rec

(defthm fty-info-alist-p-of-generate-fty-info-alist-rec
  (b* ((alst (generate-fty-info-alist-rec fty acc flextypes-table)))
    (fty-info-alist-p alst))
  :rule-classes :rewrite)

Function: fncall-of-flextype-special

(defun fncall-of-flextype-special (fn-name)
  (declare (xargs :guard (symbolp fn-name)))
  (let ((acl2::__function__ 'fncall-of-flextype-special))
    (declare (ignorable acl2::__function__))
    (if (or (equal fn-name 'cons)
            (equal fn-name 'car)
            (equal fn-name 'cdr)
            (equal fn-name 'consp)
            (equal fn-name 'acons)
            (equal fn-name 'assoc-equal))
        t
      nil)))

Theorem: booleanp-of-fncall-of-flextype-special

(defthm booleanp-of-fncall-of-flextype-special
  (b* ((special? (fncall-of-flextype-special fn-name)))
    (booleanp special?))
  :rule-classes :rewrite)

Function: fncall-of-flextype

(defun fncall-of-flextype (fn-name fty-info)
  (declare (xargs :guard (and (symbolp fn-name)
                              (fty-info-alist-p fty-info))))
  (let ((acl2::__function__ 'fncall-of-flextype))
    (declare (ignorable acl2::__function__))
    (b* ((fn-name (symbol-fix fn-name))
         (fty-info (fty-info-alist-fix fty-info))
         (item (assoc-equal fn-name fty-info))
         ((if item) t))
      (fncall-of-flextype-special fn-name))))

Theorem: fncall-of-flextype-conclusion

(defthm fncall-of-flextype-conclusion
  (b* ((flex? (fncall-of-flextype fn-name fty-info)))
    (implies (and flex? (symbolp fn-name)
                  (fty-info-alist-p fty-info))
             (or (assoc-equal fn-name fty-info)
                 (fncall-of-flextype-special fn-name))))
  :rule-classes :rewrite)

Function: typedecl-of-flextype

(defun typedecl-of-flextype (fn-name fty-info)
  (declare (xargs :guard (and (symbolp fn-name)
                              (fty-info-alist-p fty-info))))
  (let ((acl2::__function__ 'typedecl-of-flextype))
    (declare (ignorable acl2::__function__))
    (b* ((fn-name (symbol-fix fn-name))
         (fty-info (fty-info-alist-fix fty-info))
         (item (assoc-equal fn-name fty-info))
         ((unless item) nil)
         (info (cdr item))
         (type (fty-info->type info)))
      (if (equal type :recognizer) t nil))))

Theorem: booleanp-of-typedecl-of-flextype

(defthm booleanp-of-typedecl-of-flextype
  (b* ((flex? (typedecl-of-flextype fn-name fty-info)))
    (booleanp flex?))
  :rule-classes :rewrite)

Function: fixing-of-flextype

(defun fixing-of-flextype (fn-name fty-info)
  (declare (xargs :guard (and (symbolp fn-name)
                              (fty-info-alist-p fty-info))))
  (let ((acl2::__function__ 'fixing-of-flextype))
    (declare (ignorable acl2::__function__))
    (b* ((fn-name (symbol-fix fn-name))
         (fty-info (fty-info-alist-fix fty-info))
         (item (assoc-equal fn-name fty-info))
         ((unless item) (mv nil nil))
         (info (cdr item))
         (type (fty-info->type info))
         ((unless (equal type :fix))
          (mv nil nil)))
      (mv (fty-info->name info)
          (fty-info->guards info)))))

Theorem: symbolp-of-fixing-of-flextype.fixing?

(defthm symbolp-of-fixing-of-flextype.fixing?
  (b* (((mv ?fixing? ?guards)
        (fixing-of-flextype fn-name fty-info)))
    (symbolp fixing?))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-fixing-of-flextype.guards

(defthm symbol-listp-of-fixing-of-flextype.guards
  (b* (((mv ?fixing? ?guards)
        (fixing-of-flextype fn-name fty-info)))
    (symbol-listp guards))
  :rule-classes :rewrite)

Function: fixing-of-flextype-option

(defun fixing-of-flextype-option (fn-name fty-info)
  (declare (xargs :guard (and (symbolp fn-name)
                              (fty-info-alist-p fty-info))))
  (let ((acl2::__function__ 'fixing-of-flextype-option))
    (declare (ignorable acl2::__function__))
    (b* ((fn-name (symbol-fix fn-name))
         (fty-info (fty-info-alist-fix fty-info))
         (item (assoc-equal fn-name fty-info))
         ((unless item) nil)
         (info (cdr item))
         (type (fty-info->type info))
         ((unless (equal type :fix)) nil))
      (equal (fty-info->category info)
             :option))))

Theorem: symbolp-of-fixing-of-flextype-option

(defthm symbolp-of-fixing-of-flextype-option
  (b* ((fixing? (fixing-of-flextype-option fn-name fty-info)))
    (symbolp fixing?))
  :rule-classes :rewrite)

Function: fncall-of-flextype-option

(defun fncall-of-flextype-option (fn-name fty-info)
  (declare (xargs :guard (and (symbolp fn-name)
                              (fty-info-alist-p fty-info))))
  (let ((acl2::__function__ 'fncall-of-flextype-option))
    (declare (ignorable acl2::__function__))
    (b* ((fn-name (symbol-fix fn-name))
         (fty-info (fty-info-alist-fix fty-info))
         (item (assoc-equal fn-name fty-info))
         ((unless item) nil)
         (info (cdr item)))
      (equal (fty-info->category info)
             :option))))

Theorem: booleanp-of-fncall-of-flextype-option

(defthm booleanp-of-fncall-of-flextype-option
  (b* ((option? (fncall-of-flextype-option fn-name fty-info)))
    (booleanp option?))
  :rule-classes :rewrite)

Function: fty-field-alist-p

(defun fty-field-alist-p (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-field-alist-p))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        (eq x nil)
      (and (consp (car x))
           (symbolp (caar x))
           (symbolp (cdar x))
           (fty-field-alist-p (cdr x))))))

Theorem: fty-field-alist-p-of-append

(defthm fty-field-alist-p-of-append
  (equal (fty-field-alist-p (append acl2::a acl2::b))
         (and (fty-field-alist-p (acl2::list-fix acl2::a))
              (fty-field-alist-p acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-rev

(defthm fty-field-alist-p-of-rev
  (equal (fty-field-alist-p (acl2::rev acl2::x))
         (fty-field-alist-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-list-fix

(defthm fty-field-alist-p-of-list-fix
  (implies (fty-field-alist-p acl2::x)
           (fty-field-alist-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-fty-field-alist-p-compound-recognizer

(defthm true-listp-when-fty-field-alist-p-compound-recognizer
  (implies (fty-field-alist-p acl2::x)
           (true-listp acl2::x))
  :rule-classes :compound-recognizer)

Theorem: fty-field-alist-p-when-not-consp

(defthm fty-field-alist-p-when-not-consp
  (implies (not (consp acl2::x))
           (equal (fty-field-alist-p acl2::x)
                  (not acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-cdr-when-fty-field-alist-p

(defthm fty-field-alist-p-of-cdr-when-fty-field-alist-p
  (implies (fty-field-alist-p (double-rewrite acl2::x))
           (fty-field-alist-p (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-cons

(defthm fty-field-alist-p-of-cons
  (equal (fty-field-alist-p (cons acl2::a acl2::x))
         (and (and (consp acl2::a)
                   (symbolp (car acl2::a))
                   (symbolp (cdr acl2::a)))
              (fty-field-alist-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-remove-assoc

(defthm fty-field-alist-p-of-remove-assoc
  (implies
       (fty-field-alist-p acl2::x)
       (fty-field-alist-p (remove-assoc-equal acl2::name acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-put-assoc

(defthm fty-field-alist-p-of-put-assoc
  (implies (and (fty-field-alist-p acl2::x))
           (iff (fty-field-alist-p
                     (put-assoc-equal acl2::name acl2::val acl2::x))
                (and (symbolp acl2::name)
                     (symbolp acl2::val))))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-fast-alist-clean

(defthm fty-field-alist-p-of-fast-alist-clean
  (implies (fty-field-alist-p acl2::x)
           (fty-field-alist-p (fast-alist-clean acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-hons-shrink-alist

(defthm fty-field-alist-p-of-hons-shrink-alist
  (implies (and (fty-field-alist-p acl2::x)
                (fty-field-alist-p acl2::y))
           (fty-field-alist-p (hons-shrink-alist acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: fty-field-alist-p-of-hons-acons

(defthm fty-field-alist-p-of-hons-acons
  (equal (fty-field-alist-p (hons-acons acl2::a acl2::n acl2::x))
         (and (symbolp acl2::a)
              (symbolp acl2::n)
              (fty-field-alist-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-cdr-of-hons-assoc-equal-when-fty-field-alist-p

(defthm symbolp-of-cdr-of-hons-assoc-equal-when-fty-field-alist-p
  (implies (fty-field-alist-p acl2::x)
           (iff (symbolp (cdr (hons-assoc-equal acl2::k acl2::x)))
                (or (hons-assoc-equal acl2::k acl2::x)
                    (symbolp nil))))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-fty-field-alist-p-rewrite

(defthm alistp-when-fty-field-alist-p-rewrite
  (implies (fty-field-alist-p acl2::x)
           (alistp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-fty-field-alist-p

(defthm alistp-when-fty-field-alist-p
  (implies (fty-field-alist-p acl2::x)
           (alistp acl2::x))
  :rule-classes :tau-system)

Theorem: symbolp-of-cdar-when-fty-field-alist-p

(defthm symbolp-of-cdar-when-fty-field-alist-p
  (implies (fty-field-alist-p acl2::x)
           (iff (symbolp (cdar acl2::x))
                (or (consp acl2::x) (symbolp nil))))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-caar-when-fty-field-alist-p

(defthm symbolp-of-caar-when-fty-field-alist-p
  (implies (fty-field-alist-p acl2::x)
           (iff (symbolp (caar acl2::x))
                (or (consp acl2::x) (symbolp nil))))
  :rule-classes ((:rewrite)))

Function: fty-field-alist-fix$inline

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

Theorem: fty-field-alist-p-of-fty-field-alist-fix

(defthm fty-field-alist-p-of-fty-field-alist-fix
  (b* ((fty::newx (fty-field-alist-fix$inline x)))
    (fty-field-alist-p fty::newx))
  :rule-classes :rewrite)

Theorem: fty-field-alist-fix-when-fty-field-alist-p

(defthm fty-field-alist-fix-when-fty-field-alist-p
  (implies (fty-field-alist-p x)
           (equal (fty-field-alist-fix x) x)))

Function: fty-field-alist-equiv$inline

(defun fty-field-alist-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (fty-field-alist-p acl2::x)
                              (fty-field-alist-p acl2::y))))
  (equal (fty-field-alist-fix acl2::x)
         (fty-field-alist-fix acl2::y)))

Theorem: fty-field-alist-equiv-is-an-equivalence

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

Theorem: fty-field-alist-equiv-implies-equal-fty-field-alist-fix-1

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

Theorem: fty-field-alist-fix-under-fty-field-alist-equiv

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

Theorem: equal-of-fty-field-alist-fix-1-forward-to-fty-field-alist-equiv

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

Theorem: equal-of-fty-field-alist-fix-2-forward-to-fty-field-alist-equiv

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

Theorem: fty-field-alist-equiv-of-fty-field-alist-fix-1-forward

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

Theorem: fty-field-alist-equiv-of-fty-field-alist-fix-2-forward

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

Theorem: cons-of-symbol-fix-k-under-fty-field-alist-equiv

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

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

Theorem: cons-of-symbol-fix-v-under-fty-field-alist-equiv

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

Theorem: cons-symbol-equiv-congruence-on-v-under-fty-field-alist-equiv

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

Theorem: cons-of-fty-field-alist-fix-y-under-fty-field-alist-equiv

(defthm cons-of-fty-field-alist-fix-y-under-fty-field-alist-equiv
 (fty-field-alist-equiv (cons acl2::x (fty-field-alist-fix acl2::y))
                        (cons acl2::x acl2::y)))

Theorem: cons-fty-field-alist-equiv-congruence-on-y-under-fty-field-alist-equiv

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

Theorem: fty-field-alist-fix-of-acons

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

Theorem: fty-field-alist-fix-of-append

(defthm fty-field-alist-fix-of-append
  (equal (fty-field-alist-fix (append std::a std::b))
         (append (fty-field-alist-fix std::a)
                 (fty-field-alist-fix std::b))))

Theorem: consp-car-of-fty-field-alist-fix

(defthm consp-car-of-fty-field-alist-fix
  (equal (consp (car (fty-field-alist-fix x)))
         (consp (fty-field-alist-fix x))))

Function: fty-type-p

(defun fty-type-p (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-type-p))
    (declare (ignorable acl2::__function__))
    (and (consp x)
         (cond ((or (atom x) (eq (car x) :prod))
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((fields (std::da-nth 0 (cdr x))))
                       (fty-field-alist-p fields))))
               ((eq (car x) :list)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 1)
                     (b* ((elt-type (std::da-nth 0 (cdr x))))
                       (symbolp elt-type))))
               ((eq (car x) :alist)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((key-type (std::da-nth 0 (cdr x)))
                          (val-type (std::da-nth 1 (cdr x))))
                       (and (symbolp key-type)
                            (symbolp val-type)))))
               (t (and (eq (car x) :option)
                       (and (true-listp (cdr x))
                            (eql (len (cdr x)) 1))
                       (b* ((some-type (std::da-nth 0 (cdr x))))
                         (symbolp some-type))))))))

Theorem: consp-when-fty-type-p

(defthm consp-when-fty-type-p
  (implies (fty-type-p x) (consp x))
  :rule-classes :compound-recognizer)

Function: fty-type-kind$inline

(defun fty-type-kind$inline (x)
  (declare (xargs :guard (fty-type-p x)))
  (let ((acl2::__function__ 'fty-type-kind))
    (declare (ignorable acl2::__function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :prod)) :prod)
                      ((eq (car x) :list) :list)
                      ((eq (car x) :alist) :alist)
                      (t :option))
         :exec (car x))))

Theorem: fty-type-kind-possibilities

(defthm fty-type-kind-possibilities
  (or (equal (fty-type-kind x) :prod)
      (equal (fty-type-kind x) :list)
      (equal (fty-type-kind x) :alist)
      (equal (fty-type-kind x) :option))
  :rule-classes
  ((:forward-chaining :trigger-terms ((fty-type-kind x)))))

Function: fty-type-fix$inline

(defun fty-type-fix$inline (x)
 (declare (xargs :guard (fty-type-p x)))
 (let ((acl2::__function__ 'fty-type-fix))
  (declare (ignorable acl2::__function__))
  (mbe
   :logic
   (case (fty-type-kind x)
    (:prod
        (b* ((fields (fty-field-alist-fix (std::da-nth 0 (cdr x)))))
          (cons :prod (list fields))))
    (:list (b* ((elt-type (symbol-fix (std::da-nth 0 (cdr x)))))
             (cons :list (list elt-type))))
    (:alist (b* ((key-type (symbol-fix (std::da-nth 0 (cdr x))))
                 (val-type (symbol-fix (std::da-nth 1 (cdr x)))))
              (cons :alist (list key-type val-type))))
    (:option (b* ((some-type (symbol-fix (std::da-nth 0 (cdr x)))))
               (cons :option (list some-type)))))
   :exec x)))

Theorem: fty-type-p-of-fty-type-fix

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

Theorem: fty-type-fix-when-fty-type-p

(defthm fty-type-fix-when-fty-type-p
  (implies (fty-type-p x)
           (equal (fty-type-fix x) x)))

Function: fty-type-equiv$inline

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

Theorem: fty-type-equiv-is-an-equivalence

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

Theorem: fty-type-equiv-implies-equal-fty-type-fix-1

(defthm fty-type-equiv-implies-equal-fty-type-fix-1
  (implies (fty-type-equiv acl2::x x-equiv)
           (equal (fty-type-fix acl2::x)
                  (fty-type-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: fty-type-fix-under-fty-type-equiv

(defthm fty-type-fix-under-fty-type-equiv
  (fty-type-equiv (fty-type-fix acl2::x)
                  acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-fty-type-fix-1-forward-to-fty-type-equiv

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

Theorem: equal-of-fty-type-fix-2-forward-to-fty-type-equiv

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

Theorem: fty-type-equiv-of-fty-type-fix-1-forward

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

Theorem: fty-type-equiv-of-fty-type-fix-2-forward

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

Theorem: fty-type-kind$inline-of-fty-type-fix-x

(defthm fty-type-kind$inline-of-fty-type-fix-x
  (equal (fty-type-kind$inline (fty-type-fix x))
         (fty-type-kind$inline x)))

Theorem: fty-type-kind$inline-fty-type-equiv-congruence-on-x

(defthm fty-type-kind$inline-fty-type-equiv-congruence-on-x
  (implies (fty-type-equiv x x-equiv)
           (equal (fty-type-kind$inline x)
                  (fty-type-kind$inline x-equiv)))
  :rule-classes :congruence)

Theorem: consp-of-fty-type-fix

(defthm consp-of-fty-type-fix
  (consp (fty-type-fix x))
  :rule-classes :type-prescription)

Theorem: tag-when-fty-type-p-forward

(defthm tag-when-fty-type-p-forward
  (implies (fty-type-p x)
           (equal (acl2::tag x) (fty-type-kind x)))
  :rule-classes
  ((:forward-chaining :trigger-terms ((fty-type-p x)))))

Theorem: tag-of-fty-type-fix

(defthm tag-of-fty-type-fix
  (equal (acl2::tag (fty-type-fix x))
         (fty-type-kind x)))

Function: fty-type-prod->fields$inline

(defun fty-type-prod->fields$inline (x)
  (declare (xargs :guard (fty-type-p x)))
  (declare (xargs :guard (equal (fty-type-kind x) :prod)))
  (let ((acl2::__function__ 'fty-type-prod->fields))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and (equal (fty-type-kind x) :prod)
                      x)))
           (fty-field-alist-fix (std::da-nth 0 (cdr x))))
         :exec (std::da-nth 0 (cdr x)))))

Theorem: fty-field-alist-p-of-fty-type-prod->fields

(defthm fty-field-alist-p-of-fty-type-prod->fields
  (b* ((fields (fty-type-prod->fields$inline x)))
    (fty-field-alist-p fields))
  :rule-classes :rewrite)

Theorem: fty-type-prod->fields$inline-of-fty-type-fix-x

(defthm fty-type-prod->fields$inline-of-fty-type-fix-x
  (equal (fty-type-prod->fields$inline (fty-type-fix x))
         (fty-type-prod->fields$inline x)))

Theorem: fty-type-prod->fields$inline-fty-type-equiv-congruence-on-x

(defthm fty-type-prod->fields$inline-fty-type-equiv-congruence-on-x
  (implies (fty-type-equiv x x-equiv)
           (equal (fty-type-prod->fields$inline x)
                  (fty-type-prod->fields$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fty-type-prod->fields-when-wrong-kind

(defthm fty-type-prod->fields-when-wrong-kind
  (implies (not (equal (fty-type-kind x) :prod))
           (equal (fty-type-prod->fields x)
                  (fty-field-alist-fix nil))))

Function: fty-type-prod

(defun fty-type-prod (fields)
  (declare (xargs :guard (fty-field-alist-p fields)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-type-prod))
    (declare (ignorable acl2::__function__))
    (b* ((fields (mbe :logic (fty-field-alist-fix fields)
                      :exec fields)))
      (cons :prod (list fields)))))

Theorem: return-type-of-fty-type-prod

(defthm return-type-of-fty-type-prod
  (b* ((x (fty-type-prod fields)))
    (and (fty-type-p x)
         (equal (fty-type-kind x) :prod)))
  :rule-classes :rewrite)

Theorem: fty-type-prod->fields-of-fty-type-prod

(defthm fty-type-prod->fields-of-fty-type-prod
  (equal (fty-type-prod->fields (fty-type-prod fields))
         (fty-field-alist-fix fields)))

Theorem: fty-type-prod-of-fields

(defthm fty-type-prod-of-fields
  (implies (equal (fty-type-kind x) :prod)
           (equal (fty-type-prod (fty-type-prod->fields x))
                  (fty-type-fix x))))

Theorem: fty-type-fix-when-prod

(defthm fty-type-fix-when-prod
  (implies (equal (fty-type-kind x) :prod)
           (equal (fty-type-fix x)
                  (fty-type-prod (fty-type-prod->fields x))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: equal-of-fty-type-prod

(defthm equal-of-fty-type-prod
  (equal (equal (fty-type-prod fields) x)
         (and (fty-type-p x)
              (equal (fty-type-kind x) :prod)
              (equal (fty-type-prod->fields x)
                     (fty-field-alist-fix fields)))))

Theorem: fty-type-prod-of-fty-field-alist-fix-fields

(defthm fty-type-prod-of-fty-field-alist-fix-fields
  (equal (fty-type-prod (fty-field-alist-fix fields))
         (fty-type-prod fields)))

Theorem: fty-type-prod-fty-field-alist-equiv-congruence-on-fields

(defthm fty-type-prod-fty-field-alist-equiv-congruence-on-fields
  (implies (fty-field-alist-equiv fields fields-equiv)
           (equal (fty-type-prod fields)
                  (fty-type-prod fields-equiv)))
  :rule-classes :congruence)

Function: fty-type-list->elt-type$inline

(defun fty-type-list->elt-type$inline (x)
  (declare (xargs :guard (fty-type-p x)))
  (declare (xargs :guard (equal (fty-type-kind x) :list)))
  (let ((acl2::__function__ 'fty-type-list->elt-type))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and (equal (fty-type-kind x) :list)
                      x)))
           (symbol-fix (std::da-nth 0 (cdr x))))
         :exec (std::da-nth 0 (cdr x)))))

Theorem: symbolp-of-fty-type-list->elt-type

(defthm symbolp-of-fty-type-list->elt-type
  (b* ((elt-type (fty-type-list->elt-type$inline x)))
    (symbolp elt-type))
  :rule-classes :rewrite)

Theorem: fty-type-list->elt-type$inline-of-fty-type-fix-x

(defthm fty-type-list->elt-type$inline-of-fty-type-fix-x
  (equal (fty-type-list->elt-type$inline (fty-type-fix x))
         (fty-type-list->elt-type$inline x)))

Theorem: fty-type-list->elt-type$inline-fty-type-equiv-congruence-on-x

(defthm
      fty-type-list->elt-type$inline-fty-type-equiv-congruence-on-x
  (implies (fty-type-equiv x x-equiv)
           (equal (fty-type-list->elt-type$inline x)
                  (fty-type-list->elt-type$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fty-type-list->elt-type-when-wrong-kind

(defthm fty-type-list->elt-type-when-wrong-kind
  (implies (not (equal (fty-type-kind x) :list))
           (equal (fty-type-list->elt-type x)
                  (symbol-fix nil))))

Function: fty-type-list

(defun fty-type-list (elt-type)
  (declare (xargs :guard (symbolp elt-type)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-type-list))
    (declare (ignorable acl2::__function__))
    (b* ((elt-type (mbe :logic (symbol-fix elt-type)
                        :exec elt-type)))
      (cons :list (list elt-type)))))

Theorem: return-type-of-fty-type-list

(defthm return-type-of-fty-type-list
  (b* ((x (fty-type-list elt-type)))
    (and (fty-type-p x)
         (equal (fty-type-kind x) :list)))
  :rule-classes :rewrite)

Theorem: fty-type-list->elt-type-of-fty-type-list

(defthm fty-type-list->elt-type-of-fty-type-list
  (equal (fty-type-list->elt-type (fty-type-list elt-type))
         (symbol-fix elt-type)))

Theorem: fty-type-list-of-fields

(defthm fty-type-list-of-fields
  (implies (equal (fty-type-kind x) :list)
           (equal (fty-type-list (fty-type-list->elt-type x))
                  (fty-type-fix x))))

Theorem: fty-type-fix-when-list

(defthm fty-type-fix-when-list
  (implies (equal (fty-type-kind x) :list)
           (equal (fty-type-fix x)
                  (fty-type-list (fty-type-list->elt-type x))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: equal-of-fty-type-list

(defthm equal-of-fty-type-list
  (equal (equal (fty-type-list elt-type) x)
         (and (fty-type-p x)
              (equal (fty-type-kind x) :list)
              (equal (fty-type-list->elt-type x)
                     (symbol-fix elt-type)))))

Theorem: fty-type-list-of-symbol-fix-elt-type

(defthm fty-type-list-of-symbol-fix-elt-type
  (equal (fty-type-list (symbol-fix elt-type))
         (fty-type-list elt-type)))

Theorem: fty-type-list-symbol-equiv-congruence-on-elt-type

(defthm fty-type-list-symbol-equiv-congruence-on-elt-type
  (implies (acl2::symbol-equiv elt-type elt-type-equiv)
           (equal (fty-type-list elt-type)
                  (fty-type-list elt-type-equiv)))
  :rule-classes :congruence)

Function: fty-type-alist->key-type$inline

(defun fty-type-alist->key-type$inline (x)
  (declare (xargs :guard (fty-type-p x)))
  (declare (xargs :guard (equal (fty-type-kind x) :alist)))
  (let ((acl2::__function__ 'fty-type-alist->key-type))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and (equal (fty-type-kind x) :alist)
                      x)))
           (symbol-fix (std::da-nth 0 (cdr x))))
         :exec (std::da-nth 0 (cdr x)))))

Theorem: symbolp-of-fty-type-alist->key-type

(defthm symbolp-of-fty-type-alist->key-type
  (b* ((key-type (fty-type-alist->key-type$inline x)))
    (symbolp key-type))
  :rule-classes :rewrite)

Theorem: fty-type-alist->key-type$inline-of-fty-type-fix-x

(defthm fty-type-alist->key-type$inline-of-fty-type-fix-x
  (equal (fty-type-alist->key-type$inline (fty-type-fix x))
         (fty-type-alist->key-type$inline x)))

Theorem: fty-type-alist->key-type$inline-fty-type-equiv-congruence-on-x

(defthm
     fty-type-alist->key-type$inline-fty-type-equiv-congruence-on-x
  (implies (fty-type-equiv x x-equiv)
           (equal (fty-type-alist->key-type$inline x)
                  (fty-type-alist->key-type$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fty-type-alist->key-type-when-wrong-kind

(defthm fty-type-alist->key-type-when-wrong-kind
  (implies (not (equal (fty-type-kind x) :alist))
           (equal (fty-type-alist->key-type x)
                  (symbol-fix nil))))

Function: fty-type-alist->val-type$inline

(defun fty-type-alist->val-type$inline (x)
  (declare (xargs :guard (fty-type-p x)))
  (declare (xargs :guard (equal (fty-type-kind x) :alist)))
  (let ((acl2::__function__ 'fty-type-alist->val-type))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and (equal (fty-type-kind x) :alist)
                      x)))
           (symbol-fix (std::da-nth 1 (cdr x))))
         :exec (std::da-nth 1 (cdr x)))))

Theorem: symbolp-of-fty-type-alist->val-type

(defthm symbolp-of-fty-type-alist->val-type
  (b* ((val-type (fty-type-alist->val-type$inline x)))
    (symbolp val-type))
  :rule-classes :rewrite)

Theorem: fty-type-alist->val-type$inline-of-fty-type-fix-x

(defthm fty-type-alist->val-type$inline-of-fty-type-fix-x
  (equal (fty-type-alist->val-type$inline (fty-type-fix x))
         (fty-type-alist->val-type$inline x)))

Theorem: fty-type-alist->val-type$inline-fty-type-equiv-congruence-on-x

(defthm
     fty-type-alist->val-type$inline-fty-type-equiv-congruence-on-x
  (implies (fty-type-equiv x x-equiv)
           (equal (fty-type-alist->val-type$inline x)
                  (fty-type-alist->val-type$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fty-type-alist->val-type-when-wrong-kind

(defthm fty-type-alist->val-type-when-wrong-kind
  (implies (not (equal (fty-type-kind x) :alist))
           (equal (fty-type-alist->val-type x)
                  (symbol-fix nil))))

Function: fty-type-alist

(defun fty-type-alist (key-type val-type)
  (declare (xargs :guard (and (symbolp key-type)
                              (symbolp val-type))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-type-alist))
    (declare (ignorable acl2::__function__))
    (b* ((key-type (mbe :logic (symbol-fix key-type)
                        :exec key-type))
         (val-type (mbe :logic (symbol-fix val-type)
                        :exec val-type)))
      (cons :alist (list key-type val-type)))))

Theorem: return-type-of-fty-type-alist

(defthm return-type-of-fty-type-alist
  (b* ((x (fty-type-alist key-type val-type)))
    (and (fty-type-p x)
         (equal (fty-type-kind x) :alist)))
  :rule-classes :rewrite)

Theorem: fty-type-alist->key-type-of-fty-type-alist

(defthm fty-type-alist->key-type-of-fty-type-alist
  (equal
       (fty-type-alist->key-type (fty-type-alist key-type val-type))
       (symbol-fix key-type)))

Theorem: fty-type-alist->val-type-of-fty-type-alist

(defthm fty-type-alist->val-type-of-fty-type-alist
  (equal
       (fty-type-alist->val-type (fty-type-alist key-type val-type))
       (symbol-fix val-type)))

Theorem: fty-type-alist-of-fields

(defthm fty-type-alist-of-fields
  (implies (equal (fty-type-kind x) :alist)
           (equal (fty-type-alist (fty-type-alist->key-type x)
                                  (fty-type-alist->val-type x))
                  (fty-type-fix x))))

Theorem: fty-type-fix-when-alist

(defthm fty-type-fix-when-alist
  (implies (equal (fty-type-kind x) :alist)
           (equal (fty-type-fix x)
                  (fty-type-alist (fty-type-alist->key-type x)
                                  (fty-type-alist->val-type x))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: equal-of-fty-type-alist

(defthm equal-of-fty-type-alist
  (equal (equal (fty-type-alist key-type val-type)
                x)
         (and (fty-type-p x)
              (equal (fty-type-kind x) :alist)
              (equal (fty-type-alist->key-type x)
                     (symbol-fix key-type))
              (equal (fty-type-alist->val-type x)
                     (symbol-fix val-type)))))

Theorem: fty-type-alist-of-symbol-fix-key-type

(defthm fty-type-alist-of-symbol-fix-key-type
  (equal (fty-type-alist (symbol-fix key-type)
                         val-type)
         (fty-type-alist key-type val-type)))

Theorem: fty-type-alist-symbol-equiv-congruence-on-key-type

(defthm fty-type-alist-symbol-equiv-congruence-on-key-type
  (implies (acl2::symbol-equiv key-type key-type-equiv)
           (equal (fty-type-alist key-type val-type)
                  (fty-type-alist key-type-equiv val-type)))
  :rule-classes :congruence)

Theorem: fty-type-alist-of-symbol-fix-val-type

(defthm fty-type-alist-of-symbol-fix-val-type
  (equal (fty-type-alist key-type (symbol-fix val-type))
         (fty-type-alist key-type val-type)))

Theorem: fty-type-alist-symbol-equiv-congruence-on-val-type

(defthm fty-type-alist-symbol-equiv-congruence-on-val-type
  (implies (acl2::symbol-equiv val-type val-type-equiv)
           (equal (fty-type-alist key-type val-type)
                  (fty-type-alist key-type val-type-equiv)))
  :rule-classes :congruence)

Function: fty-type-option->some-type$inline

(defun fty-type-option->some-type$inline (x)
  (declare (xargs :guard (fty-type-p x)))
  (declare (xargs :guard (equal (fty-type-kind x) :option)))
  (let ((acl2::__function__ 'fty-type-option->some-type))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and (equal (fty-type-kind x) :option)
                      x)))
           (symbol-fix (std::da-nth 0 (cdr x))))
         :exec (std::da-nth 0 (cdr x)))))

Theorem: symbolp-of-fty-type-option->some-type

(defthm symbolp-of-fty-type-option->some-type
  (b* ((some-type (fty-type-option->some-type$inline x)))
    (symbolp some-type))
  :rule-classes :rewrite)

Theorem: fty-type-option->some-type$inline-of-fty-type-fix-x

(defthm fty-type-option->some-type$inline-of-fty-type-fix-x
  (equal (fty-type-option->some-type$inline (fty-type-fix x))
         (fty-type-option->some-type$inline x)))

Theorem: fty-type-option->some-type$inline-fty-type-equiv-congruence-on-x

(defthm
   fty-type-option->some-type$inline-fty-type-equiv-congruence-on-x
  (implies (fty-type-equiv x x-equiv)
           (equal (fty-type-option->some-type$inline x)
                  (fty-type-option->some-type$inline x-equiv)))
  :rule-classes :congruence)

Theorem: fty-type-option->some-type-when-wrong-kind

(defthm fty-type-option->some-type-when-wrong-kind
  (implies (not (equal (fty-type-kind x) :option))
           (equal (fty-type-option->some-type x)
                  (symbol-fix nil))))

Function: fty-type-option

(defun fty-type-option (some-type)
  (declare (xargs :guard (symbolp some-type)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-type-option))
    (declare (ignorable acl2::__function__))
    (b* ((some-type (mbe :logic (symbol-fix some-type)
                         :exec some-type)))
      (cons :option (list some-type)))))

Theorem: return-type-of-fty-type-option

(defthm return-type-of-fty-type-option
  (b* ((x (fty-type-option some-type)))
    (and (fty-type-p x)
         (equal (fty-type-kind x) :option)))
  :rule-classes :rewrite)

Theorem: fty-type-option->some-type-of-fty-type-option

(defthm fty-type-option->some-type-of-fty-type-option
  (equal (fty-type-option->some-type (fty-type-option some-type))
         (symbol-fix some-type)))

Theorem: fty-type-option-of-fields

(defthm fty-type-option-of-fields
  (implies (equal (fty-type-kind x) :option)
           (equal (fty-type-option (fty-type-option->some-type x))
                  (fty-type-fix x))))

Theorem: fty-type-fix-when-option

(defthm fty-type-fix-when-option
  (implies (equal (fty-type-kind x) :option)
           (equal (fty-type-fix x)
                  (fty-type-option (fty-type-option->some-type x))))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: equal-of-fty-type-option

(defthm equal-of-fty-type-option
  (equal (equal (fty-type-option some-type) x)
         (and (fty-type-p x)
              (equal (fty-type-kind x) :option)
              (equal (fty-type-option->some-type x)
                     (symbol-fix some-type)))))

Theorem: fty-type-option-of-symbol-fix-some-type

(defthm fty-type-option-of-symbol-fix-some-type
  (equal (fty-type-option (symbol-fix some-type))
         (fty-type-option some-type)))

Theorem: fty-type-option-symbol-equiv-congruence-on-some-type

(defthm fty-type-option-symbol-equiv-congruence-on-some-type
  (implies (acl2::symbol-equiv some-type some-type-equiv)
           (equal (fty-type-option some-type)
                  (fty-type-option some-type-equiv)))
  :rule-classes :congruence)

Theorem: fty-type-fix-redef

(defthm fty-type-fix-redef
 (equal
      (fty-type-fix x)
      (case (fty-type-kind x)
        (:prod (fty-type-prod (fty-type-prod->fields x)))
        (:list (fty-type-list (fty-type-list->elt-type x)))
        (:alist (fty-type-alist (fty-type-alist->key-type x)
                                (fty-type-alist->val-type x)))
        (:option (fty-type-option (fty-type-option->some-type x)))))
 :rule-classes :definition)

Function: fty-types-p

(defun fty-types-p (x)
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-types-p))
    (declare (ignorable acl2::__function__))
    (if (atom x)
        (eq x nil)
      (and (consp (car x))
           (symbolp (caar x))
           (fty-type-p (cdar x))
           (fty-types-p (cdr x))))))

Theorem: fty-types-p-of-append

(defthm fty-types-p-of-append
  (equal (fty-types-p (append acl2::a acl2::b))
         (and (fty-types-p (acl2::list-fix acl2::a))
              (fty-types-p acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-rev

(defthm fty-types-p-of-rev
  (equal (fty-types-p (acl2::rev acl2::x))
         (fty-types-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-list-fix

(defthm fty-types-p-of-list-fix
  (implies (fty-types-p acl2::x)
           (fty-types-p (acl2::list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: true-listp-when-fty-types-p-compound-recognizer

(defthm true-listp-when-fty-types-p-compound-recognizer
  (implies (fty-types-p acl2::x)
           (true-listp acl2::x))
  :rule-classes :compound-recognizer)

Theorem: fty-types-p-when-not-consp

(defthm fty-types-p-when-not-consp
  (implies (not (consp acl2::x))
           (equal (fty-types-p acl2::x)
                  (not acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-cdr-when-fty-types-p

(defthm fty-types-p-of-cdr-when-fty-types-p
  (implies (fty-types-p (double-rewrite acl2::x))
           (fty-types-p (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-cons

(defthm fty-types-p-of-cons
  (equal (fty-types-p (cons acl2::a acl2::x))
         (and (and (consp acl2::a)
                   (symbolp (car acl2::a))
                   (fty-type-p (cdr acl2::a)))
              (fty-types-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-remove-assoc

(defthm fty-types-p-of-remove-assoc
  (implies (fty-types-p acl2::x)
           (fty-types-p (remove-assoc-equal acl2::name acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-put-assoc

(defthm fty-types-p-of-put-assoc
 (implies
   (and (fty-types-p acl2::x))
   (iff (fty-types-p (put-assoc-equal acl2::name acl2::val acl2::x))
        (and (symbolp acl2::name)
             (fty-type-p acl2::val))))
 :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-fast-alist-clean

(defthm fty-types-p-of-fast-alist-clean
  (implies (fty-types-p acl2::x)
           (fty-types-p (fast-alist-clean acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-hons-shrink-alist

(defthm fty-types-p-of-hons-shrink-alist
  (implies (and (fty-types-p acl2::x)
                (fty-types-p acl2::y))
           (fty-types-p (hons-shrink-alist acl2::x acl2::y)))
  :rule-classes ((:rewrite)))

Theorem: fty-types-p-of-hons-acons

(defthm fty-types-p-of-hons-acons
  (equal (fty-types-p (hons-acons acl2::a acl2::n acl2::x))
         (and (symbolp acl2::a)
              (fty-type-p acl2::n)
              (fty-types-p acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: fty-type-p-of-cdr-of-hons-assoc-equal-when-fty-types-p

(defthm fty-type-p-of-cdr-of-hons-assoc-equal-when-fty-types-p
 (implies (fty-types-p acl2::x)
          (iff (fty-type-p (cdr (hons-assoc-equal acl2::k acl2::x)))
               (or (hons-assoc-equal acl2::k acl2::x)
                   (fty-type-p nil))))
 :rule-classes ((:rewrite)))

Theorem: alistp-when-fty-types-p-rewrite

(defthm alistp-when-fty-types-p-rewrite
  (implies (fty-types-p acl2::x)
           (alistp acl2::x))
  :rule-classes ((:rewrite)))

Theorem: alistp-when-fty-types-p

(defthm alistp-when-fty-types-p
  (implies (fty-types-p acl2::x)
           (alistp acl2::x))
  :rule-classes :tau-system)

Theorem: fty-type-p-of-cdar-when-fty-types-p

(defthm fty-type-p-of-cdar-when-fty-types-p
  (implies (fty-types-p acl2::x)
           (iff (fty-type-p (cdar acl2::x))
                (or (consp acl2::x) (fty-type-p nil))))
  :rule-classes ((:rewrite)))

Theorem: symbolp-of-caar-when-fty-types-p

(defthm symbolp-of-caar-when-fty-types-p
  (implies (fty-types-p acl2::x)
           (iff (symbolp (caar acl2::x))
                (or (consp acl2::x) (symbolp nil))))
  :rule-classes ((:rewrite)))

Function: fty-types-fix$inline

(defun fty-types-fix$inline (x)
  (declare (xargs :guard (fty-types-p x)))
  (let ((acl2::__function__ 'fty-types-fix))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (if (atom x)
             nil
           (if (consp (car x))
               (cons (cons (symbol-fix (caar x))
                           (fty-type-fix (cdar x)))
                     (fty-types-fix (cdr x)))
             (fty-types-fix (cdr x))))
         :exec x)))

Theorem: fty-types-p-of-fty-types-fix

(defthm fty-types-p-of-fty-types-fix
  (b* ((fty::newx (fty-types-fix$inline x)))
    (fty-types-p fty::newx))
  :rule-classes :rewrite)

Theorem: fty-types-fix-when-fty-types-p

(defthm fty-types-fix-when-fty-types-p
  (implies (fty-types-p x)
           (equal (fty-types-fix x) x)))

Function: fty-types-equiv$inline

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

Theorem: fty-types-equiv-is-an-equivalence

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

Theorem: fty-types-equiv-implies-equal-fty-types-fix-1

(defthm fty-types-equiv-implies-equal-fty-types-fix-1
  (implies (fty-types-equiv acl2::x x-equiv)
           (equal (fty-types-fix acl2::x)
                  (fty-types-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: fty-types-fix-under-fty-types-equiv

(defthm fty-types-fix-under-fty-types-equiv
  (fty-types-equiv (fty-types-fix acl2::x)
                   acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-fty-types-fix-1-forward-to-fty-types-equiv

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

Theorem: equal-of-fty-types-fix-2-forward-to-fty-types-equiv

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

Theorem: fty-types-equiv-of-fty-types-fix-1-forward

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

Theorem: fty-types-equiv-of-fty-types-fix-2-forward

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

Theorem: cons-of-symbol-fix-k-under-fty-types-equiv

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

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

Theorem: cons-of-fty-type-fix-v-under-fty-types-equiv

(defthm cons-of-fty-type-fix-v-under-fty-types-equiv
  (fty-types-equiv (cons (cons acl2::k (fty-type-fix acl2::v))
                         acl2::x)
                   (cons (cons acl2::k acl2::v) acl2::x)))

Theorem: cons-fty-type-equiv-congruence-on-v-under-fty-types-equiv

(defthm cons-fty-type-equiv-congruence-on-v-under-fty-types-equiv
  (implies (fty-type-equiv acl2::v v-equiv)
           (fty-types-equiv (cons (cons acl2::k acl2::v) acl2::x)
                            (cons (cons acl2::k v-equiv) acl2::x)))
  :rule-classes :congruence)

Theorem: cons-of-fty-types-fix-y-under-fty-types-equiv

(defthm cons-of-fty-types-fix-y-under-fty-types-equiv
  (fty-types-equiv (cons acl2::x (fty-types-fix acl2::y))
                   (cons acl2::x acl2::y)))

Theorem: cons-fty-types-equiv-congruence-on-y-under-fty-types-equiv

(defthm cons-fty-types-equiv-congruence-on-y-under-fty-types-equiv
  (implies (fty-types-equiv acl2::y y-equiv)
           (fty-types-equiv (cons acl2::x acl2::y)
                            (cons acl2::x y-equiv)))
  :rule-classes :congruence)

Theorem: fty-types-fix-of-acons

(defthm fty-types-fix-of-acons
  (equal (fty-types-fix (cons (cons acl2::a acl2::b) x))
         (cons (cons (symbol-fix acl2::a)
                     (fty-type-fix acl2::b))
               (fty-types-fix x))))

Theorem: fty-types-fix-of-append

(defthm fty-types-fix-of-append
  (equal (fty-types-fix (append std::a std::b))
         (append (fty-types-fix std::a)
                 (fty-types-fix std::b))))

Theorem: consp-car-of-fty-types-fix

(defthm consp-car-of-fty-types-fix
  (equal (consp (car (fty-types-fix x)))
         (consp (fty-types-fix x))))

Function: generate-type-measure

(defun generate-type-measure (fty-info acc)
  (declare (xargs :guard (and (fty-info-alist-p fty-info)
                              (fty-types-p acc))))
  (let ((acl2::__function__ 'generate-type-measure))
    (declare (ignorable acl2::__function__))
    (b* ((fty-info (fty-info-alist-fix fty-info))
         (acc (fty-types-fix acc))
         (measure (- (len fty-info) (len acc))))
      (if (<= measure 0) 0 measure))))

Theorem: natp-of-generate-type-measure

(defthm natp-of-generate-type-measure
  (b* ((m (generate-type-measure fty-info acc)))
    (natp m))
  :rule-classes :rewrite)

Theorem: generate-type-measure-with-fty-types-fix

(defthm generate-type-measure-with-fty-types-fix
  (b* ((m (generate-type-measure fty-info acc)))
    (equal (generate-type-measure fty-info (fty-types-fix acc))
           m))
  :rule-classes :rewrite)

Theorem: generate-type-measure-increase-prod

(defthm generate-type-measure-increase-prod
 (b* ((m (generate-type-measure fty-info acc)))
  (implies
    (and (not (equal m 0)))
    (< (generate-type-measure fty-info
                              (acons name prod (fty-types-fix acc)))
       m)))
 :rule-classes :rewrite)

Theorem: generate-type-measure-increase-option

(defthm generate-type-measure-increase-option
 (b* ((m (generate-type-measure fty-info acc)))
  (implies
   (and (not (equal m 0)))
   (<
     (generate-type-measure fty-info
                            (acons name option (fty-types-fix acc)))
     m)))
 :rule-classes :rewrite)

Theorem: generate-type-measure-increase-list

(defthm generate-type-measure-increase-list
 (b* ((m (generate-type-measure fty-info acc)))
  (implies
    (and (not (equal m 0)))
    (< (generate-type-measure fty-info
                              (acons name list (fty-types-fix acc)))
       m)))
 :rule-classes :rewrite)

Theorem: generate-type-measure-increase-alist

(defthm generate-type-measure-increase-alist
 (b* ((m (generate-type-measure fty-info acc)))
  (implies
   (and (not (equal m 0)))
   (< (generate-type-measure fty-info
                             (acons name alist (fty-types-fix acc)))
      m)))
 :rule-classes :rewrite)

Function: smt-types

(defun smt-types nil
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'smt-types))
    (declare (ignorable acl2::__function__))
    *smt-types*))

Theorem: alistp-of-smt-types

(defthm alistp-of-smt-types
  (b* ((smt-types (smt-types)))
    (alistp smt-types))
  :rule-classes :rewrite)

Function: generate-fty-field-alist

(defun generate-fty-field-alist (fields fty-info)
 (declare (xargs :guard (fty-info-alist-p fty-info)))
 (let ((acl2::__function__ 'generate-fty-field-alist))
  (declare (ignorable acl2::__function__))
  (b*
   ((fty-info (fty-info-alist-fix fty-info))
    ((unless (consp fields)) (mv nil nil))
    ((cons first rest) fields)
    ((unless (fty::flexprod-field-p first))
     (prog2$ (er hard? 'fty=>generate-fty-field-alist
                 "Should be a field: ~q0" first)
             (mv nil nil)))
    (name (fty::flexprod-field->name first))
    ((unless (symbolp name))
     (prog2$ (er hard? 'fty=>generate-fty-field-alist
                 "Should be a symbolp: ~q0" name)
             (mv nil nil)))
    (type (fty::flexprod-field->type first))
    ((unless (symbolp type))
     (prog2$ (er hard? 'fty=>generate-fty-field-alist
                 "Should be a symbolp: ~q0" type)
             (mv nil nil)))
    ((mv cdr-type-lst cdr-field-alst)
     (generate-fty-field-alist rest fty-info))
    (basic? (assoc-equal type (smt-types)))
    ((if basic?)
     (mv (cons type cdr-type-lst)
         (acons name type cdr-field-alst)))
    (info (assoc-equal type fty-info))
    ((unless info)
     (prog2$
      (er
       hard? 'fty=>generate-fty-field-alist
       "type ~p0 doesn't ~
                                 exist~%"
       type)
      (mv nil nil)))
    (type-name (fty-info->name (cdr info))))
   (mv (cons type-name cdr-type-lst)
       (acons name type-name cdr-field-alst)))))

Theorem: symbol-listp-of-generate-fty-field-alist.type-lst

(defthm symbol-listp-of-generate-fty-field-alist.type-lst
  (b* (((mv ?type-lst ?field-alst)
        (generate-fty-field-alist fields fty-info)))
    (symbol-listp type-lst))
  :rule-classes :rewrite)

Theorem: fty-field-alist-p-of-generate-fty-field-alist.field-alst

(defthm fty-field-alist-p-of-generate-fty-field-alist.field-alst
  (b* (((mv ?type-lst ?field-alst)
        (generate-fty-field-alist fields fty-info)))
    (fty-field-alist-p field-alst))
  :rule-classes :rewrite)

Function: generate-flexprod-type

(defun generate-flexprod-type (name prod flextypes-table
                                    fty-info acc ordered-acc)
 (declare (xargs :guard (and (symbolp name)
                             (fty::flexprod-p prod)
                             (alistp flextypes-table)
                             (fty-info-alist-p fty-info)
                             (fty-types-p acc)
                             (fty-types-p ordered-acc))))
 (let ((acl2::__function__ 'generate-flexprod-type))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-types-fix acc))
    (ordered-acc (fty-types-fix ordered-acc))
    (name (symbol-fix name))
    ((if (equal (generate-type-measure fty-info acc)
                0))
     (prog2$
      (er
       hard? 'fty=>generate-flexprod-type
       "accumulator exceeding
                                length of all fty functions.~%")
      (mv acc ordered-acc)))
    ((if (assoc-equal name acc))
     (mv acc ordered-acc))
    ((unless (fty::flexprod-p prod))
     (mv acc ordered-acc))
    (fields (fty::flexprod->fields prod))
    ((mv type-lst field-alst)
     (generate-fty-field-alist fields fty-info))
    (new-prod (make-fty-type-prod :fields field-alst))
    (new-acc-1 (acons name new-prod acc))
    ((mv new-acc-2 updated-ordered-acc)
     (generate-fty-type-list type-lst flextypes-table
                             fty-info new-acc-1 ordered-acc)))
   (mv new-acc-2
       (acons name new-prod updated-ordered-acc)))))

Function: generate-flexoption-type

(defun generate-flexoption-type (name option flextypes-table
                                      fty-info acc ordered-acc)
 (declare (xargs :guard (and (symbolp name)
                             (fty::flexprod-p option)
                             (alistp flextypes-table)
                             (fty-info-alist-p fty-info)
                             (fty-types-p acc)
                             (fty-types-p ordered-acc))))
 (let ((acl2::__function__ 'generate-flexoption-type))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-types-fix acc))
    (ordered-acc (fty-types-fix ordered-acc))
    (name (symbol-fix name))
    ((if (equal (generate-type-measure fty-info acc)
                0))
     (prog2$
      (er
       hard? 'fty=>generate-flexprod-type
       "accumulator exceeding
                                length of all fty functions.~%")
      (mv acc ordered-acc)))
    ((if (assoc-equal name acc))
     (mv acc ordered-acc))
    ((unless (fty::flexprod-p option))
     (mv acc ordered-acc))
    (fields (fty::flexprod->fields option))
    ((unless (and (consp fields)
                  (null (cdr fields))))
     (prog2$
      (er
       hard? 'fty=>generate-flexoption-type
       "A flexoption type ~
                                  with more than one field?: ~q0"
       fields)
      (mv acc ordered-acc)))
    (first (car fields))
    ((unless (fty::flexprod-field-p first))
     (prog2$
      (er
       hard? 'fty=>generate-flexoption-type
       "Found a none field
                                  type in a flexprod :field field: ~q0"
       first)
      (mv acc ordered-acc)))
    (some-type (fty::flexprod-field->type first))
    ((unless (symbolp some-type))
     (prog2$ (er hard? 'fty=>generate-flexoption-type
                 "Must be a symbol ~q0" some-type)
             (mv acc ordered-acc)))
    (basic? (assoc-equal some-type (smt-types)))
    ((if basic?)
     (mv (acons name
                (make-fty-type-option :some-type some-type)
                acc)
         (acons name
                (make-fty-type-option :some-type some-type)
                ordered-acc)))
    (some-info (assoc-equal some-type fty-info))
    ((unless some-info)
     (prog2$
      (er
       hard? 'fty=>generate-flexoption-type
       "some-type ~p0 doesn't ~
                                 exist~%"
       some-type)
      (mv acc ordered-acc)))
    (some-name (fty-info->name (cdr some-info)))
    (new-option (make-fty-type-option :some-type some-name))
    (new-acc-1 (acons name new-option acc))
    ((mv new-acc-2 new-ordered-acc)
     (generate-fty-type some-name flextypes-table
                        fty-info new-acc-1 ordered-acc)))
   (mv new-acc-2
       (acons name new-option new-ordered-acc)))))

Function: generate-flexsum-type

(defun generate-flexsum-type (flexsum flextypes-table
                                      fty-info acc ordered-acc)
  (declare (xargs :guard (and (fty::flexsum-p flexsum)
                              (alistp flextypes-table)
                              (fty-info-alist-p fty-info)
                              (fty-types-p acc)
                              (fty-types-p ordered-acc))))
  (let ((acl2::__function__ 'generate-flexsum-type))
    (declare (ignorable acl2::__function__))
    (b* ((acc (fty-types-fix acc))
         (ordered-acc (fty-types-fix ordered-acc))
         ((unless (fty::flexsum-p flexsum))
          (mv acc ordered-acc))
         (prods (fty::flexsum->prods flexsum))
         ((unless (consp prods))
          (prog2$ (cw "Warning: empty defprod ~q0" prods)
                  (mv acc ordered-acc)))
         (name (fty::flexsum->name flexsum))
         ((unless (symbolp name))
          (prog2$ (er hard? 'fty=>generate-flexsum-type
                      "Should be a symbolp: ~q0" name)
                  (mv acc ordered-acc)))
         ((unless (or (equal (len prods) 1)
                      (equal (len prods) 2)))
          (prog2$ (cw "Warning: tagsum not supported ~q0"
                      prods)
                  (mv acc ordered-acc))))
      (cond ((and (equal (len prods) 1)
                  (fty::flexprod-p (car prods)))
             (generate-flexprod-type name (car prods)
                                     flextypes-table
                                     fty-info acc ordered-acc))
            ((and (equal (len prods) 2)
                  (fty::flexprod-p (car prods))
                  (fty::flexprod-p (cadr prods))
                  (and (equal (fty::flexprod->kind (car prods))
                              :none)
                       (equal (fty::flexprod->kind (cadr prods))
                              :some)))
             (generate-flexoption-type name (cadr prods)
                                       flextypes-table
                                       fty-info acc ordered-acc))
            ((and (equal (len prods) 2)
                  (fty::flexprod-p (car prods))
                  (fty::flexprod-p (cadr prods))
                  (and (equal (fty::flexprod->kind (cadr prods))
                              :none)
                       (equal (fty::flexprod->kind (car prods))
                              :some)))
             (generate-flexoption-type name (car prods)
                                       flextypes-table
                                       fty-info acc ordered-acc))
            (t (mv acc ordered-acc))))))

Function: generate-flexalist-type

(defun generate-flexalist-type (flexalst flextypes-table
                                         fty-info acc ordered-acc)
 (declare (xargs :guard (and (fty::flexalist-p flexalst)
                             (alistp flextypes-table)
                             (fty-info-alist-p fty-info)
                             (fty-types-p acc)
                             (fty-types-p ordered-acc))))
 (let ((acl2::__function__ 'generate-flexalist-type))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-types-fix acc))
    (ordered-acc (fty-types-fix ordered-acc))
    ((if (equal (generate-type-measure fty-info acc)
                0))
     (prog2$
      (er
       hard? 'fty=>generate-flexprod-type
       "accumulator exceeding
                                length of all fty functions.~%")
      (mv acc ordered-acc)))
    ((unless (fty::flexalist-p flexalst))
     (mv acc ordered-acc))
    (name (fty::flexalist->name flexalst))
    ((unless (symbolp name))
     (prog2$ (er hard? 'fty=>generate-flexalist-type
                 "Should be a symbolp: ~q0" name)
             (mv acc ordered-acc)))
    ((if (assoc-equal name acc))
     (mv acc ordered-acc))
    (key-type (fty::flexalist->key-type flexalst))
    ((unless (symbolp key-type))
     (prog2$ (er hard? 'fty=>generate-flexalist-type
                 "Should be a symbolp: ~q0" key-type)
             (mv acc ordered-acc)))
    (val-type (fty::flexalist->val-type flexalst))
    ((unless (symbolp val-type))
     (prog2$ (er hard? 'fty=>generate-flexalist-type
                 "Should be a symbolp: ~q0" val-type)
             (mv acc ordered-acc)))
    (basic-key? (assoc-equal key-type (smt-types)))
    (basic-val? (assoc-equal val-type (smt-types)))
    (key-info (assoc-equal key-type fty-info))
    (val-info (assoc-equal val-type fty-info)))
   (cond
    ((and basic-key? basic-val?)
     (mv (acons name
                (make-fty-type-alist :key-type key-type
                                     :val-type val-type)
                acc)
         (acons name
                (make-fty-type-alist :key-type key-type
                                     :val-type val-type)
                ordered-acc)))
    ((and basic-key? val-info)
     (b* ((val-name (fty-info->name (cdr val-info)))
          (new-alist (make-fty-type-alist :key-type key-type
                                          :val-type val-name))
          (new-acc-1 (acons name new-alist acc))
          ((mv new-acc-2 new-ordered-acc)
           (generate-fty-type val-name flextypes-table
                              fty-info new-acc-1 ordered-acc)))
       (mv new-acc-2
           (acons name new-alist new-ordered-acc))))
    ((and basic-val? key-info)
     (b* ((key-name (fty-info->name (cdr key-info)))
          (new-alist (make-fty-type-alist :key-type key-name
                                          :val-type val-type))
          (new-acc-1 (acons name new-alist acc))
          ((mv new-acc-2 new-ordered-acc)
           (generate-fty-type key-name flextypes-table
                              fty-info new-acc-1 ordered-acc)))
       (mv new-acc-2
           (acons name new-alist new-ordered-acc))))
    ((and key-info val-info)
     (b*
      ((val-name (fty-info->name (cdr val-info)))
       (key-name (fty-info->name (cdr key-info)))
       (new-alist (make-fty-type-alist :key-type key-name
                                       :val-type val-name))
       (new-acc (acons name new-alist acc))
       ((mv new-acc-1 new-ordered-acc-1)
        (generate-fty-type key-name flextypes-table
                           fty-info new-acc ordered-acc))
       (new-acc-1
            (mbe :logic
                 (if (o<= (generate-type-measure fty-info new-acc-1)
                          (generate-type-measure fty-info new-acc))
                     new-acc-1
                   nil)
                 :exec new-acc-1))
       ((if (null new-acc-1))
        (mv new-acc new-ordered-acc-1))
       ((mv new-acc-2 new-ordered-acc-2)
        (generate-fty-type val-name flextypes-table
                           fty-info new-acc-1 new-ordered-acc-1)))
      (mv new-acc-2
          (acons name new-alist new-ordered-acc-2))))
    (t
     (prog2$
      (er
       hard? 'fty=>generate-flexalist-type
       "key-type ~p0 ~
                             and val-type ~p1 doesn't exist~%"
       key-type val-type)
      (mv acc ordered-acc)))))))

Function: generate-flexlist-type

(defun generate-flexlist-type (flexlst flextypes-table
                                       fty-info acc ordered-acc)
 (declare (xargs :guard (and (fty::flexlist-p flexlst)
                             (alistp flextypes-table)
                             (fty-info-alist-p fty-info)
                             (fty-types-p acc)
                             (fty-types-p ordered-acc))))
 (let ((acl2::__function__ 'generate-flexlist-type))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-types-fix acc))
    (ordered-acc (fty-types-fix ordered-acc))
    ((if (equal (generate-type-measure fty-info acc)
                0))
     (prog2$
      (er
       hard? 'fty=>generate-flexprod-type
       "accumulator exceeding ~
                                length of all fty functions.~%")
      (mv acc ordered-acc)))
    ((unless (fty::flexlist-p flexlst))
     (mv acc ordered-acc))
    (name (fty::flexlist->name flexlst))
    ((unless (symbolp name))
     (prog2$
      (er
       hard? 'fty=>generate-flexlist-type
       "Name should be a symbol ~
                                ~q0"
       name)
      (mv acc ordered-acc)))
    ((if (assoc-equal name acc))
     (mv acc ordered-acc))
    (true-listp? (fty::flexlist->true-listp flexlst))
    ((unless true-listp?)
     (prog2$
      (er
       hard? 'fty=>generate-flexlist-type
       "Smtlink can't handle ~
                                lists that are not true-listp yet due to ~
                                soundness concerns: ~q0"
       name)
      (mv acc ordered-acc)))
    (elt-type (fty::flexlist->elt-type flexlst))
    ((unless (symbolp elt-type))
     (prog2$ (er hard? 'fty=>generate-flexlist-type
                 "Should be a symbolp: ~q0" elt-type)
             (mv acc ordered-acc)))
    (basic? (assoc-equal elt-type (smt-types)))
    ((if basic?)
     (mv (acons name
                (make-fty-type-list :elt-type elt-type)
                acc)
         (acons name
                (make-fty-type-list :elt-type elt-type)
                ordered-acc)))
    (info (assoc-equal elt-type fty-info))
    ((unless info)
     (prog2$
      (er
       hard? 'fty=>generate-flexlist-type
       "elt-type ~p0 doesn't ~
                                exist in fty-info~%"
       elt-type)
      (mv acc ordered-acc)))
    (elt-name (fty-info->name (cdr info)))
    (new-list (make-fty-type-list :elt-type elt-name))
    (new-acc-1 (acons name new-list acc))
    ((mv new-acc-2 new-ordered-acc)
     (generate-fty-type elt-name flextypes-table
                        fty-info new-acc-1 ordered-acc)))
   (mv new-acc-2
       (acons name new-list new-ordered-acc)))))

Function: generate-fty-type

(defun generate-fty-type (name flextypes-table
                               fty-info acc ordered-acc)
 (declare (xargs :guard (and (symbolp name)
                             (alistp flextypes-table)
                             (fty-info-alist-p fty-info)
                             (fty-types-p acc)
                             (fty-types-p ordered-acc))))
 (let ((acl2::__function__ 'generate-fty-type))
  (declare (ignorable acl2::__function__))
  (b*
   ((acc (fty-types-fix acc))
    (ordered-acc (fty-types-fix ordered-acc))
    ((unless (alistp flextypes-table))
     (prog2$
      (er
       hard? 'fty=>generate-fty-type
       "flextypes-table is not an ~
                           alist?~%")
      (mv acc ordered-acc)))
    (exist? (assoc-equal name flextypes-table))
    ((unless exist?)
     (prog2$
      (er
       hard? 'fty=>generate-fty-type
       "Found a type that's ~
                                  not basic and not fty: ~q0"
       name)
      (mv acc ordered-acc)))
    (agg (cdr exist?))
    ((unless (fty::flextypes-p agg))
     (prog2$
      (er
       hard? 'fty=>generate-fty-type
       "Should be a flextypes, but ~
                       found ~q0"
       agg)
      (mv acc ordered-acc)))
    (types (fty::flextypes->types agg))
    ((if (or (not (true-listp types))
             (atom types)
             (not (null (cdr types)))))
     (prog2$
      (er
       hard? 'fty=>generate-fty-type
       "Possible recursive types ~
                      found, not supported in Smtlink yet.~%")
      (mv acc ordered-acc)))
    (type (car types)))
   (cond ((fty::flexsum-p type)
          (generate-flexsum-type type flextypes-table
                                 fty-info acc ordered-acc))
         ((fty::flexlist-p type)
          (generate-flexlist-type type flextypes-table
                                  fty-info acc ordered-acc))
         ((fty::flexalist-p type)
          (generate-flexalist-type type flextypes-table
                                   fty-info acc ordered-acc))
         (t (mv acc ordered-acc))))))

Function: generate-fty-type-list

(defun generate-fty-type-list (name-lst flextypes-table
                                        fty-info acc ordered-acc)
 (declare (xargs :guard (and (symbol-listp name-lst)
                             (alistp flextypes-table)
                             (fty-info-alist-p fty-info)
                             (fty-types-p acc)
                             (fty-types-p ordered-acc))))
 (let ((acl2::__function__ 'generate-fty-type-list))
   (declare (ignorable acl2::__function__))
   (b*
    ((name-lst (symbol-list-fix name-lst))
     (acc (fty-types-fix acc))
     (ordered-acc (fty-types-fix ordered-acc))
     ((unless (consp name-lst))
      (mv acc ordered-acc))
     ((cons first rest) name-lst)
     (basic? (assoc-equal first (smt-types)))
     ((if basic?)
      (generate-fty-type-list rest flextypes-table
                              fty-info acc ordered-acc))
     ((mv new-acc new-ordered-acc)
      (generate-fty-type first flextypes-table
                         fty-info acc ordered-acc))
     (new-acc (mbe :logic
                   (if (o<= (generate-type-measure fty-info new-acc)
                            (generate-type-measure fty-info acc))
                       new-acc
                     nil)
                   :exec new-acc))
     ((if (null new-acc))
      (mv acc new-ordered-acc)))
    (generate-fty-type-list rest flextypes-table
                            fty-info new-acc new-ordered-acc))))

Function: generate-fty-types-mutual-flag

(defun generate-fty-types-mutual-flag
       (flag prod option flexsum flexalst
             flexlst name name-lst flextypes-table
             fty-info acc ordered-acc)
 (declare (xargs :non-executable t))
 (declare (ignorable prod option flexsum flexalst
                     flexlst name name-lst flextypes-table
                     fty-info acc ordered-acc))
 (prog2$
  (acl2::throw-nonexec-error
       'generate-fty-types-mutual-flag
       (list flag prod option flexsum flexalst
             flexlst name name-lst flextypes-table
             fty-info acc ordered-acc))
  (cond
   ((equal flag 'generate-flexprod-type)
    ((lambda
        (acl2::__function__ ordered-acc
                            fty-info prod flextypes-table name acc)
      ((lambda (acc name flextypes-table
                    prod fty-info ordered-acc)
        ((lambda
               (ordered-acc fty-info acc prod flextypes-table name)
          ((lambda (name flextypes-table
                         prod ordered-acc acc fty-info)
            (if (equal (generate-type-measure fty-info acc)
                       '0)
                (cons acc (cons ordered-acc 'nil))
             (if (assoc-equal name acc)
                 (cons acc (cons ordered-acc 'nil))
              (if
               (fty::flexprod-p prod)
               ((lambda (fields flextypes-table
                                ordered-acc acc name fty-info)
                 ((lambda (mv name acc
                              ordered-acc fty-info flextypes-table)
                   ((lambda
                     (type-lst field-alst name acc
                               ordered-acc fty-info flextypes-table)
                     ((lambda
                           (new-prod type-lst flextypes-table
                                     fty-info ordered-acc acc name)
                       ((lambda
                            (new-acc-1
                                 name new-prod ordered-acc
                                 fty-info flextypes-table type-lst)
                         ((lambda (mv new-prod name)
                           ((lambda
                             (new-acc-2
                                  updated-ordered-acc new-prod name)
                             (cons
                              new-acc-2
                              (cons
                               (acons
                                  name new-prod updated-ordered-acc)
                               'nil)))
                            (mv-nth '0 mv)
                            (mv-nth '1 mv)
                            new-prod name))
                          (generate-fty-types-mutual-flag
                            'generate-fty-type-list
                            nil nil
                            nil nil nil nil type-lst flextypes-table
                            fty-info new-acc-1 ordered-acc)
                          new-prod name))
                        (acons name new-prod acc)
                        name new-prod ordered-acc
                        fty-info flextypes-table type-lst))
                      (fty-type-prod field-alst)
                      type-lst flextypes-table
                      fty-info ordered-acc acc name))
                    (mv-nth '0 mv)
                    (mv-nth '1 mv)
                    name acc
                    ordered-acc fty-info flextypes-table))
                  (generate-fty-field-alist fields fty-info)
                  name acc
                  ordered-acc fty-info flextypes-table))
                (fty::flexprod->fields$inline prod)
                flextypes-table
                ordered-acc acc name fty-info)
               (cons acc (cons ordered-acc 'nil))))))
           (symbol-fix name)
           flextypes-table
           prod ordered-acc acc fty-info))
         (fty-types-fix$inline ordered-acc)
         fty-info acc prod flextypes-table name))
       (fty-types-fix$inline acc)
       name flextypes-table
       prod fty-info ordered-acc))
     'generate-flexprod-type
     ordered-acc
     fty-info prod flextypes-table name acc))
   ((equal flag 'generate-flexoption-type)
    ((lambda (acl2::__function__ ordered-acc fty-info
                                 option flextypes-table name acc)
      ((lambda (acc name flextypes-table
                    option fty-info ordered-acc)
        ((lambda (ordered-acc fty-info
                              acc option flextypes-table name)
          ((lambda (name flextypes-table
                         option ordered-acc acc fty-info)
            (if (equal (generate-type-measure fty-info acc)
                       '0)
                (cons acc (cons ordered-acc 'nil))
             (if (assoc-equal name acc)
                 (cons acc (cons ordered-acc 'nil))
              (if
               (fty::flexprod-p option)
               ((lambda
                      (fields name acc
                              ordered-acc fty-info flextypes-table)
                 (if
                  (consp fields)
                  (if
                   (equal (cdr fields) 'nil)
                   ((lambda (first flextypes-table
                                   fty-info ordered-acc acc name)
                     (if
                      (fty::flexprod-field-p first)
                      ((lambda
                         (some-type
                              name acc
                              ordered-acc fty-info flextypes-table)
                        (if
                         (symbolp some-type)
                         ((lambda
                           (basic?
                            flextypes-table
                            fty-info ordered-acc acc some-type name)
                           (if basic?
                            (cons
                             (acons name (fty-type-option some-type)
                                    acc)
                             (cons
                               (acons
                                    name (fty-type-option some-type)
                                    ordered-acc)
                               'nil))
                            ((lambda
                                (some-info
                                     some-type flextypes-table
                                     fty-info ordered-acc acc name)
                              (if some-info
                               ((lambda
                                     (some-name
                                          name acc ordered-acc
                                          fty-info flextypes-table)
                                 ((lambda
                                   (new-option
                                      some-name flextypes-table
                                      fty-info ordered-acc acc name)
                                   ((lambda
                                     (new-acc-1
                                          name new-option
                                          ordered-acc fty-info
                                          flextypes-table some-name)
                                     ((lambda (mv new-option name)
                                       ((lambda
                                         (new-acc-2 new-ordered-acc
                                                    new-option name)
                                         (cons
                                          new-acc-2
                                          (cons
                                             (acons name new-option
                                                    new-ordered-acc)
                                             'nil)))
                                        (mv-nth '0 mv)
                                        (mv-nth '1 mv)
                                        new-option name))
                                      (generate-fty-types-mutual-flag
                                       'generate-fty-type
                                       nil nil nil nil nil some-name
                                       nil flextypes-table fty-info
                                       new-acc-1 ordered-acc)
                                      new-option name))
                                    (acons name new-option acc)
                                    name
                                    new-option ordered-acc fty-info
                                    flextypes-table some-name))
                                  (fty-type-option some-name)
                                  some-name flextypes-table
                                  fty-info ordered-acc acc name))
                                (fty-info->name$inline
                                     (cdr some-info))
                                name acc ordered-acc
                                fty-info flextypes-table)
                               (cons acc (cons ordered-acc 'nil))))
                             (assoc-equal some-type fty-info)
                             some-type flextypes-table
                             fty-info ordered-acc acc name)))
                          (assoc-equal some-type (smt-types))
                          flextypes-table
                          fty-info ordered-acc acc some-type name)
                         (cons acc (cons ordered-acc 'nil))))
                       (fty::flexprod-field->type$inline first)
                       name acc
                       ordered-acc fty-info flextypes-table)
                      (cons acc (cons ordered-acc 'nil))))
                    (car fields)
                    flextypes-table
                    fty-info ordered-acc acc name)
                   (cons acc (cons ordered-acc 'nil)))
                  (cons acc (cons ordered-acc 'nil))))
                (fty::flexprod->fields$inline option)
                name acc
                ordered-acc fty-info flextypes-table)
               (cons acc (cons ordered-acc 'nil))))))
           (symbol-fix name)
           flextypes-table
           option ordered-acc acc fty-info))
         (fty-types-fix$inline ordered-acc)
         fty-info
         acc option flextypes-table name))
       (fty-types-fix$inline acc)
       name flextypes-table
       option fty-info ordered-acc))
     'generate-flexoption-type
     ordered-acc fty-info
     option flextypes-table name acc))
   ((equal flag 'generate-flexsum-type)
    ((lambda
          (acl2::__function__ ordered-acc
                              fty-info flextypes-table flexsum acc)
      ((lambda (acc flexsum
                    flextypes-table fty-info ordered-acc)
        ((lambda (ordered-acc acc fty-info flextypes-table flexsum)
          (if
           (fty::flexsum-p flexsum)
           ((lambda (prods flextypes-table
                           fty-info acc ordered-acc flexsum)
             (if
              (consp prods)
              ((lambda (name ordered-acc
                             acc fty-info flextypes-table prods)
                (if
                 (symbolp name)
                 (if
                  (equal (len prods) '1)
                  (if (fty::flexprod-p (car prods))
                      (generate-fty-types-mutual-flag
                           'generate-flexprod-type
                           (car prods)
                           nil nil nil nil name nil flextypes-table
                           fty-info acc ordered-acc)
                    (cons acc (cons ordered-acc 'nil)))
                  (if
                   (equal (len prods) '2)
                   (if
                    (fty::flexprod-p (car prods))
                    (if
                     (fty::flexprod-p (car (cdr prods)))
                     (if
                      (equal
                           (fty::flexprod->kind$inline (car prods))
                           ':none)
                      (if (equal (fty::flexprod->kind$inline
                                      (car (cdr prods)))
                                 ':some)
                          (generate-fty-types-mutual-flag
                               'generate-flexoption-type
                               nil (car (cdr prods))
                               nil nil nil name nil flextypes-table
                               fty-info acc ordered-acc)
                        (cons acc (cons ordered-acc 'nil)))
                      (if
                       (equal (fty::flexprod->kind$inline
                                   (car (cdr prods)))
                              ':none)
                       (if
                        (equal
                            (fty::flexprod->kind$inline (car prods))
                            ':some)
                        (generate-fty-types-mutual-flag
                             'generate-flexoption-type
                             nil (car prods)
                             nil nil nil name nil flextypes-table
                             fty-info acc ordered-acc)
                        (cons acc (cons ordered-acc 'nil)))
                       (cons acc (cons ordered-acc 'nil))))
                     (cons acc (cons ordered-acc 'nil)))
                    (cons acc (cons ordered-acc 'nil)))
                   (cons acc (cons ordered-acc 'nil))))
                 (cons acc (cons ordered-acc 'nil))))
               (fty::flexsum->name$inline flexsum)
               ordered-acc
               acc fty-info flextypes-table prods)
              (cons acc (cons ordered-acc 'nil))))
            (fty::flexsum->prods$inline flexsum)
            flextypes-table
            fty-info acc ordered-acc flexsum)
           (cons acc (cons ordered-acc 'nil))))
         (fty-types-fix$inline ordered-acc)
         acc fty-info flextypes-table flexsum))
       (fty-types-fix$inline acc)
       flexsum
       flextypes-table fty-info ordered-acc))
     'generate-flexsum-type
     ordered-acc
     fty-info flextypes-table flexsum acc))
   ((equal flag 'generate-flexalist-type)
    ((lambda
         (acl2::__function__ ordered-acc
                             flextypes-table flexalst fty-info acc)
      ((lambda (acc fty-info
                    flexalst flextypes-table ordered-acc)
        ((lambda (ordered-acc flextypes-table flexalst acc fty-info)
          (if (equal (generate-type-measure fty-info acc)
                     '0)
              (cons acc (cons ordered-acc 'nil))
           (if
            (fty::flexalist-p flexalst)
            ((lambda (name flextypes-table
                           fty-info flexalst ordered-acc acc)
              (if
               (symbolp name)
               (if (assoc-equal name acc)
                   (cons acc (cons ordered-acc 'nil))
                ((lambda
                    (key-type fty-info name acc
                              ordered-acc flextypes-table flexalst)
                  (if
                   (symbolp key-type)
                   ((lambda
                       (val-type
                            flextypes-table
                            ordered-acc acc name fty-info key-type)
                     (if
                      (symbolp val-type)
                      ((lambda
                         (basic-key?
                              key-type fty-info name acc
                              ordered-acc flextypes-table val-type)
                        ((lambda
                          (basic-val?
                              val-type flextypes-table ordered-acc
                              acc name basic-key? fty-info key-type)
                          ((lambda
                            (key-info
                                 basic-key? basic-val?
                                 name key-type acc ordered-acc
                                 flextypes-table fty-info val-type)
                            ((lambda
                              (val-info
                                key-info flextypes-table
                                fty-info ordered-acc acc val-type
                                key-type name basic-val? basic-key?)
                              (if basic-key?
                               (if basic-val?
                                (cons
                                 (acons
                                  name
                                  (fty-type-alist key-type val-type)
                                  acc)
                                 (cons
                                      (acons name
                                             (fty-type-alist
                                                  key-type val-type)
                                             ordered-acc)
                                      'nil))
                                (if val-info
                                 ((lambda
                                   (val-name
                                       name acc ordered-acc fty-info
                                       flextypes-table key-type)
                                   ((lambda
                                     (new-alist
                                      val-name flextypes-table
                                      fty-info ordered-acc acc name)
                                     ((lambda
                                       (new-acc-1
                                           name new-alist
                                           ordered-acc fty-info
                                           flextypes-table val-name)
                                       ((lambda (mv new-alist name)
                                         ((lambda
                                               (new-acc-2
                                                    new-ordered-acc
                                                    new-alist name)
                                           (cons
                                            new-acc-2
                                            (cons
                                             (acons name new-alist
                                                    new-ordered-acc)
                                             'nil)))
                                          (mv-nth '0 mv)
                                          (mv-nth '1 mv)
                                          new-alist name))
                                        (generate-fty-types-mutual-flag
                                            'generate-fty-type
                                            nil nil
                                            nil nil nil val-name nil
                                            flextypes-table fty-info
                                            new-acc-1 ordered-acc)
                                        new-alist name))
                                      (acons name new-alist acc)
                                      name
                                      new-alist ordered-acc fty-info
                                      flextypes-table val-name))
                                    (fty-type-alist
                                         key-type val-name)
                                    val-name flextypes-table
                                    fty-info ordered-acc acc name))
                                  (fty-info->name$inline
                                       (cdr val-info))
                                  name acc ordered-acc
                                  fty-info flextypes-table key-type)
                                 (cons
                                      acc (cons ordered-acc 'nil))))
                               (if basic-val?
                                (if key-info
                                 ((lambda
                                   (key-name
                                       name acc ordered-acc fty-info
                                       flextypes-table val-type)
                                   ((lambda
                                     (new-alist
                                      key-name flextypes-table
                                      fty-info ordered-acc acc name)
                                     ((lambda
                                       (new-acc-1
                                           name new-alist
                                           ordered-acc fty-info
                                           flextypes-table key-name)
                                       ((lambda (mv new-alist name)
                                         ((lambda
                                               (new-acc-2
                                                    new-ordered-acc
                                                    new-alist name)
                                           (cons
                                            new-acc-2
                                            (cons
                                             (acons name new-alist
                                                    new-ordered-acc)
                                             'nil)))
                                          (mv-nth '0 mv)
                                          (mv-nth '1 mv)
                                          new-alist name))
                                        (generate-fty-types-mutual-flag
                                            'generate-fty-type
                                            nil nil
                                            nil nil nil key-name nil
                                            flextypes-table fty-info
                                            new-acc-1 ordered-acc)
                                        new-alist name))
                                      (acons name new-alist acc)
                                      name
                                      new-alist ordered-acc fty-info
                                      flextypes-table key-name))
                                    (fty-type-alist
                                         key-name val-type)
                                    key-name flextypes-table
                                    fty-info ordered-acc acc name))
                                  (fty-info->name$inline
                                       (cdr key-info))
                                  name acc ordered-acc
                                  fty-info flextypes-table val-type)
                                 (cons acc (cons ordered-acc 'nil)))
                                (if key-info
                                 (if val-info
                                  ((lambda
                                    (val-name
                                      flextypes-table fty-info
                                      ordered-acc acc name key-info)
                                    ((lambda
                                      (key-name
                                       name acc ordered-acc fty-info
                                       flextypes-table val-name)
                                      ((lambda
                                        (new-alist
                                            key-name flextypes-table
                                            fty-info ordered-acc
                                            val-name acc name)
                                        ((lambda
                                          (new-acc
                                           name new-alist val-name
                                           ordered-acc fty-info
                                           flextypes-table key-name)
                                          ((lambda
                                            (mv
                                              val-name
                                              flextypes-table
                                              new-alist
                                              name new-acc fty-info)
                                            ((lambda
                                              (new-acc-1
                                                   new-ordered-acc-1
                                                   val-name
                                                   flextypes-table
                                                   new-alist name
                                                   new-acc fty-info)
                                              ((lambda
                                                (new-acc-1
                                                  name
                                                  new-alist fty-info
                                                  flextypes-table
                                                  val-name
                                                  new-ordered-acc-1
                                                  new-acc)
                                                (if
                                                 (equal
                                                     new-acc-1 'nil)
                                                 (cons
                                                  new-acc
                                                  (cons
                                                   new-ordered-acc-1
                                                   'nil))
                                                 ((lambda
                                                   (mv
                                                     new-alist name)
                                                   ((lambda
                                                     (new-acc-2
                                                      new-ordered-acc-2
                                                      new-alist
                                                      name)
                                                     (cons
                                                      new-acc-2
                                                      (cons
                                                       (acons
                                                        name
                                                        new-alist
                                                        new-ordered-acc-2)
                                                       'nil)))
                                                    (mv-nth '0 mv)
                                                    (mv-nth '1 mv)
                                                    new-alist name))
                                                  (generate-fty-types-mutual-flag
                                                   'generate-fty-type
                                                   nil nil nil nil
                                                   nil val-name nil
                                                   flextypes-table
                                                   fty-info
                                                   new-acc-1
                                                   new-ordered-acc-1)
                                                  new-alist name)))
                                               (if
                                                (o<
                                                 (generate-type-measure
                                                   fty-info new-acc)
                                                 (generate-type-measure
                                                      fty-info
                                                      new-acc-1))
                                                'nil
                                                new-acc-1)
                                               name
                                               new-alist fty-info
                                               flextypes-table
                                               val-name
                                               new-ordered-acc-1
                                               new-acc))
                                             (mv-nth '0 mv)
                                             (mv-nth '1 mv)
                                             val-name
                                             flextypes-table
                                             new-alist
                                             name new-acc fty-info))
                                           (generate-fty-types-mutual-flag
                                            'generate-fty-type
                                            nil nil
                                            nil nil nil key-name nil
                                            flextypes-table fty-info
                                            new-acc ordered-acc)
                                           val-name
                                           flextypes-table new-alist
                                           name new-acc fty-info))
                                         (acons name new-alist acc)
                                         name new-alist val-name
                                         ordered-acc fty-info
                                         flextypes-table key-name))
                                       (fty-type-alist
                                            key-name val-name)
                                       key-name flextypes-table
                                       fty-info ordered-acc
                                       val-name acc name))
                                     (fty-info->name$inline
                                          (cdr key-info))
                                     name acc ordered-acc fty-info
                                     flextypes-table val-name))
                                   (fty-info->name$inline
                                        (cdr val-info))
                                   flextypes-table fty-info
                                   ordered-acc acc name key-info)
                                  (cons
                                       acc (cons ordered-acc 'nil)))
                                 (cons
                                    acc (cons ordered-acc 'nil))))))
                             (assoc-equal val-type fty-info)
                             key-info flextypes-table
                             fty-info ordered-acc acc val-type
                             key-type name basic-val? basic-key?))
                           (assoc-equal key-type fty-info)
                           basic-key?
                           basic-val? name key-type acc ordered-acc
                           flextypes-table fty-info val-type))
                         (assoc-equal val-type (smt-types))
                         val-type flextypes-table ordered-acc
                         acc name basic-key? fty-info key-type))
                       (assoc-equal key-type (smt-types))
                       key-type fty-info name acc
                       ordered-acc flextypes-table val-type)
                      (cons acc (cons ordered-acc 'nil))))
                    (fty::flexalist->val-type$inline flexalst)
                    flextypes-table
                    ordered-acc acc name fty-info key-type)
                   (cons acc (cons ordered-acc 'nil))))
                 (fty::flexalist->key-type$inline flexalst)
                 fty-info name acc
                 ordered-acc flextypes-table flexalst))
               (cons acc (cons ordered-acc 'nil))))
             (fty::flexalist->name$inline flexalst)
             flextypes-table
             fty-info flexalst ordered-acc acc)
            (cons acc (cons ordered-acc 'nil)))))
         (fty-types-fix$inline ordered-acc)
         flextypes-table flexalst acc fty-info))
       (fty-types-fix$inline acc)
       fty-info
       flexalst flextypes-table ordered-acc))
     'generate-flexalist-type
     ordered-acc
     flextypes-table flexalst fty-info acc))
   ((equal flag 'generate-flexlist-type)
    ((lambda
          (acl2::__function__ ordered-acc
                              flextypes-table flexlst fty-info acc)
      ((lambda (acc fty-info
                    flexlst flextypes-table ordered-acc)
        ((lambda (ordered-acc flextypes-table flexlst acc fty-info)
          (if (equal (generate-type-measure fty-info acc)
                     '0)
              (cons acc (cons ordered-acc 'nil))
           (if
            (fty::flexlist-p flexlst)
            ((lambda (name fty-info
                           flextypes-table flexlst ordered-acc acc)
              (if
               (symbolp name)
               (if (assoc-equal name acc)
                   (cons acc (cons ordered-acc 'nil))
                ((lambda (true-listp?
                              flextypes-table
                              fty-info ordered-acc acc name flexlst)
                  (if true-listp?
                   ((lambda
                     (elt-type name acc
                               ordered-acc fty-info flextypes-table)
                     (if
                      (symbolp elt-type)
                      ((lambda
                        (basic?
                             flextypes-table
                             fty-info ordered-acc acc elt-type name)
                        (if basic?
                         (cons
                          (acons name (fty-type-list elt-type)
                                 acc)
                          (cons (acons name (fty-type-list elt-type)
                                       ordered-acc)
                                'nil))
                         ((lambda
                               (info elt-type flextypes-table
                                     fty-info ordered-acc acc name)
                           (if info
                            ((lambda
                              (elt-name
                               name acc
                               ordered-acc fty-info flextypes-table)
                              ((lambda
                                (new-list
                                     elt-name flextypes-table
                                     fty-info ordered-acc acc name)
                                ((lambda
                                  (new-acc-1
                                       name
                                       new-list ordered-acc fty-info
                                       flextypes-table elt-name)
                                  ((lambda (mv new-list name)
                                    ((lambda
                                         (new-acc-2 new-ordered-acc
                                                    new-list name)
                                      (cons
                                       new-acc-2
                                       (cons
                                        (acons
                                           name
                                           new-list new-ordered-acc)
                                        'nil)))
                                     (mv-nth '0 mv)
                                     (mv-nth '1 mv)
                                     new-list name))
                                   (generate-fty-types-mutual-flag
                                    'generate-fty-type
                                    nil nil nil nil
                                    nil elt-name nil flextypes-table
                                    fty-info new-acc-1 ordered-acc)
                                   new-list name))
                                 (acons name new-list acc)
                                 name new-list ordered-acc
                                 fty-info flextypes-table elt-name))
                               (fty-type-list elt-name)
                               elt-name flextypes-table
                               fty-info ordered-acc acc name))
                             (fty-info->name$inline (cdr info))
                             name acc
                             ordered-acc fty-info flextypes-table)
                            (cons acc (cons ordered-acc 'nil))))
                          (assoc-equal elt-type fty-info)
                          elt-type flextypes-table
                          fty-info ordered-acc acc name)))
                       (assoc-equal elt-type (smt-types))
                       flextypes-table
                       fty-info ordered-acc acc elt-type name)
                      (cons acc (cons ordered-acc 'nil))))
                    (fty::flexlist->elt-type$inline flexlst)
                    name acc
                    ordered-acc fty-info flextypes-table)
                   (cons acc (cons ordered-acc 'nil))))
                 (fty::flexlist->true-listp$inline flexlst)
                 flextypes-table
                 fty-info ordered-acc acc name flexlst))
               (cons acc (cons ordered-acc 'nil))))
             (fty::flexlist->name$inline flexlst)
             fty-info
             flextypes-table flexlst ordered-acc acc)
            (cons acc (cons ordered-acc 'nil)))))
         (fty-types-fix$inline ordered-acc)
         flextypes-table flexlst acc fty-info))
       (fty-types-fix$inline acc)
       fty-info
       flexlst flextypes-table ordered-acc))
     'generate-flexlist-type
     ordered-acc
     flextypes-table flexlst fty-info acc))
   ((equal flag 'generate-fty-type)
    ((lambda (acl2::__function__ ordered-acc
                                 fty-info name flextypes-table acc)
      ((lambda (acc flextypes-table
                    name fty-info ordered-acc)
        ((lambda (ordered-acc acc fty-info name flextypes-table)
          (if
           (alistp flextypes-table)
           ((lambda (exist? name flextypes-table
                            fty-info ordered-acc acc)
             (if exist?
              ((lambda (agg acc
                            ordered-acc fty-info flextypes-table)
                (if
                 (fty::flextypes-p agg)
                 ((lambda (types flextypes-table
                                 fty-info ordered-acc acc)
                   (if
                    (true-listp types)
                    (if
                     (consp types)
                     (if
                      (equal (cdr types) 'nil)
                      ((lambda (type ordered-acc
                                     acc fty-info flextypes-table)
                        (if
                         (fty::flexsum-p type)
                         (generate-fty-types-mutual-flag
                            'generate-flexsum-type
                            nil
                            nil type nil nil nil nil flextypes-table
                            fty-info acc ordered-acc)
                         (if
                          (fty::flexlist-p type)
                          (generate-fty-types-mutual-flag
                            'generate-flexlist-type
                            nil
                            nil nil nil type nil nil flextypes-table
                            fty-info acc ordered-acc)
                          (if
                           (fty::flexalist-p type)
                           (generate-fty-types-mutual-flag
                            'generate-flexalist-type
                            nil
                            nil nil type nil nil nil flextypes-table
                            fty-info acc ordered-acc)
                           (cons acc (cons ordered-acc 'nil))))))
                       (car types)
                       ordered-acc
                       acc fty-info flextypes-table)
                      (cons acc (cons ordered-acc 'nil)))
                     (cons acc (cons ordered-acc 'nil)))
                    (cons acc (cons ordered-acc 'nil))))
                  (fty::flextypes->types$inline agg)
                  flextypes-table
                  fty-info ordered-acc acc)
                 (cons acc (cons ordered-acc 'nil))))
               (cdr exist?)
               acc
               ordered-acc fty-info flextypes-table)
              (cons acc (cons ordered-acc 'nil))))
            (assoc-equal name flextypes-table)
            name flextypes-table
            fty-info ordered-acc acc)
           (cons acc (cons ordered-acc 'nil))))
         (fty-types-fix$inline ordered-acc)
         acc fty-info name flextypes-table))
       (fty-types-fix$inline acc)
       flextypes-table
       name fty-info ordered-acc))
     'generate-fty-type
     ordered-acc
     fty-info name flextypes-table acc))
   (t
    ((lambda
          (acl2::__function__ acc fty-info
                              flextypes-table ordered-acc name-lst)
      ((lambda (name-lst ordered-acc
                         flextypes-table fty-info acc)
        ((lambda (acc name-lst
                      fty-info flextypes-table ordered-acc)
          ((lambda
                (ordered-acc flextypes-table fty-info acc name-lst)
            (if
             (consp name-lst)
             ((lambda (first ordered-acc
                             acc fty-info flextypes-table name-lst)
               ((lambda (rest flextypes-table
                              fty-info acc ordered-acc first)
                 ((lambda (basic? first ordered-acc
                                  acc fty-info flextypes-table rest)
                   (if basic?
                       (generate-fty-types-mutual-flag
                            'generate-fty-type-list
                            nil
                            nil nil nil nil nil rest flextypes-table
                            fty-info acc ordered-acc)
                    ((lambda (mv rest flextypes-table acc fty-info)
                      ((lambda
                        (new-acc new-ordered-acc
                                 rest flextypes-table acc fty-info)
                        ((lambda (new-acc fty-info flextypes-table
                                          rest new-ordered-acc acc)
                          (if (equal new-acc 'nil)
                              (cons acc (cons new-ordered-acc 'nil))
                           (generate-fty-types-mutual-flag
                            'generate-fty-type-list
                            nil
                            nil nil nil nil nil rest flextypes-table
                            fty-info new-acc new-ordered-acc)))
                         (if
                          (o<
                           (generate-type-measure fty-info acc)
                           (generate-type-measure fty-info new-acc))
                          'nil
                          new-acc)
                         fty-info flextypes-table
                         rest new-ordered-acc acc))
                       (mv-nth '0 mv)
                       (mv-nth '1 mv)
                       rest flextypes-table acc fty-info))
                     (generate-fty-types-mutual-flag
                          'generate-fty-type
                          nil nil
                          nil nil nil first nil flextypes-table
                          fty-info acc ordered-acc)
                     rest flextypes-table acc fty-info)))
                  (assoc-equal first (smt-types))
                  first ordered-acc
                  acc fty-info flextypes-table rest))
                (cdr name-lst)
                flextypes-table
                fty-info acc ordered-acc first))
              (car name-lst)
              ordered-acc
              acc fty-info flextypes-table name-lst)
             (cons acc (cons ordered-acc 'nil))))
           (fty-types-fix$inline ordered-acc)
           flextypes-table fty-info acc name-lst))
         (fty-types-fix$inline acc)
         name-lst
         fty-info flextypes-table ordered-acc))
       (acl2::symbol-list-fix$inline name-lst)
       ordered-acc
       flextypes-table fty-info acc))
     'generate-fty-type-list
     acc fty-info flextypes-table
     ordered-acc name-lst)))))

Theorem: generate-fty-types-mutual-flag-equivalences

(defthm generate-fty-types-mutual-flag-equivalences
  (and (equal (generate-fty-types-mutual-flag
                   'generate-flexprod-type
                   prod option flexsum flexalst
                   flexlst name name-lst flextypes-table
                   fty-info acc ordered-acc)
              (generate-flexprod-type name prod flextypes-table
                                      fty-info acc ordered-acc))
       (equal (generate-fty-types-mutual-flag
                   'generate-flexoption-type
                   prod option flexsum flexalst
                   flexlst name name-lst flextypes-table
                   fty-info acc ordered-acc)
              (generate-flexoption-type name option flextypes-table
                                        fty-info acc ordered-acc))
       (equal (generate-fty-types-mutual-flag
                   'generate-flexsum-type
                   prod option flexsum flexalst
                   flexlst name name-lst flextypes-table
                   fty-info acc ordered-acc)
              (generate-flexsum-type flexsum flextypes-table
                                     fty-info acc ordered-acc))
       (equal (generate-fty-types-mutual-flag
                   'generate-flexalist-type
                   prod option flexsum flexalst
                   flexlst name name-lst flextypes-table
                   fty-info acc ordered-acc)
              (generate-flexalist-type flexalst flextypes-table
                                       fty-info acc ordered-acc))
       (equal (generate-fty-types-mutual-flag
                   'generate-flexlist-type
                   prod option flexsum flexalst
                   flexlst name name-lst flextypes-table
                   fty-info acc ordered-acc)
              (generate-flexlist-type flexlst flextypes-table
                                      fty-info acc ordered-acc))
       (equal (generate-fty-types-mutual-flag
                   'generate-fty-type
                   prod option flexsum flexalst
                   flexlst name name-lst flextypes-table
                   fty-info acc ordered-acc)
              (generate-fty-type name flextypes-table
                                 fty-info acc ordered-acc))
       (equal (generate-fty-types-mutual-flag
                   'generate-fty-type-list
                   prod option flexsum flexalst
                   flexlst name name-lst flextypes-table
                   fty-info acc ordered-acc)
              (generate-fty-type-list name-lst flextypes-table
                                      fty-info acc ordered-acc))))

Theorem: return-type-of-generate-flexprod-type.updated-acc

(defthm return-type-of-generate-flexprod-type.updated-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexprod-type name prod flextypes-table
                                fty-info acc ordered-acc)))
    (fty-types-p updated-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexprod-type.updated-ordered-acc

(defthm return-type-of-generate-flexprod-type.updated-ordered-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexprod-type name prod flextypes-table
                                fty-info acc ordered-acc)))
    (fty-types-p updated-ordered-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexoption-type.updated-acc

(defthm return-type-of-generate-flexoption-type.updated-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexoption-type name option flextypes-table
                                  fty-info acc ordered-acc)))
    (fty-types-p updated-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexoption-type.updated-ordered-acc

(defthm return-type-of-generate-flexoption-type.updated-ordered-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexoption-type name option flextypes-table
                                  fty-info acc ordered-acc)))
    (fty-types-p updated-ordered-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexsum-type.updated-acc

(defthm return-type-of-generate-flexsum-type.updated-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexsum-type flexsum flextypes-table
                               fty-info acc ordered-acc)))
    (fty-types-p updated-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexsum-type.updated-ordered-acc

(defthm return-type-of-generate-flexsum-type.updated-ordered-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexsum-type flexsum flextypes-table
                               fty-info acc ordered-acc)))
    (fty-types-p updated-ordered-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexalist-type.updated-acc

(defthm return-type-of-generate-flexalist-type.updated-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexalist-type flexalst flextypes-table
                                 fty-info acc ordered-acc)))
    (fty-types-p updated-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexalist-type.updated-ordered-acc

(defthm return-type-of-generate-flexalist-type.updated-ordered-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexalist-type flexalst flextypes-table
                                 fty-info acc ordered-acc)))
    (fty-types-p updated-ordered-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexlist-type.updated-acc

(defthm return-type-of-generate-flexlist-type.updated-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexlist-type flexlst flextypes-table
                                fty-info acc ordered-acc)))
    (fty-types-p updated-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-flexlist-type.updated-ordered-acc

(defthm return-type-of-generate-flexlist-type.updated-ordered-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-flexlist-type flexlst flextypes-table
                                fty-info acc ordered-acc)))
    (fty-types-p updated-ordered-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-fty-type.updated-acc

(defthm return-type-of-generate-fty-type.updated-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-fty-type name flextypes-table
                           fty-info acc ordered-acc)))
    (fty-types-p updated-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-fty-type.updated-ordered-acc

(defthm return-type-of-generate-fty-type.updated-ordered-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-fty-type name flextypes-table
                           fty-info acc ordered-acc)))
    (fty-types-p updated-ordered-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-fty-type-list.updated-acc

(defthm return-type-of-generate-fty-type-list.updated-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-fty-type-list name-lst flextypes-table
                                fty-info acc ordered-acc)))
    (fty-types-p updated-acc))
  :rule-classes :rewrite)

Theorem: return-type-of-generate-fty-type-list.updated-ordered-acc

(defthm return-type-of-generate-fty-type-list.updated-ordered-acc
  (b* (((mv ?updated-acc ?updated-ordered-acc)
        (generate-fty-type-list name-lst flextypes-table
                                fty-info acc ordered-acc)))
    (fty-types-p updated-ordered-acc))
  :rule-classes :rewrite)

Subtopics

Fncall-of-flextype

Checking if a function call is a flextype related call. These calls will be translated directly to SMT solver, therefore won't need to be expanded.