/usr/share/acl2-8.0dfsg/books/system/all-ffn-symbs-logic.lisp is in acl2-books-source 8.0dfsg-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 | (in-package "ACL2")
(verify-termination all-ffn-symbs
(declare (xargs :verify-guards nil))) ; and all-ffn-symbs-lst
(defun all-ffn-symbs-flg (flg x ans)
(cond
(flg (cond ((endp x) ans)
(t (all-ffn-symbs-flg t (cdr x)
(all-ffn-symbs-flg nil (car x) ans)))))
((variablep x) ans)
((fquotep x) ans)
(t (all-ffn-symbs-flg
t
(fargs x)
(cond ((flambda-applicationp x)
(all-ffn-symbs-flg nil (lambda-body (ffn-symb x)) ans))
(t (add-to-set-eq (ffn-symb x) ans)))))))
(defthm symbol-listp-all-ffn-symbs-flg
(implies (and (symbol-listp ans)
(if flg (pseudo-term-listp x) (pseudo-termp x)))
(symbol-listp (all-ffn-symbs-flg flg x ans)))
:rule-classes nil)
(defthm all-ffn-symbs-flg-is-all-ffn-symbs
(equal (all-ffn-symbs-flg flg x ans)
(if flg
(all-ffn-symbs-lst x ans)
(all-ffn-symbs x ans))))
(defthm symbol-listp-all-ffn-symbs
(implies (and (symbol-listp ans)
(pseudo-termp x))
(symbol-listp (all-ffn-symbs x ans)))
:hints (("Goal" :use ((:instance symbol-listp-all-ffn-symbs-flg
(flg nil))))))
(defthm symbol-listp-all-ffn-symbs-lst
(implies (and (symbol-listp ans)
(pseudo-term-listp x))
(symbol-listp (all-ffn-symbs-lst x ans)))
:hints (("Goal" :use ((:instance symbol-listp-all-ffn-symbs-flg
(flg t))))))
(verify-guards all-ffn-symbs
:hints (("Goal" :use all-ffn-symbs-flg-is-all-ffn-symbs)))
|