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.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 "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 444 CONS pages..(8306 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8869 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8869 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(8900 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(8906 writable)..(T=1).GC finished]

Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
start address -T 0x91e9000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
[SGC for 1281 CONS pages..(9200 writable)..(T=1).GC finished]
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
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
start address -T 0x89e1000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o
start address -T 0x93f4000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o

Summary
Form:  ( INCLUDE-BOOK "membership" ...)
Rules: NIL
Warnings:  None
Time:  0.33 seconds (prove: 0.00, print: 0.00, other: 0.33)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.lisp"
2
[SGC for 25 FIXNUM pages..(9494 writable)..(T=1).GC finished]

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

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

Summary
Form:  ( DEFTHM CONS-TO-INSERT-EMPTY ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION INSERT)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (: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)
CONS-TO-INSERT-EMPTY

We suspect this conjecture sould be proven by functional instantiation
of ALL-BY-MEMBERSHIP.  This suspicion is caused by PICK-A-POINT-SUBSET-
STRATEGY, so if this is not what you want to do, then you should disable
PICK-A-POINT-SUBSET-STRATEGY.  Accordingly, we suggest the following
hint: 

("Goal'''"
     (:USE ((:FUNCTIONAL-INSTANCE
                 ALL-BY-MEMBERSHIP
                 (ALL-HYPS (LAMBDA NIL (AND (SETP X) (<< A (CAR X)))))
                 (ALL-SET (LAMBDA NIL X))
                 (ALL (LAMBDA (COMPUTED-HINTS::?X)
                              (SUBSET COMPUTED-HINTS::?X (CONS A X))))
                 (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                    (IN COMPUTED-HINTS::?X (CONS A X))))))
           :EXPAND ((SUBSET-TRIGGER X (CONS A X)))))

[SGC for 25 FIXNUM pages..(9553 writable)..(T=2).GC finished]

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

Summary
Form:  ( DEFTHM CONS-IN ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CONS-SET)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE IN-INSERT)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
CONS-IN

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

Summary
Form:  ( DEFUN FAST-UNION-OLD ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FAST-MEASURE)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
FAST-UNION-OLD
[SGC for 2708 CONS pages..(10924 writable)..(T=2).GC finished]

Summary
Form:  ( DEFTHM FAST-UNION-OLD-HEAD-WEAK ...)
Rules: ((:DEFINITION FAST-UNION-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-HEAD)
        (:REWRITE CONS-SET)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE HEAD-INSERT)
        (:REWRITE HEAD-INSERT-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.07 seconds (prove: 0.06, print: 0.00, other: 0.01)
(:DEFTHMD FAST-UNION-OLD-HEAD-WEAK)

Summary
Form:  ( DEFTHM FAST-UNION-OLD-SET ...)
Rules: ((:DEFINITION FAST-UNION-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-UNION-OLD)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-SET)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.02, print: 0.00, other: 0.01)
FAST-UNION-OLD-SET

Summary
Form:  ( DEFTHM FAST-UNION-OLD-HEAD-STRONG ...)
Rules: ((:DEFINITION FAST-UNION-OLD)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-UNION-OLD)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-HEAD)
        (:REWRITE CONS-SET)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE FAST-UNION-OLD-SET)
        (:REWRITE HEAD-INSERT)
        (:REWRITE HEAD-INSERT-EMPTY)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:REWRITE INSERT-HEAD-TAIL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.06 seconds (prove: 0.06, print: 0.00, other: 0.00)
FAST-UNION-OLD-HEAD-STRONG
[SGC for 4272 CONS pages..(12488 writable)..(T=2).GC finished]

