GCL (GNU Common Lisp) Version(2.5.0) Tue Aug 27 18:02:58 CDT 2002 Licensed under GNU Library General Public License Contains Enhancements by W. Schelter ACL2 Version 2.7 built November 14, 2002 10:53:25. Copyright (C) 2002 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* T). See the documentation topic note-2-7 for recent changes. NOTE!! Proof trees are disabled in ACL2. To enable them in emacs, look under the ACL2 source directory in interface/emacs/README.doc; and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 command loop. Look in the ACL2 documentation under PROOF-TREE. Loading /v/filer1b/v0q004/moore/acl2-init.lsp Finished loading /v/filer1b/v0q004/moore/acl2-init.lsp ACL2 Version 2.7. Level 1. Cbd "/v/net2/v2/users/prof/moore/publications/trecia/support/". Type :help for help. ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT) ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2> ACL2 Version 2.7. Level 1. Cbd "/v/net2/v2/users/prof/moore/publications/trecia/support/". Type :help for help. ACL2 !> ACL2 Version 2.7. Level 2. Cbd "/v/net2/v2/users/prof/moore/publications/trecia/support/". Type :help for help. ACL2 !>> (PROVE PROOF-TREE WARNING OBSERVATION EVENT) ACL2 !>>:INVISIBLE Summary Form: ( DEFUN TEST ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) TEST Summary Form: ( ENCAPSULATE ((TEST ...) ...) ...) Rules: NIL Warnings: None Time: 0.06 seconds (prove: 0.00, print: 0.00, other: 0.06) T :INVISIBLE Summary Form: ( DEFUN BASE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) BASE Summary Form: ( ENCAPSULATE ((BASE ...) ...) ...) Rules: NIL Warnings: None Time: 0.06 seconds (prove: 0.00, print: 0.00, other: 0.06) T :INVISIBLE Summary Form: ( DEFUN ST ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ST Summary Form: ( ENCAPSULATE ((ST ...) ...) ...) Rules: NIL Warnings: None Time: 0.06 seconds (prove: 0.00, print: 0.00, other: 0.06) T Summary Form: ( DEFUN STN ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) STN Summary Form: ( DEFCHOOSE FCH ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FCH Summary Form: ( DEFUN FN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION E0-ORD-<) (:DEFINITION E0-ORDINALP) (:DEFINITION NFIX) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) FN Summary Form: ( DEFUN F ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) F Summary Form: ( DEFTHM TEST-FCH ...) Rules: ((:DEFINITION NOT) (:DEFINITION STN) (:EXECUTABLE-COUNTERPART ZP)) Warnings: None Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.02) TEST-FCH Summary Form: ( DEFTHM TEST-F-DEF ...) Rules: ((:DEFINITION F) (:DEFINITION FN) (:DEFINITION NOT) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE TEST-FCH) (:REWRITE ZP-OPEN)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) TEST-F-DEF Summary Form: ( DEFTHM OPEN-STN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION STN) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.02) OPEN-STN [SGC for 618 CONS pages..(3094 writable)..(T=7).GC finished] Summary Form: ( DEFTHM |+1-1| ...) Rules: ((:DEFINITION FIX) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIX) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DEFAULT-+-2)) Warnings: None Time: 0.09 seconds (prove: 0.08, print: 0.00, other: 0.01) |+1-1| Summary Form: ( DEFTHM ST-STN-FCH ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION FIX) (:DEFINITION NFIX) (:DEFINITION NOT) (:DEFINITION STN) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE |+1-1|) (:REWRITE OPEN-STN)) Warnings: None Time: 0.05 seconds (prove: 0.01, print: 0.00, other: 0.04) ST-STN-FCH Summary Form: ( DEFTHM TEST-NIL-FCH ...) Rules: ((:DEFINITION IFF) (:DEFINITION NOT) (:DEFINITION STN) (:DEFINITION SYNP) (:FORWARD-CHAINING ST-STN-FCH) (:REWRITE ZP-OPEN)) Warnings: None Time: 0.04 seconds (prove: 0.02, print: 0.00, other: 0.02) TEST-NIL-FCH Summary Form: ( DEFTHM FN-ST ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION FN) (:DEFINITION STN) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE OPEN-STN)) Warnings: None Time: 0.04 seconds (prove: 0.03, print: 0.00, other: 0.01) FN-ST Summary Form: ( DEFTHM GENERIC-TAIL-RECURSIVE-F ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION F) (:DEFINITION FN) (:DEFINITION NOT) (:DEFINITION STN) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE OPEN-STN) (:REWRITE TEST-FCH) (:REWRITE TEST-NIL-FCH) (:REWRITE ZP-OPEN)) Warnings: None Time: 0.04 seconds (prove: 0.03, print: 0.00, other: 0.01) GENERIC-TAIL-RECURSIVE-F Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: None Time: 0.35 seconds (prove: 0.19, print: 0.00, other: 0.16) T Summary Form: ( DEFUN ARITY-1-TAIL-RECURSIVE-ENCAP ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ARITY-1-TAIL-RECURSIVE-ENCAP Summary Form: ( DEFUN PROBABLY-TAIL-RECURSIVEP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) PROBABLY-TAIL-RECURSIVEP Summary Form: ( DEFUN DESTRUCTURE-TAIL-RECURSION-AUX ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) DESTRUCTURE-TAIL-RECURSION-AUX Summary Form: ( DEFUN DESTRUCTURE-TAIL-RECURSION ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) DESTRUCTURE-TAIL-RECURSION Summary Form: ( DEFUN ARBITRARY-TAIL-RECURSIVE-ENCAP ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ARBITRARY-TAIL-RECURSIVE-ENCAP Summary Form: ( DEFUN REMOVE-XARGS-DOMAIN-AND-MEASURE ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) REMOVE-XARGS-DOMAIN-AND-MEASURE Summary Form: ( MUTUAL-RECURSION ( DEFUN SUBST-FN-INTO-PSEUDO-TERM ...) ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) (SUBST-FN-INTO-PSEUDO-TERM SUBST-FN-INTO-PSEUDO-BINDINGS SUBST-FN-INTO-PSEUDO-COND-CLAUSES SUBST-FN-INTO-PSEUDO-TERM-LIST) Summary Form: ( DEFUN DEFAULT-DEFPUN-RULE-CLASSES ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DEFAULT-DEFPUN-RULE-CLASSES Summary Form: ( DEFUN DESTRUCTURE-DCL-BODY-KEYPAIRS ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) DESTRUCTURE-DCL-BODY-KEYPAIRS Summary Form: ( DEFUN DEFPUN-SYNTAX-ER ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) DEFPUN-SYNTAX-ER Summary Form: ( DEFMACRO DEFPUN ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) DEFPUN [SGC for 618 CONS pages..(3099 writable)..(T=8).GC finished] Summary Form: ( INCLUDE-BOOK "defpun" ...) Rules: NIL Warnings: None Time: 0.39 seconds (prove: 0.00, print: 0.00, other: 0.39) Compiling /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.lisp. End of Pass 1. ;; Note: Tail-recursive call of STN was replaced by iteration. ;; Note: Tail-recursive call of FN was replaced by iteration.[SGC for 618 CONS pages..(3120 writable)..(T=9).GC finished] End of Pass 2. OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3 Finished compiling /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o. "/v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o" Loading /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o start address -T 0x97fa000 Finished loading /v/net2/v2/users/prof/moore/publications/trecia/support/defpun.o Summary Form: (CERTIFY-BOOK "defpun" ...) Rules: NIL Warnings: None Time: 1.27 seconds (prove: 0.20, print: 0.01, other: 1.06) "/v/net2/v2/users/prof/moore/publications/trecia/support/defpun.lisp" ACL2 !>>Bye. :EOF ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2>