(vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) → (mv portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)
Function:
(defun vl-sort-genelements-aux (x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (declare (xargs :guard (and (vl-genelementlist-p x) (vl-portdecllist-p portdecls) (vl-assignlist-p assigns) (vl-aliaslist-p aliases) (vl-vardecllist-p vardecls) (vl-paramdecllist-p paramdecls) (vl-fundecllist-p fundecls) (vl-taskdecllist-p taskdecls) (vl-modinstlist-p modinsts) (vl-gateinstlist-p gateinsts) (vl-alwayslist-p alwayses) (vl-initiallist-p initials) (vl-typedeflist-p typedefs) (vl-importlist-p imports) (vl-fwdtypedeflist-p fwdtypedefs) (vl-modportlist-p modports) (vl-genvarlist-p genvars) (vl-genelementlist-p generates)))) (let ((__function__ 'vl-sort-genelements-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv (rev (vl-portdecllist-fix portdecls)) (rev (vl-assignlist-fix assigns)) (rev (vl-aliaslist-fix aliases)) (rev (vl-vardecllist-fix vardecls)) (rev (vl-paramdecllist-fix paramdecls)) (rev (vl-fundecllist-fix fundecls)) (rev (vl-taskdecllist-fix taskdecls)) (rev (vl-modinstlist-fix modinsts)) (rev (vl-gateinstlist-fix gateinsts)) (rev (vl-alwayslist-fix alwayses)) (rev (vl-initiallist-fix initials)) (rev (vl-typedeflist-fix typedefs)) (rev (vl-importlist-fix imports)) (rev (vl-fwdtypedeflist-fix fwdtypedefs)) (rev (vl-modportlist-fix modports)) (rev (vl-genvarlist-fix genvars)) (vl-genelementlist-fix generates))) (xf (car x))) (vl-genelement-case xf :vl-genbase (b* ((x1 xf.item) (tag (tag x1))) (vl-sort-genelements-aux (cdr x) (if (eq tag :vl-portdecl) (cons x1 portdecls) portdecls) (if (eq tag :vl-assign) (cons x1 assigns) assigns) (if (eq tag :vl-alias) (cons x1 aliases) aliases) (if (eq tag :vl-vardecl) (cons x1 vardecls) vardecls) (if (eq tag :vl-paramdecl) (cons x1 paramdecls) paramdecls) (if (eq tag :vl-fundecl) (cons x1 fundecls) fundecls) (if (eq tag :vl-taskdecl) (cons x1 taskdecls) taskdecls) (if (eq tag :vl-modinst) (cons x1 modinsts) modinsts) (if (eq tag :vl-gateinst) (cons x1 gateinsts) gateinsts) (if (eq tag :vl-always) (cons x1 alwayses) alwayses) (if (eq tag :vl-initial) (cons x1 initials) initials) (if (eq tag :vl-typedef) (cons x1 typedefs) typedefs) (if (eq tag :vl-import) (cons x1 imports) imports) (if (eq tag :vl-fwdtypedef) (cons x1 fwdtypedefs) fwdtypedefs) (if (eq tag :vl-modport) (cons x1 modports) modports) (if (eq tag :vl-genvar) (cons x1 genvars) genvars) generates)) :otherwise (vl-sort-genelements-aux (cdr x) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars (cons (vl-genelement-fix (car x)) generates))))))
Theorem:
(defthm vl-portdecllist-p-of-vl-sort-genelements-aux.portdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-portdecllist-p portdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-sort-genelements-aux.assigns (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm vl-aliaslist-p-of-vl-sort-genelements-aux.aliases (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-aliaslist-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm vl-vardecllist-p-of-vl-sort-genelements-aux.vardecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-paramdecllist-p-of-vl-sort-genelements-aux.paramdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-paramdecllist-p paramdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-fundecllist-p-of-vl-sort-genelements-aux.fundecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-fundecllist-p fundecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-taskdecllist-p-of-vl-sort-genelements-aux.taskdecls (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-taskdecllist-p taskdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-modinstlist-p-of-vl-sort-genelements-aux.modinsts (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-modinstlist-p modinsts)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist-p-of-vl-sort-genelements-aux.gateinsts (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-gateinstlist-p gateinsts)) :rule-classes :rewrite)
Theorem:
(defthm vl-alwayslist-p-of-vl-sort-genelements-aux.alwayses (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-alwayslist-p alwayses)) :rule-classes :rewrite)
Theorem:
(defthm vl-initiallist-p-of-vl-sort-genelements-aux.initials (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-initiallist-p initials)) :rule-classes :rewrite)
Theorem:
(defthm vl-typedeflist-p-of-vl-sort-genelements-aux.typedefs (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-typedeflist-p typedefs)) :rule-classes :rewrite)
Theorem:
(defthm vl-importlist-p-of-vl-sort-genelements-aux.imports (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-importlist-p imports)) :rule-classes :rewrite)
Theorem:
(defthm vl-fwdtypedeflist-p-of-vl-sort-genelements-aux.fwdtypedefs (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-fwdtypedeflist-p fwdtypedefs)) :rule-classes :rewrite)
Theorem:
(defthm vl-modportlist-p-of-vl-sort-genelements-aux.modports (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-modportlist-p modports)) :rule-classes :rewrite)
Theorem:
(defthm vl-genvarlist-p-of-vl-sort-genelements-aux.genvars (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-genvarlist-p genvars)) :rule-classes :rewrite)
Theorem:
(defthm vl-genelementlist-p-of-vl-sort-genelements-aux.generates (b* (((mv ?portdecls ?assigns ?aliases ?vardecls ?paramdecls ?fundecls ?taskdecls ?modinsts ?gateinsts ?alwayses ?initials ?typedefs ?imports ?fwdtypedefs ?modports ?genvars ?generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) (vl-genelementlist-p generates)) :rule-classes :rewrite)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-genelementlist-fix-x (equal (vl-sort-genelements-aux (vl-genelementlist-fix x) portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-genelementlist-equiv-congruence-on-x (implies (vl-genelementlist-equiv x x-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x-equiv portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-portdecllist-fix-portdecls (equal (vl-sort-genelements-aux x (vl-portdecllist-fix portdecls) assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-portdecllist-equiv-congruence-on-portdecls (implies (vl-portdecllist-equiv portdecls portdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls-equiv assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-assignlist-fix-assigns (equal (vl-sort-genelements-aux x portdecls (vl-assignlist-fix assigns) aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-assignlist-equiv-congruence-on-assigns (implies (vl-assignlist-equiv assigns assigns-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns-equiv aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-aliaslist-fix-aliases (equal (vl-sort-genelements-aux x portdecls assigns (vl-aliaslist-fix aliases) vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-aliaslist-equiv-congruence-on-aliases (implies (vl-aliaslist-equiv aliases aliases-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases-equiv vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-vardecllist-fix-vardecls (equal (vl-sort-genelements-aux x portdecls assigns aliases (vl-vardecllist-fix vardecls) paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-vardecllist-equiv-congruence-on-vardecls (implies (vl-vardecllist-equiv vardecls vardecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls-equiv paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-paramdecllist-fix-paramdecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls (vl-paramdecllist-fix paramdecls) fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-paramdecllist-equiv-congruence-on-paramdecls (implies (vl-paramdecllist-equiv paramdecls paramdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls-equiv fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-fundecllist-fix-fundecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls (vl-fundecllist-fix fundecls) taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-fundecllist-equiv-congruence-on-fundecls (implies (vl-fundecllist-equiv fundecls fundecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls-equiv taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-taskdecllist-fix-taskdecls (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls (vl-taskdecllist-fix taskdecls) modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-taskdecllist-equiv-congruence-on-taskdecls (implies (vl-taskdecllist-equiv taskdecls taskdecls-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls-equiv modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-modinstlist-fix-modinsts (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls (vl-modinstlist-fix modinsts) gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-modinstlist-equiv-congruence-on-modinsts (implies (vl-modinstlist-equiv modinsts modinsts-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts-equiv gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-gateinstlist-fix-gateinsts (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts (vl-gateinstlist-fix gateinsts) alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-gateinstlist-equiv-congruence-on-gateinsts (implies (vl-gateinstlist-equiv gateinsts gateinsts-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts-equiv alwayses initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-alwayslist-fix-alwayses (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts (vl-alwayslist-fix alwayses) initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-alwayslist-equiv-congruence-on-alwayses (implies (vl-alwayslist-equiv alwayses alwayses-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses-equiv initials typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-initiallist-fix-initials (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses (vl-initiallist-fix initials) typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-initiallist-equiv-congruence-on-initials (implies (vl-initiallist-equiv initials initials-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials-equiv typedefs imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-typedeflist-fix-typedefs (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials (vl-typedeflist-fix typedefs) imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-typedeflist-equiv-congruence-on-typedefs (implies (vl-typedeflist-equiv typedefs typedefs-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs-equiv imports fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-importlist-fix-imports (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs (vl-importlist-fix imports) fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-importlist-equiv-congruence-on-imports (implies (vl-importlist-equiv imports imports-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports-equiv fwdtypedefs modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-fwdtypedeflist-fix-fwdtypedefs (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports (vl-fwdtypedeflist-fix fwdtypedefs) modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-fwdtypedeflist-equiv-congruence-on-fwdtypedefs (implies (vl-fwdtypedeflist-equiv fwdtypedefs fwdtypedefs-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs-equiv modports genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-modportlist-fix-modports (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs (vl-modportlist-fix modports) genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-modportlist-equiv-congruence-on-modports (implies (vl-modportlist-equiv modports modports-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports-equiv genvars generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-genvarlist-fix-genvars (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports (vl-genvarlist-fix genvars) generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-genvarlist-equiv-congruence-on-genvars (implies (vl-genvarlist-equiv genvars genvars-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars-equiv generates))) :rule-classes :congruence)
Theorem:
(defthm vl-sort-genelements-aux-of-vl-genelementlist-fix-generates (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars (vl-genelementlist-fix generates)) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates)))
Theorem:
(defthm vl-sort-genelements-aux-vl-genelementlist-equiv-congruence-on-generates (implies (vl-genelementlist-equiv generates generates-equiv) (equal (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates) (vl-sort-genelements-aux x portdecls assigns aliases vardecls paramdecls fundecls taskdecls modinsts gateinsts alwayses initials typedefs imports fwdtypedefs modports genvars generates-equiv))) :rule-classes :congruence)