Summary
Form:  ( DEFTHM FAST-UNION-OLD-MEMBERSHIP ...)
Rules: ((:DEFINITION FAST-UNION-OLD)
        (:DEFINITION IN)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:INDUCTION FAST-UNION-OLD)
        (:INDUCTION IN)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-SET)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE FAST-UNION-OLD-HEAD-STRONG)
        (:REWRITE FAST-UNION-OLD-SET)
        (:REWRITE HEAD-INSERT)
        (:REWRITE HEAD-INSERT-EMPTY)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-HEAD)
        (:REWRITE IN-INSERT)
        (:REWRITE IN-SET)
        (:REWRITE IN-TAIL-OR-HEAD)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SUBSET-IN)
        (:REWRITE SUBSET-IN-2)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  1.29 seconds (prove: 1.29, print: 0.00, other: 0.00)
FAST-UNION-OLD-MEMBERSHIP

Summary
Form:  ( ENCAPSULATE NIL (LOCAL ...) ...)
Rules: NIL
Warnings:  None
Time:  1.38 seconds (prove: 1.37, print: 0.00, other: 0.01)
T

Summary
Form:  ( DEFUN FAST-UNION ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FAST-MEASURE)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION REVAPPEND))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FAST-UNION

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION FAST-UNION)
        (:DEFINITION FAST-UNION-OLD)
        (:DEFINITION REVAPPEND)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-UNION)
        (:INDUCTION FAST-UNION-OLD)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE LEMMA))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
LEMMA2

Summary
Form:  ( DEFTHM FAST-UNION-SET ...)
Rules: ((:REWRITE FAST-UNION-OLD-SET)
        (:REWRITE LEMMA2)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FAST-UNION-SET

Summary
Form:  ( DEFTHM FAST-UNION-MEMBERSHIP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE FAST-UNION-OLD-MEMBERSHIP)
        (:REWRITE LEMMA2)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FAST-UNION-MEMBERSHIP

Summary
Form:  ( ENCAPSULATE NIL (LOCAL ...) ...)
Rules: NIL
Warnings:  None
Time:  0.03 seconds (prove: 0.01, print: 0.00, other: 0.02)
T

Summary
Form:  ( DEFUN FAST-INTERSECT-OLD ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FAST-MEASURE)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SFIX))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FAST-INTERSECT-OLD

Summary
Form:  ( DEFTHM FAST-INTERSECT-OLD-EMPTY ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (: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)
FAST-INTERSECT-OLD-EMPTY

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA
[SGC for 6037 CONS pages..(14253 writable)..(T=4).GC finished]

Summary
Form:  ( DEFTHM LEMMA-2 ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE FAST-INTERSECT-OLD-EMPTY)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
LEMMA-2

Summary
Form:  ( DEFTHM FAST-INTERSECT-OLD-HEAD ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-INTERSECT-OLD)
        (:REWRITE CONS-HEAD)
        (:REWRITE NONEMPTY-MEANS-SET))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
(:DEFTHMD FAST-INTERSECT-OLD-HEAD)

Summary
Form:  ( DEFTHM FAST-INTERSECT-OLD-ORDER-WEAK ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-INTERSECT-OLD)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRANSITIVE)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE FAST-INTERSECT-OLD-EMPTY)
        (:REWRITE HEAD-INSERT-EMPTY)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE INSERT-HEAD-TAIL)
        (:REWRITE LEMMA)
        (:REWRITE LEMMA-2)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.08 seconds (prove: 0.08, print: 0.00, other: 0.00)
FAST-INTERSECT-OLD-ORDER-WEAK

Summary
Form:  ( DEFTHM FAST-INTERSECT-OLD-NONEMPTY-WEAK ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION NOT)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE FAST-INTERSECT-OLD-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FAST-INTERSECT-OLD-NONEMPTY-WEAK

