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=0).GC finished]

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

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

Summary
Form:  ( DEFTHM <<-TYPE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION <<))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
<<-TYPE
[SGC for 12 STRING pages..(8306 writable)..(T=1).GC finished]

Summary
Form:  ( DEFTHM <<-IRREFLEXIVE ...)
Rules: ((:DEFINITION <<)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART IF)
        (:REWRITE ACL2::LEXORDER-REFLEXIVE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
<<-IRREFLEXIVE

Summary
Form:  ( DEFTHM <<-TRANSITIVE ...)
Rules: ((:DEFINITION <<)
        (:FORWARD-CHAINING ACL2::LEXORDER-ANTI-SYMMETRIC)
        (:REWRITE ACL2::LEXORDER-TRANSITIVE)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION LEXORDER))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
<<-TRANSITIVE

Summary
Form:  ( DEFTHM <<-ASYMMETRIC ...)
Rules: ((:DEFINITION <<)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING ACL2::LEXORDER-ANTI-SYMMETRIC)
        (:TYPE-PRESCRIPTION LEXORDER))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
<<-ASYMMETRIC

Summary
Form:  ( DEFTHM <<-TRICHOTOMY ...)
Rules: ((:DEFINITION <<)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING ACL2::LEXORDER-TOTAL)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION LEXORDER))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
<<-TRICHOTOMY

Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
1750

