(svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings) → constraints
Function:
(defun svtv-spec-fsm-constraints-for-lhprobe (lhprobe binding bindings) (declare (xargs :guard (and (lhprobe-p lhprobe) (svar/4vec-p binding) (lhprobe-map-p bindings)))) (let ((__function__ 'svtv-spec-fsm-constraints-for-lhprobe)) (declare (ignorable __function__)) (svar/4vec-case binding :4vec (list (make-lhprobe-constraint :lhprobe lhprobe :val (4vec-fix binding))) :svar (b* ((binding-look (hons-get (svar-fix binding) (lhprobe-map-fix bindings))) ((unless binding-look) (list (make-lhprobe-constraint :lhprobe lhprobe :val (4vec-x)))) (binding-lhprobe (cdr binding-look)) ((when (equal binding-lhprobe (lhprobe-fix lhprobe))) nil)) (list (make-lhprobe-constraint :lhprobe lhprobe :val binding-lhprobe))))))
Theorem:
(defthm lhprobe-constraintlist-p-of-svtv-spec-fsm-constraints-for-lhprobe (b* ((constraints (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings))) (lhprobe-constraintlist-p constraints)) :rule-classes :rewrite)
Theorem:
(defthm svtv-spec-fsm-constraints-for-lhprobe-of-lhprobe-fix-lhprobe (equal (svtv-spec-fsm-constraints-for-lhprobe (lhprobe-fix lhprobe) binding bindings) (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-lhprobe-lhprobe-equiv-congruence-on-lhprobe (implies (lhprobe-equiv lhprobe lhprobe-equiv) (equal (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings) (svtv-spec-fsm-constraints-for-lhprobe lhprobe-equiv binding bindings))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-constraints-for-lhprobe-of-svar/4vec-fix-binding (equal (svtv-spec-fsm-constraints-for-lhprobe lhprobe (svar/4vec-fix binding) bindings) (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-lhprobe-svar/4vec-equiv-congruence-on-binding (implies (svar/4vec-equiv binding binding-equiv) (equal (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings) (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding-equiv bindings))) :rule-classes :congruence)
Theorem:
(defthm svtv-spec-fsm-constraints-for-lhprobe-of-lhprobe-map-fix-bindings (equal (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding (lhprobe-map-fix bindings)) (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings)))
Theorem:
(defthm svtv-spec-fsm-constraints-for-lhprobe-lhprobe-map-equiv-congruence-on-bindings (implies (lhprobe-map-equiv bindings bindings-equiv) (equal (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings) (svtv-spec-fsm-constraints-for-lhprobe lhprobe binding bindings-equiv))) :rule-classes :congruence)