(vl-sort-clocking-block-items x idefaults odefaults clkassigns properties sequences) → (mv idefaults odefaults clkassigns properties sequences)
Function:
(defun vl-sort-clocking-block-items (x idefaults odefaults clkassigns properties sequences) (declare (xargs :guard (and (vl-clocking-block-item-list-p x) (vl-defaultskew-item-list-p idefaults) (vl-defaultskew-item-list-p odefaults) (vl-clkassignlist-p clkassigns) (vl-propertylist-p properties) (vl-sequencelist-p sequences)))) (let ((__function__ 'vl-sort-clocking-block-items)) (declare (ignorable __function__)) (if (atom x) (mv (vl-defaultskew-item-list-fix idefaults) (vl-defaultskew-item-list-fix odefaults) (vl-clkassignlist-fix clkassigns) (vl-propertylist-fix properties) (vl-sequencelist-fix sequences)) (let* ((item (car x)) (tag (tag item))) (vl-sort-clocking-block-items (cdr x) (if (and (eq tag :vl-defaultskew) (vl-defaultskew-item->inputp item)) (cons item idefaults) idefaults) (if (and (eq tag :vl-defaultskew) (not (vl-defaultskew-item->inputp item))) (cons item odefaults) odefaults) (if (eq tag :vl-clkassign) (cons item clkassigns) clkassigns) (if (eq tag :vl-property) (cons item properties) properties) (if (eq tag :vl-sequence) (cons item sequences) sequences))))))
Theorem:
(defthm vl-defaultskew-item-list-p-of-vl-sort-clocking-block-items.idefaults (b* (((mv ?idefaults ?odefaults ?clkassigns ?properties ?sequences) (vl-sort-clocking-block-items x idefaults odefaults clkassigns properties sequences))) (vl-defaultskew-item-list-p idefaults)) :rule-classes :rewrite)
Theorem:
(defthm vl-defaultskew-item-list-p-of-vl-sort-clocking-block-items.odefaults (b* (((mv ?idefaults ?odefaults ?clkassigns ?properties ?sequences) (vl-sort-clocking-block-items x idefaults odefaults clkassigns properties sequences))) (vl-defaultskew-item-list-p odefaults)) :rule-classes :rewrite)
Theorem:
(defthm vl-clkassignlist-p-of-vl-sort-clocking-block-items.clkassigns (b* (((mv ?idefaults ?odefaults ?clkassigns ?properties ?sequences) (vl-sort-clocking-block-items x idefaults odefaults clkassigns properties sequences))) (vl-clkassignlist-p clkassigns)) :rule-classes :rewrite)
Theorem:
(defthm vl-propertylist-p-of-vl-sort-clocking-block-items.properties (b* (((mv ?idefaults ?odefaults ?clkassigns ?properties ?sequences) (vl-sort-clocking-block-items x idefaults odefaults clkassigns properties sequences))) (vl-propertylist-p properties)) :rule-classes :rewrite)
Theorem:
(defthm vl-sequencelist-p-of-vl-sort-clocking-block-items.sequences (b* (((mv ?idefaults ?odefaults ?clkassigns ?properties ?sequences) (vl-sort-clocking-block-items x idefaults odefaults clkassigns properties sequences))) (vl-sequencelist-p sequences)) :rule-classes :rewrite)