other
(in-package "ACL2")
local
(local (in-theory (disable member-equal)))
other
(verify-termination legal-variablep)
other
(verify-termination arglistp1)
other
(verify-termination arglistp)
other
(verify-termination lambda-keywordp)
other
(verify-guards legal-variablep)
other
(verify-guards arglistp1)
other
(verify-guards arglistp)
other
(verify-guards lambda-keywordp)
other
(verify-termination legal-constantp (declare (xargs :verify-guards t)))
other
(verify-termination find-first-bad-arg (declare (xargs :verify-guards nil)))
symbolp-when-legal-variableptheorem
(defthm symbolp-when-legal-variablep (implies (legal-variablep x) (and (symbolp x) (not (equal x t)) (not (equal x nil)))) :rule-classes :compound-recognizer)
local
(local (defthm find-first-bad-arg-lemma-lemma (implies (and (character-listp x) (atom (cdr x)) (equal (car x) #\&)) (equal "&" (coerce x 'string))) :rule-classes nil))
local
(local (defthm find-first-bad-arg-lemma (implies (and (not (equal "&" s)) (equal (car (coerce s 'list)) #\&) (stringp s)) (consp (cdr (coerce s 'list)))) :hints (("Goal" :use ((:instance find-first-bad-arg-lemma-lemma (x (coerce s 'list))))))))
other
(verify-guards find-first-bad-arg :hints (("Goal" :in-theory (enable string< string<-l))))