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 444 CONS pages..(8307 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8395 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8395 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(8425 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(8460 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

Summary
Form:  ( INCLUDE-BOOK "primitives" ...)
Rules: NIL
Warnings:  None
Time:  0.13 seconds (prove: 0.00, print: 0.00, other: 0.13)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.lisp"
[SGC for 1281 CONS pages..(9211 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

Summary
Form:  ( INCLUDE-BOOK "computed-hints" ...)
Rules: NIL
Warnings:  None
Time:  0.10 seconds (prove: 0.00, print: 0.00, other: 0.10)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.lisp"
2

Summary
Form:  ( DEFUN IN ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN

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

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN)
        (:LINEAR HEAD-COUNT)
        (:LINEAR TAIL-COUNT)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA

Summary
Form:  ( DEFTHM NOT-IN-SELF ...)
Rules: ((:DEFINITION IN)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE HEAD-NOT-WHOLE)
        (:REWRITE LEMMA)
        (:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
NOT-IN-SELF

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

Summary
Form:  ( DEFTHM IN-SFIX-CANCEL ...)
Rules: ((:DEFINITION IN)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (: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)
IN-SFIX-CANCEL

Summary
Form:  ( DEFTHM NEVER-IN-EMPTY ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NEVER-IN-EMPTY

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

Summary
Form:  ( DEFTHM IN-TAIL ...)
Rules: ((:DEFINITION IN)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE TAIL-PRESERVES-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN-TAIL

Summary
Form:  ( DEFTHM IN-TAIL-OR-HEAD ...)
Rules: ((:DEFINITION IN) (:DEFINITION NOT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
IN-TAIL-OR-HEAD

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

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-TRANSITIVE)
        (:REWRITE HEAD-TAIL-ORDER)
        (:REWRITE IN-TAIL-OR-HEAD)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
LEMMA

Summary
Form:  ( DEFTHM HEAD-MINIMAL ...)
Rules: ((:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE IN-TAIL-OR-HEAD)
        (:REWRITE LEMMA)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
HEAD-MINIMAL

Summary
Form:  ( DEFTHM HEAD-MINIMAL-2 ...)
Rules: ((:DEFINITION NOT)
        (:REWRITE HEAD-MINIMAL)
        (:TYPE-PRESCRIPTION <<-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-MINIMAL-2

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

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION NOT)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA

Summary
Form:  ( DEFTHM LEMMA-2 ...)
Rules: ((:DEFINITION NOT)
        (:REWRITE HEAD-MINIMAL-2)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA-2

Summary
Form:  ( DEFTHM HEAD-UNIQUE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HEAD-UNIQUE
[SGC for 25 FIXNUM pages..(9332 writable)..(T=1).GC finished]

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

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

Summary
Form:  ( DEFTHM IN-INSERT ...)
Rules: ((:DEFINITION IN)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION INSERT)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE HEAD-INSERT)
        (:REWRITE HEAD-INSERT-EMPTY)
        (:REWRITE IN-HEAD)
        (:REWRITE IN-TAIL)
        (:REWRITE INSERT-IDENTITY)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-INSERT)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.04 seconds (prove: 0.03, print: 0.00, other: 0.01)
IN-INSERT

Summary
Form:  ( DEFTHM WEAK-INSERT-INDUCTION-HELPER-1 ...)
Rules: ((:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE HEAD-INSERT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
WEAK-INSERT-INDUCTION-HELPER-1

Summary
Form:  ( DEFTHM WEAK-INSERT-INDUCTION-HELPER-2 ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE HEAD-INSERT)
        (:REWRITE HEAD-INSERT-EMPTY)
        (:REWRITE TAIL-INSERT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
WEAK-INSERT-INDUCTION-HELPER-2

Summary
Form:  ( DEFTHM WEAK-INSERT-INDUCTION-HELPER-3 ...)
Rules: ((:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-IRREFLEXIVE)
        (:REWRITE HEAD-INSERT)
        (:REWRITE HEAD-MINIMAL)
        (:REWRITE IN-HEAD)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-INSERT)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
WEAK-INSERT-INDUCTION-HELPER-3

Summary
Form:  ( DEFUN WEAK-INSERT-INDUCTION ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE INSERT-PRODUCES-SET)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
WEAK-INSERT-INDUCTION
[SGC for 25 FIXNUM pages..(9332 writable)..(T=1).GC finished]

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

Summary
Form:  ( DEFTHM USE-WEAK-INSERT-INDUCTION ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
USE-WEAK-INSERT-INDUCTION

Summary
Form:  ( DEFUN FAST-SUBSET ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)
        (:EXECUTABLE-COUNTERPART IF)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FAST-SUBSET

Summary
Form:  ( DEFUN SUBSET ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBSET

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

Summary
Form:  ( DEFTHM LEMMA ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN)
        (:INDUCTION SUBSET)
        (:REWRITE IN-TAIL)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
(:DEFTHMD LEMMA)

Summary
Form:  ( DEFTHM CASE-1 ...)
Rules: ((:DEFINITION FAST-SUBSET)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE <<-ASYMMETRIC)
        (:REWRITE <<-TRICHOTOMY)
        (:REWRITE HEAD-MINIMAL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
CASE-1

Summary
Form:  ( DEFTHM CASE-2 ...)
Rules: ((:DEFINITION FAST-SUBSET)
        (:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE HEAD-MINIMAL-2)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-HEAD)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
CASE-2

Summary
Form:  ( DEFTHM FAST-SUBSET-EQUIVALENCE ...)
Rules: ((:DEFINITION FAST-SUBSET)
        (:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FAST-SUBSET)
        (:REWRITE CASE-1)
        (:REWRITE CASE-2)
        (:REWRITE HEAD-MINIMAL)
        (:REWRITE HEAD-MINIMAL-2)
        (:REWRITE IN-HEAD)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION <<-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
FAST-SUBSET-EQUIVALENCE

Summary
Form:  ( VERIFY-GUARDS SUBSET)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE FAST-SUBSET-EQUIVALENCE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBSET

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:  ( DEFUN PREDICATE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PREDICATE

Summary
Form:  ( ENCAPSULATE (((PREDICATE * ...) ...) ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
T

Summary
Form:  ( DEFUN ALL ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL

Summary
Form:  ( DEFUN FIND-NOT ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FIND-NOT

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

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

Summary
Form:  ( DEFTHM MEMBERSHIP-CONSTRAINT ...)
Rules: ((:TYPE-PRESCRIPTION ALL-HYPS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFTHMD MEMBERSHIP-CONSTRAINT)

Summary
Form:  ( ENCAPSULATE (((ALL-HYPS ...) ...) ...) ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
T

Summary
Form:  ( DEFTHM LEMMA-FIND-NOT-IS-A-WITNESS ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION FIND-NOT)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION ALL)
        (:INDUCTION FIND-NOT)
        (:INDUCTION IN)
        (:REWRITE IN-HEAD)
        (:REWRITE IN-TAIL)
        (:TYPE-PRESCRIPTION ALL)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEMMA-FIND-NOT-IS-A-WITNESS

Summary
Form:  ( DEFTHM ALL-BY-MEMBERSHIP ...)
Rules: ((:DEFINITION NOT)
        (:REWRITE LEMMA-FIND-NOT-IS-A-WITNESS)
        (:TYPE-PRESCRIPTION ALL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFTHMD ALL-BY-MEMBERSHIP)

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

Summary
Form:  ( DEFUN SUBSET-TRIGGER ...)
Rules: ((:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBSET-TRIGGER

Summary
Form:  ( DEFTHM PICK-A-POINT-SUBSET-STRATEGY ...)
Rules: ((:DEFINITION SUBSET-TRIGGER)
        (:EXECUTABLE-COUNTERPART IF)
        (:EXECUTABLE-COUNTERPART SYNP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PICK-A-POINT-SUBSET-STRATEGY

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

Summary
Form:  ( DEFUN PICK-A-POINT-SUBSET-HINT ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
PICK-A-POINT-SUBSET-HINT
((PICK-A-POINT-SUBSET-HINT ID CLAUSE
                           WORLD STABLE-UNDER-SIMPLIFICATIONP))

Summary
Form:  ( ENCAPSULATE NIL (DEFUN PICK-A-POINT-SUBSET-HINT ...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
T

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

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

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 (EMPTY X)))
                             (ALL-SET (LAMBDA NIL X))
                             (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                          (SUBSET COMPUTED-HINTS::?X Y)))
                             (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                                (IN COMPUTED-HINTS::?X Y)))))
      :EXPAND ((SUBSET-TRIGGER X Y))))


Summary
Form:  ( DEFTHM EMPTY-SUBSET ...)
Rules: ((:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EMPTY-SUBSET

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

Summary
Form:  ( DEFTHM SUBSET-IN ...)
Rules: ((:DEFINITION SUBSET)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION IN)
        (:INDUCTION SUBSET)
        (:REWRITE EMPTY-SUBSET)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-TAIL-OR-HEAD)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBSET-IN

Summary
Form:  ( DEFTHM SUBSET-IN-2 ...)
Rules: ((:DEFINITION NOT)
        (:REWRITE SUBSET-IN)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBSET-IN-2

Summary
Form:  ( DEFTHM SUBSET-INSERT-X ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION SUBSET)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION USE-WEAK-INSERT-INDUCTION)
        (:INDUCTION WEAK-INSERT-INDUCTION)
        (:REWRITE EMPTY-SUBSET)
        (:REWRITE HEAD-INSERT-EMPTY)
        (:REWRITE INSERT-IDENTITY)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE SUBSET-IN)
        (:REWRITE TAIL-INSERT-EMPTY)
        (:REWRITE WEAK-INSERT-INDUCTION-HELPER-1)
        (:REWRITE WEAK-INSERT-INDUCTION-HELPER-2)
        (:REWRITE WEAK-INSERT-INDUCTION-HELPER-3)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
SUBSET-INSERT-X

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 T))
                             (ALL-SET (LAMBDA NIL X))
                             (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                          (SUBSET COMPUTED-HINTS::?X X)))
                             (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                                (IN COMPUTED-HINTS::?X X)))))
      :EXPAND ((SUBSET-TRIGGER X X))))


Summary
Form:  ( DEFTHM SUBSET-REFLEXIVE ...)
Rules: ((:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBSET-REFLEXIVE

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 (SUBSET X Y) (SUBSET Y Z))))
                     (ALL-SET (LAMBDA NIL X))
                     (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                  (SUBSET COMPUTED-HINTS::?X Z)))
                     (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                        (IN COMPUTED-HINTS::?X Z)))))
               :EXPAND ((SUBSET-TRIGGER X Z))))


Summary
Form:  ( DEFTHM SUBSET-TRANSITIVE ...)
Rules: ((:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:REWRITE SUBSET-IN-2)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBSET-TRANSITIVE
[SGC for 2708 CONS pages..(10992 writable)..(T=2).GC finished]

Summary
Form:  ( DEFTHM SUBSET-MEMBERSHIP-TAIL ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION SUBSET)
        (:REWRITE EMPTY-SUBSET)
        (:REWRITE HEAD-MINIMAL-2)
        (:REWRITE HEAD-NOT-HEAD-TAIL)
        (:REWRITE HEAD-TAIL-ORDER-CONTRAPOSITIVE)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-HEAD)
        (:REWRITE IN-TAIL)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE SUBSET-IN)
        (:REWRITE TAIL-PRESERVES-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.11 seconds (prove: 0.10, print: 0.00, other: 0.01)
SUBSET-MEMBERSHIP-TAIL

Summary
Form:  ( DEFTHM SUBSET-MEMBERSHIP-TAIL-2 ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBSET-MEMBERSHIP-TAIL-2

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 T))
                 (ALL-SET (LAMBDA NIL X))
                 (ALL (LAMBDA (COMPUTED-HINTS::?X)
                              (SUBSET COMPUTED-HINTS::?X (INSERT A X))))
                 (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                    (IN COMPUTED-HINTS::?X (INSERT A X))))))
           :EXPAND ((SUBSET-TRIGGER X (INSERT A X)))))


Summary
Form:  ( DEFTHM SUBSET-INSERT ...)
Rules: ((:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE IN-INSERT)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBSET-INSERT

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 T))
                             (ALL-SET (LAMBDA NIL (TAIL X)))
                             (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                          (SUBSET COMPUTED-HINTS::?X X)))
                             (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                                (IN COMPUTED-HINTS::?X X)))))
      :EXPAND ((SUBSET-TRIGGER (TAIL X) X))))


