• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Lexer
        • Vl-loadstate
        • Parser
        • Vl-load-merge-descriptions
        • Scope-of-defines
        • Vl-load-file
        • Vl-flush-out-descriptions
        • Vl-description
          • Vl-description-p
          • Vl-sort-descriptions
          • Vl-description-fix
          • Vl-find-description
          • Vl-description-equiv
          • Vl-description->name
          • Vl-make-descalist
          • Vl-design-from-descriptions
          • Vl-design-descriptions
          • Vl-fast-filter-descriptions
          • Vl-fast-find-description
          • Vl-descalist
          • Vl-slow-delete-descriptions
        • Vl-loadresult
        • Vl-read-file
        • Vl-find-basename/extension
        • Vl-find-file
        • Vl-read-files
        • Extended-characters
        • Vl-load
        • Vl-load-main
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-load-descriptions
        • Vl-load-files
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-descriptionlist
      • Transforms
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Vl-description

Vl-sort-descriptions

Signature

(vl-sort-descriptions x &key modules udps interfaces programs 
                      packages configs taskdecls fundecls 
                      paramdecls imports fwdtypedefs typedefs) 
 
  → 
(mv modules udps interfaces programs 
    packages configs taskdecls fundecls 
    paramdecls imports fwdtypedefs typedefs) 

Arguments

x — Guard (vl-descriptionlist-p x).

modules — Guard (vl-modulelist-p modules).

udps — Guard (vl-udplist-p udps).

interfaces — Guard (vl-interfacelist-p interfaces).

programs — Guard (vl-programlist-p programs).

packages — Guard (vl-packagelist-p packages).

configs — Guard (vl-configlist-p configs).

taskdecls — Guard (vl-taskdecllist-p taskdecls).

fundecls — Guard (vl-fundecllist-p fundecls).

paramdecls — Guard (vl-paramdecllist-p paramdecls).

imports — Guard (vl-importlist-p imports).

fwdtypedefs — Guard (vl-fwdtypedeflist-p fwdtypedefs).

typedefs — Guard (vl-typedeflist-p typedefs).

Returns

modules — Type (vl-modulelist-p modules).

udps — Type (vl-udplist-p udps).

interfaces — Type (vl-interfacelist-p interfaces).

programs — Type (vl-programlist-p programs).

packages — Type (vl-packagelist-p packages).

configs — Type (vl-configlist-p configs).

taskdecls — Type (vl-taskdecllist-p taskdecls).

fundecls — Type (vl-fundecllist-p fundecls).

paramdecls — Type (vl-paramdecllist-p paramdecls).

imports — Type (vl-importlist-p imports).

fwdtypedefs — Type (vl-fwdtypedeflist-p fwdtypedefs).

typedefs — Type (vl-typedeflist-p typedefs).

Definitions and Theorems

Function: vl-sort-descriptions-fn

