(svcall-join operator args) → svex
Function:
(defun svcall-join (operator args) (declare (xargs :guard (sv::svexlist-p args))) (declare (xargs :guard (and (assoc operator sv::*svex-op-table*) (consp args)))) (let ((__function__ 'svcall-join)) (declare (ignorable __function__)) (if (atom (cdr args)) (sv::svex-fix (car args)) (sv::svex-call operator (list (car args) (svcall-join operator (cdr args)))))))
Theorem:
(defthm svex-p-of-svcall-join (b* ((svex (svcall-join operator args))) (sv::svex-p svex)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-svcall-join (b* ((?svex (svcall-join operator args))) (implies (not (member v (sv::svexlist-vars args))) (not (member v (sv::svex-vars svex))))))
Theorem:
(defthm svcall-join-of-svexlist-fix-args (equal (svcall-join operator (sv::svexlist-fix args)) (svcall-join operator args)))
Theorem:
(defthm svcall-join-svexlist-equiv-congruence-on-args (implies (sv::svexlist-equiv args args-equiv) (equal (svcall-join operator args) (svcall-join operator args-equiv))) :rule-classes :congruence)