Summary
Form:  ( DEFTHM SUBSET-TAIL ...)
Rules: ((:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:REWRITE IN-TAIL)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBSET-TAIL

Summary
Form:  ( DEFTHM DOUBLE-CONTAINMENT-LEMMA-HEAD ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION SUBSET)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE EMPTY-SUBSET-2)
        (:REWRITE HEAD-EMPTY-SAME)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE SUBSET-MEMBERSHIP-TAIL-2)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
(:DEFTHMD DOUBLE-CONTAINMENT-LEMMA-HEAD)

Summary
Form:  ( DEFTHM IN-TAIL-EXPAND ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE SUBSET-IN-2)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFTHMD IN-TAIL-EXPAND)

Summary
Form:  ( DEFTHM DOUBLE-CONTAINMENT-LEMMA-IN-TAIL ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:REWRITE EMPTY-SUBSET-2)
        (:REWRITE NEVER-IN-EMPTY)
        (:REWRITE SUBSET-IN)
        (:REWRITE SUBSET-IN-2)
        (:REWRITE SUBSET-MEMBERSHIP-TAIL)
        (:REWRITE SUBSET-MEMBERSHIP-TAIL-2)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
(:DEFTHMD DOUBLE-CONTAINMENT-LEMMA-IN-TAIL)

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 (NOT (EMPTY Y))
                                            (EQUAL (HEAD X) (HEAD Y))
                                            (SUBSET (TAIL X) Y)
                                            (NOT (EMPTY X))
                                            (SUBSET (TAIL Y) X))))
                     (ALL-SET (LAMBDA NIL (TAIL X)))
                     (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                  (SUBSET COMPUTED-HINTS::?X (TAIL Y))))
                     (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                        (IN COMPUTED-HINTS::?X (TAIL Y))))))
               :EXPAND ((SUBSET-TRIGGER (TAIL X) (TAIL Y)))))