Summary
Form:  ( DEFTHM LEMMA-3 ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.05 seconds (prove: 0.04, print: 0.00, other: 0.01)
LEMMA-3

Summary
Form:  ( DEFTHM FAST-INTERSECT-OLD-SET ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-INTERSECT-OLD)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE FAST-INTERSECT-OLD-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (: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)
FAST-INTERSECT-OLD-SET
[SGC for 6037 CONS pages..(14263 writable)..(T=3).GC finished]
[SGC for 9394 CONS pages..(17620 writable)..(T=5).GC finished]

Summary
Form:  ( DEFTHM FAST-INTERSECT-OLD-MEMBERSHIP ...)
Rules: ((:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION IN)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:INDUCTION FAST-INTERSECT-OLD)
        (:INDUCTION IN)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE FAST-INTERSECT-OLD-EMPTY)
        (:REWRITE FAST-INTERSECT-OLD-SET)
        (:REWRITE HEAD-MINIMAL)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-HEAD)
        (:REWRITE IN-INSERT)
        (:REWRITE IN-SET)
        (:REWRITE IN-TAIL-OR-HEAD)
        (:REWRITE INSERT-HEAD-TAIL)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE SUBSET-IN)
        (:REWRITE SUBSET-IN-2)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  2.67 seconds (prove: 2.67, print: 0.00, other: 0.00)
FAST-INTERSECT-OLD-MEMBERSHIP

Summary
Form:  ( ENCAPSULATE NIL (DEFTHM FAST-INTERSECT-OLD-EMPTY ...) ...)
Rules: NIL
Warnings:  None
Time:  2.82 seconds (prove: 2.80, print: 0.00, other: 0.02)
T

Summary
Form:  ( DEFUN FAST-INTERSECT ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FAST-MEASURE)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION REVERSE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
FAST-INTERSECT

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION FAST-INTERSECT)
        (:DEFINITION FAST-INTERSECT-OLD)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:DEFINITION REVERSE)
        (:DEFINITION SFIX)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART SFIX)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-INTERSECT)
        (:INDUCTION FAST-INTERSECT-OLD)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE FAST-INTERSECT-OLD-EMPTY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.02, print: 0.00, other: 0.01)
LEMMA

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE LEMMA))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA2

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

Summary
Form:  ( DEFTHM FAST-INTERSECT-SET ...)
Rules: ((:REWRITE FAST-INTERSECT-OLD-SET)
        (:REWRITE LEMMA2)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FAST-INTERSECT-SET

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

Summary
Form:  ( ENCAPSULATE NIL (LOCAL ...) ...)
Rules: NIL
Warnings:  None
Time:  0.03 seconds (prove: 0.02, print: 0.00, other: 0.01)
T

Summary
Form:  ( DEFUN FAST-DIFFERENCE-OLD ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FAST-MEASURE)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION SFIX))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
FAST-DIFFERENCE-OLD

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION FAST-DIFFERENCE-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CONS-HEAD)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:TYPE-PRESCRIPTION <<-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION FAST-DIFFERENCE-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-DIFFERENCE-OLD)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA2

Summary
Form:  ( DEFTHM FAST-DIFFERENCE-OLD-ORDER-WEAK ...)
Rules: ((:DEFINITION FAST-DIFFERENCE-OLD)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-DIFFERENCE-OLD)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRANSITIVE)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE INSERT-HEAD-TAIL)
        (:REWRITE LEMMA2)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.06 seconds (prove: 0.05, print: 0.00, other: 0.01)
FAST-DIFFERENCE-OLD-ORDER-WEAK

Summary
Form:  ( DEFTHM FAST-DIFFERENCE-OLD-SET ...)
Rules: ((:DEFINITION FAST-DIFFERENCE-OLD)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-DIFFERENCE-OLD)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-SET)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
FAST-DIFFERENCE-OLD-SET

Summary
Form:  ( DEFTHM FAST-DIFFERENCE-OLD-MEMBERSHIP ...)
Rules: ((:DEFINITION FAST-DIFFERENCE-OLD)
        (:DEFINITION IN)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:INDUCTION FAST-DIFFERENCE-OLD)
        (:INDUCTION IN)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE CONS-TO-INSERT-EMPTY)
        (:REWRITE CONS-TO-INSERT-NONEMPTY)
        (:REWRITE FAST-DIFFERENCE-OLD-SET)
        (:REWRITE HEAD-MINIMAL)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-HEAD)
        (:REWRITE IN-INSERT)
        (:REWRITE IN-SET)
        (:REWRITE IN-TAIL-OR-HEAD)
        (:REWRITE INSERT-HEAD-TAIL)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE SUBSET-IN)
        (:REWRITE SUBSET-IN-2)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.79 seconds (prove: 0.78, print: 0.00, other: 0.01)