(defun vl-sort-descriptions-fn
       (x modules udps interfaces programs
          packages configs taskdecls fundecls
          paramdecls imports fwdtypedefs typedefs)
  (declare (xargs :guard (and (vl-descriptionlist-p x)
                              (vl-modulelist-p modules)
                              (vl-udplist-p udps)
                              (vl-interfacelist-p interfaces)
                              (vl-programlist-p programs)
                              (vl-packagelist-p packages)
                              (vl-configlist-p configs)
                              (vl-taskdecllist-p taskdecls)
                              (vl-fundecllist-p fundecls)
                              (vl-paramdecllist-p paramdecls)
                              (vl-importlist-p imports)
                              (vl-fwdtypedeflist-p fwdtypedefs)
                              (vl-typedeflist-p typedefs))))
  (let ((__function__ 'vl-sort-descriptions))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (mv (vl-modulelist-fix modules)
              (vl-udplist-fix udps)
              (vl-interfacelist-fix interfaces)
              (vl-programlist-fix programs)
              (vl-packagelist-fix packages)
              (vl-configlist-fix configs)
              (vl-taskdecllist-fix taskdecls)
              (vl-fundecllist-fix fundecls)
              (vl-paramdecllist-fix paramdecls)
              (vl-importlist-fix imports)
              (vl-fwdtypedeflist-fix fwdtypedefs)
              (vl-typedeflist-fix typedefs)))
         (x1 (vl-description-fix (car x)))
         (tag (tag x1)))
      (vl-sort-descriptions (cdr x)
                            :modules
                            (if (eq tag :vl-module)
                                (cons x1 modules)
                              modules)
                            :udps
                            (if (eq tag :vl-udp)
                                (cons x1 udps)
                              udps)
                            :interfaces
                            (if (eq tag :vl-interface)
                                (cons x1 interfaces)
                              interfaces)
                            :programs
                            (if (eq tag :vl-program)
                                (cons x1 programs)
                              programs)
                            :packages
                            (if (eq tag :vl-package)
                                (cons x1 packages)
                              packages)
                            :configs
                            (if (eq tag :vl-config)
                                (cons x1 configs)
                              configs)
                            :taskdecls
                            (if (eq tag :vl-taskdecl)
                                (cons x1 taskdecls)
                              taskdecls)
                            :fundecls
                            (if (eq tag :vl-fundecl)
                                (cons x1 fundecls)
                              fundecls)
                            :paramdecls
                            (if (eq tag :vl-paramdecl)
                                (cons x1 paramdecls)
                              paramdecls)
                            :imports
                            (if (eq tag :vl-import)
                                (cons x1 imports)
                              imports)
                            :fwdtypedefs
                            (if (eq tag :vl-fwdtypedef)
                                (cons x1 fwdtypedefs)
                              fwdtypedefs)
                            :typedefs
                            (if (eq tag :vl-typedef)
                                (cons x1 typedefs)
                              typedefs)))))

Theorem: vl-modulelist-p-of-vl-sort-descriptions.modules

(defthm vl-modulelist-p-of-vl-sort-descriptions.modules
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-modulelist-p modules))
  :rule-classes :rewrite)

Theorem: vl-udplist-p-of-vl-sort-descriptions.udps

(defthm vl-udplist-p-of-vl-sort-descriptions.udps
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-udplist-p udps))
  :rule-classes :rewrite)

Theorem: vl-interfacelist-p-of-vl-sort-descriptions.interfaces

(defthm vl-interfacelist-p-of-vl-sort-descriptions.interfaces
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-interfacelist-p interfaces))
  :rule-classes :rewrite)

Theorem: vl-programlist-p-of-vl-sort-descriptions.programs

(defthm vl-programlist-p-of-vl-sort-descriptions.programs
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-programlist-p programs))
  :rule-classes :rewrite)

Theorem: vl-packagelist-p-of-vl-sort-descriptions.packages

(defthm vl-packagelist-p-of-vl-sort-descriptions.packages
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-packagelist-p packages))
  :rule-classes :rewrite)

Theorem: vl-configlist-p-of-vl-sort-descriptions.configs

(defthm vl-configlist-p-of-vl-sort-descriptions.configs
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-configlist-p configs))
  :rule-classes :rewrite)

Theorem: vl-taskdecllist-p-of-vl-sort-descriptions.taskdecls

(defthm vl-taskdecllist-p-of-vl-sort-descriptions.taskdecls
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-taskdecllist-p taskdecls))
  :rule-classes :rewrite)

Theorem: vl-fundecllist-p-of-vl-sort-descriptions.fundecls

(defthm vl-fundecllist-p-of-vl-sort-descriptions.fundecls
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-fundecllist-p fundecls))
  :rule-classes :rewrite)

Theorem: vl-paramdecllist-p-of-vl-sort-descriptions.paramdecls

(defthm vl-paramdecllist-p-of-vl-sort-descriptions.paramdecls
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-paramdecllist-p paramdecls))
  :rule-classes :rewrite)

Theorem: vl-importlist-p-of-vl-sort-descriptions.imports

(defthm vl-importlist-p-of-vl-sort-descriptions.imports
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-importlist-p imports))
  :rule-classes :rewrite)

Theorem: vl-fwdtypedeflist-p-of-vl-sort-descriptions.fwdtypedefs

(defthm vl-fwdtypedeflist-p-of-vl-sort-descriptions.fwdtypedefs
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-fwdtypedeflist-p fwdtypedefs))
  :rule-classes :rewrite)

