where alist is a symbol-alistp and w is an ACL2 logical
world. The alist is presumed to pair :logic-mode function
symbols with arities. The result is t or nil according to whether
each symbol in the alist is a :logic-mode function symbol with the
associated arity as its arity in w. See well-formedness-guarantee.