/usr/share/acl2-6.5/books/cgen/mv-proof.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 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 | #|$ACL2s-Preamble$;
(ld ;; Newline to fool ACL2/cert.pl dependency scanner
"portcullis.lsp")
(begin-book t);$ACL2s-Preamble$|#
(in-package "DEFDATA")
(defun my-mv-nth (n v)
(declare (xargs :guard nil))
(if (zp n)
(car v)
(my-mv-nth (- n 1) (cdr v))))
(defthm my-mv-nth--nil
(equal (my-mv-nth x nil)
nil))
(defthm my-mv-nth--reduce1
(implies (and (syntaxp (integerp n))
(integerp n)
(< 0 n))
(equal (my-mv-nth n v)
(my-mv-nth (- n 1) (cdr v)))))
(defthm my-mv-nth--reduce2
(implies (or (not (integerp n))
(<= n 0))
(equal (my-mv-nth n v)
(car v))))
; not by default
(defthmd mv-nth--to--my-mv-nth
(equal (mv-nth x y)
(my-mv-nth x y)))#|ACL2s-ToDo-Line|#
|