Theorem: vl-typedeflist-p-of-vl-sort-descriptions.typedefs

(defthm vl-typedeflist-p-of-vl-sort-descriptions.typedefs
  (b*
    (((mv ?modules ?udps
          ?interfaces ?programs ?packages ?configs
          ?taskdecls ?fundecls ?paramdecls
          ?imports ?fwdtypedefs ?typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))
    (vl-typedeflist-p typedefs))
  :rule-classes :rewrite)

Theorem: vl-sort-descriptions-fn-of-vl-descriptionlist-fix-x

(defthm vl-sort-descriptions-fn-of-vl-descriptionlist-fix-x
 (equal
   (vl-sort-descriptions-fn (vl-descriptionlist-fix x)
                            modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-descriptionlist-equiv-congruence-on-x

(defthm
   vl-sort-descriptions-fn-vl-descriptionlist-equiv-congruence-on-x
 (implies
  (vl-descriptionlist-equiv x x-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x-equiv modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-modulelist-fix-modules

(defthm vl-sort-descriptions-fn-of-vl-modulelist-fix-modules
 (equal
   (vl-sort-descriptions-fn x (vl-modulelist-fix modules)
                            udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-modulelist-equiv-congruence-on-modules

(defthm
  vl-sort-descriptions-fn-vl-modulelist-equiv-congruence-on-modules
 (implies
  (vl-modulelist-equiv modules modules-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules-equiv
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-udplist-fix-udps

(defthm vl-sort-descriptions-fn-of-vl-udplist-fix-udps
 (equal
   (vl-sort-descriptions-fn x modules (vl-udplist-fix udps)
                            interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-udplist-equiv-congruence-on-udps

(defthm vl-sort-descriptions-fn-vl-udplist-equiv-congruence-on-udps
 (implies
  (vl-udplist-equiv udps udps-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps-equiv interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-interfacelist-fix-interfaces

(defthm vl-sort-descriptions-fn-of-vl-interfacelist-fix-interfaces
 (equal
   (vl-sort-descriptions-fn x modules
                            udps (vl-interfacelist-fix interfaces)
                            programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-interfacelist-equiv-congruence-on-interfaces

(defthm
 vl-sort-descriptions-fn-vl-interfacelist-equiv-congruence-on-interfaces
 (implies
  (vl-interfacelist-equiv interfaces interfaces-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces-equiv programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-programlist-fix-programs

(defthm vl-sort-descriptions-fn-of-vl-programlist-fix-programs
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces (vl-programlist-fix programs)
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-programlist-equiv-congruence-on-programs

(defthm
 vl-sort-descriptions-fn-vl-programlist-equiv-congruence-on-programs
 (implies
  (vl-programlist-equiv programs programs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs-equiv packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-packagelist-fix-packages

(defthm vl-sort-descriptions-fn-of-vl-packagelist-fix-packages
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs (vl-packagelist-fix packages)
                            configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-packagelist-equiv-congruence-on-packages

(defthm
 vl-sort-descriptions-fn-vl-packagelist-equiv-congruence-on-packages
 (implies
  (vl-packagelist-equiv packages packages-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages-equiv
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-configlist-fix-configs

(defthm vl-sort-descriptions-fn-of-vl-configlist-fix-configs
 (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages (vl-configlist-fix configs)
                            taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-configlist-equiv-congruence-on-configs

(defthm
  vl-sort-descriptions-fn-vl-configlist-equiv-congruence-on-configs
 (implies
  (vl-configlist-equiv configs configs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules udps interfaces
                            programs packages configs-equiv
                            taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-taskdecllist-fix-taskdecls

(defthm vl-sort-descriptions-fn-of-vl-taskdecllist-fix-taskdecls
 (equal
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs (vl-taskdecllist-fix taskdecls)
                            fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-taskdecllist-equiv-congruence-on-taskdecls

(defthm
 vl-sort-descriptions-fn-vl-taskdecllist-equiv-congruence-on-taskdecls
 (implies
  (vl-taskdecllist-equiv taskdecls taskdecls-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs packages configs
                            taskdecls-equiv fundecls paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-fundecllist-fix-fundecls

(defthm vl-sort-descriptions-fn-of-vl-fundecllist-fix-fundecls
 (equal
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs packages configs
                            taskdecls (vl-fundecllist-fix fundecls)
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-fundecllist-equiv-congruence-on-fundecls

(defthm
 vl-sort-descriptions-fn-vl-fundecllist-equiv-congruence-on-fundecls
 (implies
  (vl-fundecllist-equiv fundecls fundecls-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs packages configs
                            taskdecls fundecls-equiv paramdecls
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-paramdecllist-fix-paramdecls

(defthm vl-sort-descriptions-fn-of-vl-paramdecllist-fix-paramdecls
 (equal
      (vl-sort-descriptions-fn x modules udps interfaces programs
                               packages configs taskdecls fundecls
                               (vl-paramdecllist-fix paramdecls)
                               imports fwdtypedefs typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-paramdecllist-equiv-congruence-on-paramdecls

(defthm
 vl-sort-descriptions-fn-vl-paramdecllist-equiv-congruence-on-paramdecls
 (implies
  (vl-paramdecllist-equiv paramdecls paramdecls-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules udps
                            interfaces programs packages configs
                            taskdecls fundecls paramdecls-equiv
                            imports fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-importlist-fix-imports

(defthm vl-sort-descriptions-fn-of-vl-importlist-fix-imports
 (equal
     (vl-sort-descriptions-fn x modules udps interfaces programs
                              packages configs taskdecls fundecls
                              paramdecls (vl-importlist-fix imports)
                              fwdtypedefs typedefs)
     (vl-sort-descriptions-fn x modules
                              udps interfaces programs packages
                              configs taskdecls fundecls paramdecls
                              imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-importlist-equiv-congruence-on-imports

(defthm
  vl-sort-descriptions-fn-vl-importlist-equiv-congruence-on-imports
 (implies
  (vl-importlist-equiv imports imports-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports-equiv fwdtypedefs typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-fwdtypedeflist-fix-fwdtypedefs

(defthm vl-sort-descriptions-fn-of-vl-fwdtypedeflist-fix-fwdtypedefs
 (equal
      (vl-sort-descriptions-fn x modules udps
                               interfaces programs packages configs
                               taskdecls fundecls paramdecls imports
                               (vl-fwdtypedeflist-fix fwdtypedefs)
                               typedefs)
      (vl-sort-descriptions-fn x modules
                               udps interfaces programs packages
                               configs taskdecls fundecls paramdecls
                               imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-fwdtypedeflist-equiv-congruence-on-fwdtypedefs

(defthm
 vl-sort-descriptions-fn-vl-fwdtypedeflist-equiv-congruence-on-fwdtypedefs
 (implies
  (vl-fwdtypedeflist-equiv fwdtypedefs fwdtypedefs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs-equiv typedefs)))
 :rule-classes :congruence)

Theorem: vl-sort-descriptions-fn-of-vl-typedeflist-fix-typedefs

(defthm vl-sort-descriptions-fn-of-vl-typedeflist-fix-typedefs
 (equal
    (vl-sort-descriptions-fn x modules udps interfaces
                             programs packages configs taskdecls
                             fundecls paramdecls imports fwdtypedefs
                             (vl-typedeflist-fix typedefs))
    (vl-sort-descriptions-fn x modules
                             udps interfaces programs packages
                             configs taskdecls fundecls paramdecls
                             imports fwdtypedefs typedefs)))

Theorem: vl-sort-descriptions-fn-vl-typedeflist-equiv-congruence-on-typedefs

(defthm
 vl-sort-descriptions-fn-vl-typedeflist-equiv-congruence-on-typedefs
 (implies
  (vl-typedeflist-equiv typedefs typedefs-equiv)
  (equal
   (vl-sort-descriptions-fn x modules udps interfaces programs
                            packages configs taskdecls fundecls
                            paramdecls imports fwdtypedefs typedefs)
   (vl-sort-descriptions-fn x modules
                            udps interfaces programs packages
                            configs taskdecls fundecls paramdecls
                            imports fwdtypedefs typedefs-equiv)))
 :rule-classes :congruence)