		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Fun-substp

Recognize function substitutions.

Signature
(fun-substp fsbs) → yes/no
Returns: yes/no — Type (booleanp yes/no).

A function substitution is an alist from function names to function names, with unique keys and with no trivial pairs.

Definitions and Theorems

Function: fun-substp

(defun fun-substp (fsbs)
  (declare (xargs :guard t))
  (let ((__function__ 'fun-substp))
    (declare (ignorable __function__))
    (and (symbol-symbol-alistp fsbs)
         (no-duplicatesp (alist-keys fsbs))
         (no-trivial-pairsp fsbs))))

Theorem: booleanp-of-fun-substp

(defthm booleanp-of-fun-substp
  (b* ((yes/no (fun-substp fsbs)))
    (booleanp yes/no))
  :rule-classes :rewrite)