Summary
Form:  ( DEFTHM DOUBLE-CONTAINMENT-LEMMA-TAIL ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:REWRITE EMPTY-SUBSET-2)
        (:REWRITE HEAD-NOT-HEAD-TAIL)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-HEAD)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:REWRITE SUBSET-MEMBERSHIP-TAIL-2)
        (:REWRITE SUBSET-TRANSITIVE)
        (:REWRITE TAIL-PRESERVES-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.07 seconds (prove: 0.07, print: 0.00, other: 0.00)
(:DEFTHMD DOUBLE-CONTAINMENT-LEMMA-TAIL)

Summary
Form:  ( DEFUN DOUBLE-TAIL-INDUCTION ...)
Rules: ((:DEFINITION O-FINP)
        (:DEFINITION O<)
        (:EXECUTABLE-COUNTERPART IF)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:LINEAR TAIL-COUNT)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ACL2-COUNT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
DOUBLE-TAIL-INDUCTION

Summary
Form:  ( DEFTHM DOUBLE-CONTAINMENT-IS-EQUALITY-LEMMA ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:REWRITE HEAD-TAIL-SAME)
        (:REWRITE IN-HEAD)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SUBSET-TAIL)
        (:REWRITE SUBSET-TRANSITIVE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
DOUBLE-CONTAINMENT-IS-EQUALITY-LEMMA

Summary
Form:  ( DEFTHM DOUBLE-CONTAINMENT-IS-EQUALITY ...)
Rules: ((:DEFINITION IN)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DOUBLE-TAIL-INDUCTION)
        (:REWRITE DOUBLE-CONTAINMENT-IS-EQUALITY-LEMMA)
        (:REWRITE EMPTY-SET-UNIQUE)
        (:REWRITE EMPTY-SUBSET)
        (:REWRITE EMPTY-SUBSET-2)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-HEAD)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SUBSET-MEMBERSHIP-TAIL-2)
        (:REWRITE SUBSET-REFLEXIVE)
        (:REWRITE SUBSET-TAIL)
        (:REWRITE SUBSET-TRANSITIVE)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
(:DEFTHMD DOUBLE-CONTAINMENT-IS-EQUALITY)

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

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

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

Summary
Form:  ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
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 0x9e16000 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 0x9e18160 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
[SGC for 4272 CONS pages..(12820 writable)..(T=3).GC finished]

Summary
Form:  ( INCLUDE-BOOK "membership" ...)
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/membership.lisp.
End of Pass 1.  

;; Note: Tail-recursive call of IN was replaced by iteration.
;; Note: Tail-recursive call of FAST-SUBSET was replaced by iteration.
;; Note: Tail-recursive call of FAST-SUBSET was replaced by iteration.
;; Note: Tail-recursive call of ALL was replaced by iteration.
;; Note: Tail-recursive call of FIND-NOT 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/membership.o.

"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.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:  (CERTIFY-BOOK "membership" ...)
Rules: NIL
Warnings:  None
Time:  0.33 seconds (prove: 0.03, print: 0.00, other: 0.30)
 "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.lisp"
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>