GCL (GNU Common Lisp)  2.6.6 CLtL1    Jan 19 2005 20:24:14
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License:  GPL due to GPL'ed components: (BFD UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter

Use (help) to get some basic information on how to use GCL.

 ACL2 Version 2.9.3 built August 2, 2005  18:40:53.
 Copyright (C) 2005  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*
                      NIL).
 See the documentation topic note-2-9-3 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

 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.

ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
ACL2>
#<"ACL2" package>

ACL2>
ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>
ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
ACL2 Version 2.9.3.  Level 2.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>>
Summary
Form:  ( DEFPKG "INSTANCE" ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 "INSTANCE"
ACL2 !>>
Summary
Form:  ( DEFPKG "COMPUTED-HINTS" ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "COMPUTED-HINTS"
ACL2 !>>[SGC for 444 CONS pages..(8302 writable)..(T=1).GC finished]

Summary
Form:  ( DEFPKG "SETS" ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "SETS"
ACL2 !>>Bye.
 :EOF
ACL2 !>[SGC for 12 STRING pages..(8304 writable)..(T=0).GC finished]
:INVISIBLE

Summary
Form:  ( DEFUN INSTANCE-VARIABLEP ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE-VARIABLEP

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN INSTANCE-UNIFY-TERM ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(INSTANCE-UNIFY-TERM INSTANCE-UNIFY-LIST)
[SGC for 12 STRING pages..(8306 writable)..(T=1).GC finished]

Summary
Form:  ( DEFUN INSTANCE-SUBSTITUTE ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
INSTANCE-SUBSTITUTE

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN INSTANCE-REWRITE1 ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(INSTANCE-REWRITE1 INSTANCE-REWRITE-LST1)

Summary
Form:  ( DEFUN INSTANCE-REWRITE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE-REWRITE

Summary
Form:  ( DEFUN INSTANCE-DECLS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE-DECLS

Summary
Form:  ( DEFUN INSTANCE-DEFUN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE-DEFUN

Summary
Form:  ( DEFUN INSTANCE-DEFUNS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE-DEFUNS

Summary
Form:  ( DEFUN DEFTHM-NAMES ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
DEFTHM-NAMES

Summary
Form:  ( DEFUN CREATE-NEW-NAMES ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CREATE-NEW-NAMES

Summary
Form:  ( DEFUN RENAME-DEFTHMS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
RENAME-DEFTHMS

Summary
Form:  ( DEFUN SUB-TO-LAMBDA ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUB-TO-LAMBDA

Summary
Form:  ( DEFUN SUBS-TO-LAMBDAS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBS-TO-LAMBDAS

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN TERM-FUNCTIONS ...) ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
(TERM-FUNCTIONS TERM-LIST-FUNCTIONS)

Summary
Form:  ( DEFUN SUBS-REPL-FUNCTIONS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBS-REPL-FUNCTIONS

Summary
Form:  ( DEFUN FUNCTION-LIST-TO-DEFINITIONS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FUNCTION-LIST-TO-DEFINITIONS

Summary
Form:  ( DEFUN SUBS-TO-DEFS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBS-TO-DEFS

Summary
Form:  ( DEFCONST *DEFAULT-PARSE-VALUES* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*DEFAULT-PARSE-VALUES*

Summary
Form:  ( DEFUN PARSE-DEFTHM-OPTION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PARSE-DEFTHM-OPTION

Summary
Form:  ( DEFUN PARSE-DEFTHM-OPTIONS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PARSE-DEFTHM-OPTIONS

Summary
Form:  ( DEFUN INSTANCE-DEFTHM ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
INSTANCE-DEFTHM

Summary
Form:  ( DEFUN INSTANCE-SIGNATURE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE-SIGNATURE

Summary
Form:  ( DEFUN INSTANCE-SIGNATURES ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE-SIGNATURES

Summary
Form:  ( MUTUAL-RECURSION ( DEFUN INSTANCE-EVENT ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(INSTANCE-EVENT INSTANCE-EVENT-LIST
                INSTANCE-ENCAPSULATE)

Summary
Form:  ( DEFMACRO INSTANCE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSTANCE

Summary
Form:  ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2::ACL2-DEFAULTS-TABLE
[SGC for 20 CFUN pages..(8341 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(8349 writable)..(T=0).GC finished]

Summary
Form:  ( INCLUDE-BOOK "instance" ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
Compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.lisp.
End of Pass 1.  

;; Note: Tail-recursive call of INSTANCE-UNIFY-LIST was replaced by iteration.
;; Note: Tail-recursive call of INSTANCE-SUBSTITUTE was replaced by iteration.
;; Note: Tail-recursive call of INSTANCE-REWRITE was replaced by iteration.
;; Note: Tail-recursive call of DEFTHM-NAMES was replaced by iteration.
;; Note: Tail-recursive call of PARSE-DEFTHM-OPTIONS was replaced by iteration.
;; Note: Tail-recursive call of INSTANCE-EVENT was replaced by iteration.
End of Pass 2.  
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o.

"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o" 

Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
start address -T 0x9e95000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o

Summary
Form:  (CERTIFY-BOOK "instance" ...)
Rules: NIL
Warnings:  None
Time:  0.07 seconds (prove: 0.00, print: 0.00, other: 0.07)
 "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.lisp"
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>