Core routine for introducing
(vl-expr-resolve-indexing-aux x ss warnings) → (mv new-warnings changedp new-x)
Theorem:
(defthm return-type-of-vl-expr-resolve-indexing-aux.new-warnings (b* (((mv ?new-warnings ?changedp ?new-x) (vl-expr-resolve-indexing-aux x ss warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expr-resolve-indexing-aux.changedp (b* (((mv ?new-warnings ?changedp ?new-x) (vl-expr-resolve-indexing-aux x ss warnings))) (booleanp changedp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-expr-resolve-indexing-aux.new-x (b* (((mv ?new-warnings ?changedp ?new-x) (vl-expr-resolve-indexing-aux x ss warnings))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-resolve-indexing-aux.new-warnings (b* (((mv ?new-warnings ?changedp ?new-x) (vl-exprlist-resolve-indexing-aux x ss warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-resolve-indexing-aux.changedp (b* (((mv ?new-warnings ?changedp ?new-x) (vl-exprlist-resolve-indexing-aux x ss warnings))) (booleanp changedp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-exprlist-resolve-indexing-aux.new-x (b* (((mv ?new-warnings ?changedp ?new-x) (vl-exprlist-resolve-indexing-aux x ss warnings))) (and (vl-exprlist-p new-x) (equal (len new-x) (len x)))) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-exprlist-resolve-indexing-aux (b* (((mv ?warnings ?changedp new-x) (vl-exprlist-resolve-indexing-aux x ss warnings))) (true-listp new-x)) :rule-classes :type-prescription)
Theorem:
(defthm vl-expr-resolve-indexing-aux-of-vl-expr-fix-x (equal (vl-expr-resolve-indexing-aux (vl-expr-fix x) ss warnings) (vl-expr-resolve-indexing-aux x ss warnings)))
Theorem:
(defthm vl-expr-resolve-indexing-aux-of-vl-scopestack-fix-ss (equal (vl-expr-resolve-indexing-aux x (vl-scopestack-fix ss) warnings) (vl-expr-resolve-indexing-aux x ss warnings)))
Theorem:
(defthm vl-expr-resolve-indexing-aux-of-vl-warninglist-fix-warnings (equal (vl-expr-resolve-indexing-aux x ss (vl-warninglist-fix warnings)) (vl-expr-resolve-indexing-aux x ss warnings)))
Theorem:
(defthm vl-exprlist-resolve-indexing-aux-of-vl-exprlist-fix-x (equal (vl-exprlist-resolve-indexing-aux (vl-exprlist-fix x) ss warnings) (vl-exprlist-resolve-indexing-aux x ss warnings)))
Theorem:
(defthm vl-exprlist-resolve-indexing-aux-of-vl-scopestack-fix-ss (equal (vl-exprlist-resolve-indexing-aux x (vl-scopestack-fix ss) warnings) (vl-exprlist-resolve-indexing-aux x ss warnings)))
Theorem:
(defthm vl-exprlist-resolve-indexing-aux-of-vl-warninglist-fix-warnings (equal (vl-exprlist-resolve-indexing-aux x ss (vl-warninglist-fix warnings)) (vl-exprlist-resolve-indexing-aux x ss warnings)))
Theorem:
(defthm vl-expr-resolve-indexing-aux-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-resolve-indexing-aux x ss warnings) (vl-expr-resolve-indexing-aux x-equiv ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-resolve-indexing-aux-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-expr-resolve-indexing-aux x ss warnings) (vl-expr-resolve-indexing-aux x ss-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-resolve-indexing-aux-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-expr-resolve-indexing-aux x ss warnings) (vl-expr-resolve-indexing-aux x ss warnings-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-resolve-indexing-aux-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-exprlist-resolve-indexing-aux x ss warnings) (vl-exprlist-resolve-indexing-aux x-equiv ss warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-resolve-indexing-aux-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-exprlist-resolve-indexing-aux x ss warnings) (vl-exprlist-resolve-indexing-aux x ss-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-resolve-indexing-aux-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-exprlist-resolve-indexing-aux x ss warnings) (vl-exprlist-resolve-indexing-aux x ss warnings-equiv))) :rule-classes :congruence)