(svtv-outputs->outalist x phase) → outalist
Function:
(defun svtv-outputs->outalist (x phase) (declare (xargs :guard (and (svtv-lines-p x) (natp phase)))) (let ((__function__ 'svtv-outputs->outalist)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((svtv-line xf) (car x)) (ent (or (nth phase xf.entries) '_)) ((when (svtv-dontcare-p ent)) (svtv-outputs->outalist (cdr x) phase)) ((unless (svar-p ent)) (raise "Bad output entry: ~x0~%" ent) (svtv-outputs->outalist (cdr x) phase))) (cons (cons ent (lhs->svex-zero xf.lhs)) (svtv-outputs->outalist (cdr x) phase)))))
Theorem:
(defthm svex-alist-p-of-svtv-outputs->outalist (b* ((outalist (svtv-outputs->outalist x phase))) (svex-alist-p outalist)) :rule-classes :rewrite)
Theorem:
(defthm svtv-outputs->outalist-of-svtv-lines-fix-x (equal (svtv-outputs->outalist (svtv-lines-fix x) phase) (svtv-outputs->outalist x phase)))
Theorem:
(defthm svtv-outputs->outalist-svtv-lines-equiv-congruence-on-x (implies (svtv-lines-equiv x x-equiv) (equal (svtv-outputs->outalist x phase) (svtv-outputs->outalist x-equiv phase))) :rule-classes :congruence)
Theorem:
(defthm svtv-outputs->outalist-of-nfix-phase (equal (svtv-outputs->outalist x (nfix phase)) (svtv-outputs->outalist x phase)))
Theorem:
(defthm svtv-outputs->outalist-nat-equiv-congruence-on-phase (implies (nat-equiv phase phase-equiv) (equal (svtv-outputs->outalist x phase) (svtv-outputs->outalist x phase-equiv))) :rule-classes :congruence)