/usr/share/acl2-6.5/books/system/verified-termination-and-guards.lisp is in acl2-books-source 6.5-2.
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 | ; Copyright (C) 2014, Regents of the University of Texas
; Written by David Rager (original date April, 2012)
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
(in-package "ACL2")
; This books serves as a place to verify the termination and guards of ACL2
; system functions. A user may wish to include this book or system/top.lisp
; when reasoning about system functions.
; Note that calling verify-termination also verifies the guards of any function
; that has a guard specified. In the event that there is no guard specified,
; then one must also call verify-guards to verify that the implicit guard of
; "t" is strong enough. See :doc verify-termination for further details.
; (verify-termination fmt-char) ; and guards
; (verify-termination fmt-var) ; and guards
(verify-termination missing-fmt-alist-chars1) ; and guards
(verify-termination missing-fmt-alist-chars) ; and guards
|