FAST-DIFFERENCE-OLD-MEMBERSHIP

Summary
Form:  ( DEFTHM FAST-DIFFERENCE-OLD-EMPTY ...)
Rules: ((:DEFINITION FAST-DIFFERENCE-OLD)
        (: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)
FAST-DIFFERENCE-OLD-EMPTY

Summary
Form:  ( ENCAPSULATE NIL (LOCAL ...) ...)
Rules: NIL
Warnings:  None
Time:  0.90 seconds (prove: 0.88, print: 0.00, other: 0.02)
T

Summary
Form:  ( DEFUN FAST-DIFFERENCE ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::NATP-COMPOUND-RECOGNIZER)
        (:DEFINITION FAST-MEASURE)
        (:DEFINITION NOT)
        (:DEFINITION O-FINP)
        (:DEFINITION O-P)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION REVAPPEND)
        (:TYPE-PRESCRIPTION REVERSE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FAST-DIFFERENCE

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION EMPTY)
        (:DEFINITION NOT)
        (: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)
LEMMA
[SGC for 9394 CONS pages..(17631 writable)..(T=5).GC finished]

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION FAST-DIFFERENCE)
        (:DEFINITION FAST-DIFFERENCE-OLD)
        (:DEFINITION REVAPPEND)
        (:DEFINITION REVERSE)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-DIFFERENCE)
        (:INDUCTION FAST-DIFFERENCE-OLD)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE FAST-DIFFERENCE-OLD-EMPTY)
        (:REWRITE LEMMA)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.05 seconds (prove: 0.05, print: 0.00, other: 0.00)
LEMMA2

Summary
Form:  ( DEFTHM LEMMA3 ...)
Rules: ((:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE LEMMA2))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA3

Summary
Form:  ( DEFTHM FAST-DIFFERENCE-SET ...)
Rules: ((:REWRITE FAST-DIFFERENCE-OLD-SET)
        (:REWRITE LEMMA3)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FAST-DIFFERENCE-SET

Summary
Form:  ( DEFTHM FAST-DIFFERENCE-MEMBERSHIP ...)
Rules: ((:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE FAST-DIFFERENCE-OLD-MEMBERSHIP)
        (:REWRITE LEMMA3)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
FAST-DIFFERENCE-MEMBERSHIP

Summary
Form:  ( DEFTHM FAST-DIFFERENCE-EMPTY ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
        (:REWRITE FAST-DIFFERENCE-OLD-EMPTY)
        (:REWRITE LEMMA)
        (:REWRITE LEMMA3)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FAST-DIFFERENCE-EMPTY

Summary
Form:  ( ENCAPSULATE NIL (LOCAL ...) ...)
Rules: NIL
Warnings:  None
Time:  0.06 seconds (prove: 0.05, print: 0.00, other: 0.01)
T

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

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

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

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

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

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
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
start address -T 0x9b24b90 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
start address -T 0x9ea5000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
start address -T 0x9ea7160 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o
start address -T 0x8f67000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o

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

;; Note: Tail-recursive call of FAST-UNION was replaced by iteration.
;; Note: Tail-recursive call of FAST-UNION was replaced by iteration.
;; Note: Tail-recursive call of FAST-UNION was replaced by iteration.
;; Note: Tail-recursive call of FAST-INTERSECT was replaced by iteration.
;; Note: Tail-recursive call of FAST-INTERSECT was replaced by iteration.
;; Note: Tail-recursive call of FAST-INTERSECT was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE-OLD was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE-OLD was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE was replaced by iteration.
;; Note: Tail-recursive call of FAST-DIFFERENCE 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/fast.o.

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

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

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

ACL2>