(vl-collect-exprs-for-implicit-wires-from-namedargs x) → (mv main other)
Function:
(defun vl-collect-exprs-for-implicit-wires-from-namedargs (x) (declare (xargs :guard (vl-namedarglist-p x))) (let ((__function__ 'vl-collect-exprs-for-implicit-wires-from-namedargs)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv main1 other1) (vl-collect-exprs-for-implicit-wires-from-namedarg (car x))) ((mv main2 other2) (vl-collect-exprs-for-implicit-wires-from-namedargs (cdr x)))) (mv (append main1 main2) (append other1 other2)))))
Theorem:
(defthm vl-exprlist-p-of-vl-collect-exprs-for-implicit-wires-from-namedargs.main (b* (((mv ?main ?other) (vl-collect-exprs-for-implicit-wires-from-namedargs x))) (vl-exprlist-p main)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-p-of-vl-collect-exprs-for-implicit-wires-from-namedargs.other (b* (((mv ?main ?other) (vl-collect-exprs-for-implicit-wires-from-namedargs x))) (vl-exprlist-p other)) :rule-classes :rewrite)
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedargs-mvtypes-0 (true-listp (mv-nth 0 (vl-collect-exprs-for-implicit-wires-from-namedargs x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedargs-mvtypes-1 (true-listp (mv-nth 1 (vl-collect-exprs-for-implicit-wires-from-namedargs x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedargs-complete (b* (((mv main other) (vl-collect-exprs-for-implicit-wires-from-namedargs x))) (set-equiv (append main other) (vl-namedarglist-allexprs x))))
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedargs-of-vl-namedarglist-fix-x (equal (vl-collect-exprs-for-implicit-wires-from-namedargs (vl-namedarglist-fix x)) (vl-collect-exprs-for-implicit-wires-from-namedargs x)))
Theorem:
(defthm vl-collect-exprs-for-implicit-wires-from-namedargs-vl-namedarglist-equiv-congruence-on-x (implies (vl-namedarglist-equiv x x-equiv) (equal (vl-collect-exprs-for-implicit-wires-from-namedargs x) (vl-collect-exprs-for-implicit-wires-from-namedargs x-equiv))) :rule-classes :congruence)