(vttree-constraints-to-svstmts x) → svstmts
Function:
(defun vttree-constraints-to-svstmts (x) (declare (xargs :guard (vttree-p x))) (let ((__function__ 'vttree-constraints-to-svstmts)) (declare (ignorable __function__)) (b* ((constraints (vttree->constraints x))) (if (atom constraints) nil (list (sv::make-svstmt-constraints :constraints constraints))))))
Theorem:
(defthm svstmtlist-p-of-vttree-constraints-to-svstmts (b* ((svstmts (vttree-constraints-to-svstmts x))) (sv::svstmtlist-p svstmts)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vttree-constraints-to-svstmts (b* ((?svstmts (vttree-constraints-to-svstmts x))) (implies (not (member v (sv::constraintlist-vars (vttree->constraints x)))) (not (member v (sv::svstmtlist-vars svstmts))))))
Theorem:
(defthm vttree-constraints-to-svstmts-of-vttree-fix-x (equal (vttree-constraints-to-svstmts (vttree-fix x)) (vttree-constraints-to-svstmts x)))
Theorem:
(defthm vttree-constraints-to-svstmts-vttree-equiv-congruence-on-x (implies (vttree-equiv x x-equiv) (equal (vttree-constraints-to-svstmts x) (vttree-constraints-to-svstmts x-equiv))) :rule-classes :congruence)