Split up complex subexpressions throughout an expression.
(vl-expr-split x elem delta) → (mv new-x delta)
We return a new, expression(-list) that is a replacement for
Theorem:
(defthm return-type-of-vl-expr-split.new-x (implies (and (force (vl-expr-p x)) (force (vl-modelement-p elem)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-expr-split x elem delta))) (vl-expr-p new-x))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expr-split.delta (implies (and (force (vl-expr-p x)) (force (vl-modelement-p elem)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-expr-split x elem delta))) (vl-delta-p delta))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-split.new-x (implies (and (force (vl-exprlist-p x)) (force (vl-modelement-p elem)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-exprlist-split x elem delta))) (and (vl-exprlist-p new-x) (equal (len new-x) (len x))))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-split.delta (implies (and (force (vl-exprlist-p x)) (force (vl-modelement-p elem)) (force (vl-delta-p delta))) (b* (((mv ?new-x ?delta) (vl-exprlist-split x elem delta))) (vl-delta-p delta))) :rule-classes :rewrite)