Summary
Form:  ( DEFUN SETP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SETP

Summary
Form:  ( DEFTHM SETP-TYPE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SETP-TYPE

Summary
Form:  ( DEFTHM SETS-ARE-TRUE-LISTS ...)
Rules: ((:DEFINITION SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SETP)
        (:INDUCTION TRUE-LISTP)
        (:TYPE-PRESCRIPTION TRUE-LISTP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SETS-ARE-TRUE-LISTS

Summary
Form:  ( DEFUN EMPTY ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION NULL)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EMPTY

Summary
Form:  ( DEFTHM EMPTY-TYPE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION EMPTY))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EMPTY-TYPE

Summary
Form:  ( DEFUN SFIX ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SFIX

Summary
Form:  ( DEFUN HEAD ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD

Summary
Form:  ( DEFUN TAIL ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
TAIL

Summary
Form:  ( DEFUN INSERT ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION EMPTY)
        (:DEFINITION FIX)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
INSERT

Summary
Form:  ( DEFTHM TAIL-COUNT ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION EMPTY)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TAIL-COUNT
[SGC for 444 CONS pages..(8329 writable)..(T=1).GC finished]

Summary
Form:  ( DEFTHM HEAD-COUNT ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION EMPTY)
        (:DEFINITION FIX)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
HEAD-COUNT

Summary
Form:  ( DEFTHM TAIL-COUNT-BUILT-IN ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION EMPTY)
        (:DEFINITION FIX)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TAIL-COUNT-BUILT-IN

Summary
Form:  ( DEFTHM HEAD-COUNT-BUILT-IN ...)
Rules: ((:DEFINITION ACL2-COUNT)
        (:DEFINITION EMPTY)
        (:DEFINITION FIX)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ACL2-COUNT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE UNICITY-OF-0)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
HEAD-COUNT-BUILT-IN

Summary
Form:  ( DEFTHM SFIX-PRODUCES-SET ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SFIX-PRODUCES-SET

Summary
Form:  ( DEFTHM TAIL-PRODUCES-SET ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TAIL-PRODUCES-SET
[SGC for 444 CONS pages..(8331 writable)..(T=1).GC finished]

Summary
Form:  ( DEFTHM INSERT-PRODUCES-SET ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION INSERT)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION INSERT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.06 seconds (prove: 0.06, print: 0.00, other: 0.00)
INSERT-PRODUCES-SET

Summary
Form:  ( DEFTHM NONEMPTY-MEANS-SET ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION NOT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NONEMPTY-MEANS-SET

Summary
Form:  ( DEFTHM EMPTY-SET-UNIQUE ...)
Rules: ((:DEFINITION EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EMPTY-SET-UNIQUE

Summary
Form:  ( DEFTHM HEAD-EMPTY-SAME ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-EMPTY-SAME

Summary
Form:  ( DEFTHM TAIL-EMPTY-SAME ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TAIL-EMPTY-SAME

Summary
Form:  ( DEFTHM INSERT-EMPTY-SAME ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION INSERT)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSERT-EMPTY-SAME

Summary
Form:  ( DEFTHM SFIX-EMPTY-SAME ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SFIX-EMPTY-SAME

Summary
Form:  ( DEFTHM HEAD-TAIL-SAME ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-TAIL-SAME

Summary
Form:  ( DEFTHM INSERT-NEVER-EMPTY ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION INSERT)
        (:REWRITE INSERT-PRODUCES-SET)
        (:TYPE-PRESCRIPTION INSERT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
INSERT-NEVER-EMPTY

Summary
Form:  ( DEFTHM TAIL-PRESERVES-EMPTY ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TAIL-PRESERVES-EMPTY

Summary
Form:  ( DEFTHM SFIX-SET-IDENTITY ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SFIX-SET-IDENTITY

Summary
Form:  ( DEFTHM EMPTY-SFIX-CANCEL ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EMPTY-SFIX-CANCEL

Summary
Form:  ( DEFTHM HEAD-SFIX-CANCEL ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
HEAD-SFIX-CANCEL

Summary
Form:  ( DEFTHM TAIL-SFIX-CANCEL ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TAIL-SFIX-CANCEL

Summary
Form:  ( DEFTHM INSERT-SFIX-CANCEL ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION INSERT)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INSERT-SFIX-CANCEL

Summary
Form:  ( DEFTHM HEAD-INSERT ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION TAIL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CAR)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
HEAD-INSERT

Summary
Form:  ( DEFTHM TAIL-INSERT ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CDR-CONS)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
TAIL-INSERT
[SGC for 25 FIXNUM pages..(9789 writable)..(T=1).GC finished]
[SGC for 25 FIXNUM pages..(9789 writable)..(T=2).GC finished]
[SGC for 2996 CONS pages..(10915 writable)..(T=2).GC finished]

Summary
Form:  ( DEFTHM INSERT-INSERT ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART CONS)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION INSERT)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE <<-TRANSITIVE)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE ACL2::CONS-CAR-CDR)
        (:REWRITE CONS-EQUAL)
        (:REWRITE DEFAULT-CAR)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION INSERT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  1.52 seconds (prove: 1.52, print: 0.00, other: 0.00)
INSERT-INSERT
[SGC for 4481 CONS pages..(12411 writable)..(T=3).GC finished]

Summary
Form:  ( DEFTHM REPEATED-INSERT ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION TAIL)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION INSERT)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION INSERT)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.32 seconds (prove: 0.32, print: 0.00, other: 0.00)
REPEATED-INSERT

Summary
Form:  ( DEFTHM INSERT-HEAD ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
INSERT-HEAD

Summary
Form:  ( DEFTHM INSERT-HEAD-TAIL ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE ACL2::CONS-CAR-CDR)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
INSERT-HEAD-TAIL

Summary
Form:  ( DEFTHM HEAD-INSERT-EMPTY ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION SETP)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-INSERT-EMPTY

Summary
Form:  ( DEFTHM TAIL-INSERT-EMPTY ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION INSERT)
        (:DEFINITION SETP)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CDR-CONS)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TAIL-INSERT-EMPTY

Summary
Form:  ( DEFTHM INSERT-INDUCTION-CASE ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION INSERT)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE ACL2::CONS-CAR-CDR)
        (:REWRITE HEAD-INSERT)
        (:REWRITE HEAD-TAIL-SAME)
        (:REWRITE INSERT-INSERT)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-INSERT)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
(:DEFTHMD INSERT-INDUCTION-CASE)

Summary
Form:  ( DEFTHM HEAD-TAIL-ORDER ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-TAIL-ORDER

Summary
Form:  ( DEFTHM HEAD-TAIL-ORDER-CONTRAPOSITIVE ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:EXECUTABLE-COUNTERPART CDR)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
HEAD-TAIL-ORDER-CONTRAPOSITIVE

Summary
Form:  ( DEFTHM HEAD-NOT-HEAD-TAIL ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:DEFINITION SETP)
        (:DEFINITION SFIX)
        (:DEFINITION TAIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-NOT-HEAD-TAIL

Summary
Form:  ( DEFTHM HEAD-NOT-WHOLE ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION HEAD)
        (:DEFINITION NOT)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE SFIX-SET-IDENTITY)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-NOT-WHOLE

Summary
Form:  ( DEFTHEORY PRIMITIVES-THEORY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
7

Summary
Form:  ( DEFTHEORY PRIMITIVE-ORDER-THEORY ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
8

Summary
Form:  ( IN-THEORY (DISABLE ...))
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
1791

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..(12449 writable)..(T=2).GC finished]
[SGC for 20 CFUN pages..(12449 writable)..(T=2).GC finished]

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

;; Note: Tail-recursive call of SETP 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/primitives.o.

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

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

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

ACL2>