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.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "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..(8307 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8427 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8427 writable)..(T=0).GC finished]
[SGC for 20 CFUN pages..(9133 writable)..(T=2).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
[SGC for 20 CFUN pages..(9168 writable)..(T=1).GC finished]
[SGC for 1281 CONS pages..(9500 writable)..(T=1).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o
start address -T 0x9665000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o

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

Summary
Form:  ( DEFCONST *POSITIVE-FUNCTIONS* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*POSITIVE-FUNCTIONS*
[SGC for 12 SYMBOL pages..(9660 writable)..(T=2).GC finished]

Summary
Form:  ( DEFCONST *NEGATIVE-FUNCTIONS* ...)
Rules: NIL
Warnings:  None
Time:  0.05 seconds (prove: 0.00, print: 0.00, other: 0.05)
*NEGATIVE-FUNCTIONS*

Summary
Form:  ( DEFCONST *FUNCTIONS* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*FUNCTIONS*

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

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

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

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

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

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

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

Summary
Form:  ( DEFUN FIND ...)
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

Summary
Form:  ( DEFUN FILTER ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)
        (:TYPE-PRESCRIPTION INSERT)
        (:TYPE-PRESCRIPTION SFIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER

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

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

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

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

Summary
Form:  ( DEFUN ALL<NOT> ...)
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<NOT>
[SGC for 25 FIXNUM pages..(9849 writable)..(T=1).GC finished]

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

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

Summary
Form:  ( DEFUN FILTER<NOT> ...)
Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)
        (:TYPE-PRESCRIPTION INSERT)
        (:TYPE-PRESCRIPTION SFIX))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER<NOT>

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

Summary
Form:  ( DEFCONST *POSITIVE-THEOREMS* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*POSITIVE-THEOREMS*
[SGC for 25 FIXNUM pages..(9849 writable)..(T=2).GC finished]
[SGC for 2708 CONS pages..(11084 writable)..(T=2).GC finished]
[SGC for 2708 CONS pages..(11084 writable)..(T=2).GC finished]

Summary
Form:  ( DEFCONST *NEGATIVE-THEOREMS* ...)
Rules: NIL
Warnings:  None
Time:  0.33 seconds (prove: 0.00, print: 0.00, other: 0.33)
*NEGATIVE-THEOREMS*

Summary
Form:  ( DEFCONST *THEOREMS* ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
*THEOREMS*

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

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

Summary
Form:  ( DEFTHM ALL-LIST-CDR ...)
Rules: ((:DEFINITION ALL-LIST)
        (:EXECUTABLE-COUNTERPART ALL-LIST)
        (:REWRITE DEFAULT-CDR)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-CDR

Summary
Form:  ( DEFTHM ALL-LIST-ENDP ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-ENDP

Summary
Form:  ( DEFTHM ALL-LIST-IN ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION IN-LIST)
        (:REWRITE ALL-LIST-ENDP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-IN

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

Summary
Form:  ( DEFTHM ALL-LIST-CONS ...)
Rules: ((:DEFINITION ALL-LIST)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-CONS

Summary
Form:  ( DEFTHM ALL-LIST-APPEND ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION BINARY-APPEND)
        (:REWRITE ALL-LIST-CONS)
        (:REWRITE ALL-LIST-ENDP)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-APPEND

Summary
Form:  ( DEFTHM ALL-LIST-NTH ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION LEN)
        (:INDUCTION NTH)
        (:REWRITE ALL-LIST-ENDP))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-NTH

Summary
Form:  ( DEFTHM LEMMA1 ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CDR)
        (:REWRITE ALL-LIST-CONS)
        (:REWRITE ALL-LIST-ENDP)
        (:REWRITE ALL-LIST-IN)
        (:REWRITE IN-LIST-CONS)
        (:REWRITE IN-LIST-REVAPPEND)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE)
        (:TYPE-PRESCRIPTION REVAPPEND))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA1

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CONS))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA2

Summary
Form:  ( DEFTHM LEMMA3 ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CDR)
        (:REWRITE ALL-LIST-CONS)
        (:REWRITE ALL-LIST-ENDP)
        (:REWRITE ALL-LIST-IN)
        (:REWRITE IN-LIST-REVAPPEND)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA3

Summary
Form:  ( DEFTHM ALL-LIST-REVAPPEND ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CONS)
        (:REWRITE ALL-LIST-ENDP)
        (:REWRITE LEMMA2)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-REVAPPEND

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

Summary
Form:  ( DEFTHM ALL-LIST-REVERSE ...)
Rules: ((:DEFINITION REVERSE)
        (:EXECUTABLE-COUNTERPART ALL-LIST)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-LIST-ENDP)
        (:REWRITE ALL-LIST-REVAPPEND)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-REVERSE

Summary
Form:  ( DEFTHM EXISTS-LIST-ELIMINATION ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION EXISTS-LIST)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION EXISTS-LIST)
        (:TYPE-PRESCRIPTION ALL-LIST<NOT>))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
EXISTS-LIST-ELIMINATION

Summary
Form:  ( DEFTHM FILTER-LIST-TRUE-LIST ...)
Rules: ((:TYPE-PRESCRIPTION FILTER-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-LIST-TRUE-LIST

Summary
Form:  ( DEFTHM FILTER-LIST-MEMBERSHIP ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION FILTER-LIST)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ALL-LIST)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FILTER-LIST)
        (:INDUCTION IN-LIST)
        (:REWRITE ALL-LIST-IN-2)
        (:REWRITE IN-LIST-CONS)
        (:REWRITE IN-LIST-ON-SET)
        (:REWRITE NEVER-IN-EMPTY))
Warnings:  None
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
FILTER-LIST-MEMBERSHIP

Summary
Form:  ( DEFTHM FILTER-LIST-ALL-LIST ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION FILTER-LIST)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART ALL-LIST)
        (:INDUCTION FILTER-LIST)
        (:REWRITE ALL-LIST-CDR)
        (:REWRITE ALL-LIST-CONS)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE)
        (:TYPE-PRESCRIPTION FILTER-LIST-TRUE-LIST))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-LIST-ALL-LIST

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

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

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

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

Summary
Form:  ( DEFTHM ALL-IN ...)
Rules: ((:DEFINITION ALL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL)
        (:INDUCTION IN)
        (:REWRITE ALL-EMPTY)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE IN-TAIL-OR-HEAD)
        (: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)
ALL-IN

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

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

Summary
Form:  ( DEFTHM ALL-DELETE ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION DELETE)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL)
        (:INDUCTION DELETE)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-INSERT)
        (:REWRITE ALL-TAIL)
        (:REWRITE DELETE-NONMEMBER-CANCEL)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-DELETE

Summary
Form:  ( DEFTHM ALL-DELETE-2 ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION DELETE)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL)
        (:INDUCTION DELETE)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-INSERT)
        (:REWRITE DELETE-NONMEMBER-CANCEL)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-DELETE-2

Summary
Form:  ( DEFTHM ALL-UNION ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION UNION)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL)
        (:INDUCTION UNION)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-INSERT)
        (:REWRITE ALL-SFIX)
        (:REWRITE UNION-EMPTY-X)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-UNION

Summary
Form:  ( DEFTHM ALL-INTERSECT-X ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION INTERSECT)
        (:INDUCTION ALL)
        (:INDUCTION INTERSECT)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-INSERT)
        (:REWRITE ALL-TAIL)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE INTERSECT-SYMMETRIC)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.05 seconds (prove: 0.05, print: 0.00, other: 0.00)
ALL-INTERSECT-X

Summary
Form:  ( DEFTHM ALL-INTERSECT-Y ...)
Rules: ((:REWRITE ALL-INTERSECT-X)
        (:REWRITE INTERSECT-SYMMETRIC)
        (:TYPE-PRESCRIPTION ALL-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-INTERSECT-Y
[SGC for 4519 CONS pages..(12917 writable)..(T=3).GC finished]

Summary
Form:  ( DEFTHM ALL-DIFFERENCE ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION DIFFERENCE)
        (:INDUCTION ALL)
        (:INDUCTION DIFFERENCE)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-INSERT)
        (:REWRITE ALL-TAIL)
        (:REWRITE DIFFERENCE-EMPTY-X)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE SUBSET-DIFFERENCE)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.07 seconds (prove: 0.07, print: 0.00, other: 0.00)
ALL-DIFFERENCE

Summary
Form:  ( DEFTHM ALL-DIFFERENCE-2 ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION DIFFERENCE)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL)
        (:INDUCTION DIFFERENCE)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-IN-2)
        (:REWRITE ALL-INSERT)
        (:REWRITE DIFFERENCE-EMPTY-X)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
ALL-DIFFERENCE-2

Summary
Form:  ( DEFTHM EXISTS-ELIMINATION ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION EXISTS)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION EXISTS)
        (:TYPE-PRESCRIPTION ALL<NOT>)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EXISTS-ELIMINATION

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

Summary
Form:  ( DEFTHM FIND-WITNESS ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION FIND<NOT>)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:INDUCTION ALL)
        (:INDUCTION FIND<NOT>)
        (:INDUCTION IN)
        (:REWRITE ALL-EMPTY)
        (:REWRITE IN-HEAD)
        (:REWRITE SUBSET-IN)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (: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)
FIND-WITNESS

Summary
Form:  ( DEFTHM FILTER-SET ...)
Rules: ((:DEFINITION FILTER)
        (:INDUCTION FILTER)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-PRODUCES-SET)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-SET

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: 

("Subgoal 2'"
     (:USE ((:FUNCTIONAL-INSTANCE
                 ALL-BY-MEMBERSHIP
                 (ALL-HYPS (LAMBDA NIL T))
                 (ALL-SET (LAMBDA NIL (FILTER (SFIX X))))
                 (ALL (LAMBDA (COMPUTED-HINTS::?X)
                              (SUBSET COMPUTED-HINTS::?X (FILTER X))))
                 (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                    (IN COMPUTED-HINTS::?X (FILTER X))))))
           :EXPAND ((SUBSET-TRIGGER (FILTER (SFIX X))
                                    (FILTER X)))))


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

Summary
Form:  ( DEFTHM FILTER-IN ...)
Rules: ((:DEFINITION FILTER)
        (:DEFINITION IN)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FILTER)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE IN-INSERT)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
FILTER-IN

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


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

Summary
Form:  ( DEFTHM FILTER-ALL ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION FILTER)
        (:INDUCTION FILTER)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-INSERT)
        (:REWRITE ALL-TAIL)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-ALL

Summary
Form:  ( DEFTHM FILTER-ALL-2 ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION FILTER)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL)
        (:INDUCTION FILTER)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-IN)
        (:REWRITE IN-HEAD)
        (:REWRITE INSERT-HEAD-TAIL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
FILTER-ALL-2

Summary
Form:  ( DEFTHM ALL-MERGESORT ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION MERGESORT)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART ALL)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION MERGESORT)
        (:REWRITE ALL-INSERT)
        (:REWRITE ALL-LIST-ENDP))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-MERGESORT

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

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

Summary
Form:  ( DEFTHM ALL-LIST-CDR-NOT ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:EXECUTABLE-COUNTERPART ALL-LIST<NOT>)
        (:REWRITE DEFAULT-CDR)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-CDR-NOT

Summary
Form:  ( DEFTHM ALL-LIST-ENDP-NOT ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-ENDP-NOT

Summary
Form:  ( DEFTHM ALL-LIST-IN-NOT ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION IN-LIST)
        (:REWRITE ALL-LIST-ENDP-NOT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-IN-NOT

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

Summary
Form:  ( DEFTHM ALL-LIST-CONS-NOT ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-CONS-NOT

Summary
Form:  ( DEFTHM ALL-LIST-APPEND-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION BINARY-APPEND)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION BINARY-APPEND)
        (:REWRITE ALL-LIST-CONS-NOT)
        (:REWRITE ALL-LIST-ENDP-NOT)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-APPEND-NOT

Summary
Form:  ( DEFTHM ALL-LIST-NTH-NOT ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION LEN)
        (:INDUCTION NTH)
        (:REWRITE ALL-LIST-ENDP-NOT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-NTH-NOT

Summary
Form:  ( DEFTHM LEMMA1 ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CDR-NOT)
        (:REWRITE ALL-LIST-CONS-NOT)
        (:REWRITE ALL-LIST-ENDP-NOT)
        (:REWRITE ALL-LIST-IN-NOT)
        (:REWRITE IN-LIST-CONS)
        (:REWRITE IN-LIST-REVAPPEND)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT)
        (:TYPE-PRESCRIPTION REVAPPEND))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
LEMMA1

Summary
Form:  ( DEFTHM LEMMA2 ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CONS-NOT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA2

Summary
Form:  ( DEFTHM LEMMA3 ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CDR-NOT)
        (:REWRITE ALL-LIST-CONS-NOT)
        (:REWRITE ALL-LIST-ENDP-NOT)
        (:REWRITE ALL-LIST-IN-NOT)
        (:REWRITE IN-LIST-REVAPPEND)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
LEMMA3

Summary
Form:  ( DEFTHM ALL-LIST-REVAPPEND-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION NOT)
        (:DEFINITION REVAPPEND)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION REVAPPEND)
        (:REWRITE ALL-LIST-CONS-NOT)
        (:REWRITE ALL-LIST-ENDP-NOT)
        (:REWRITE LEMMA2)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-REVAPPEND-NOT

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

Summary
Form:  ( DEFTHM ALL-LIST-REVERSE-NOT ...)
Rules: ((:DEFINITION REVERSE)
        (:EXECUTABLE-COUNTERPART ALL-LIST<NOT>)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-LIST-ENDP-NOT)
        (:REWRITE ALL-LIST-REVAPPEND-NOT)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-LIST-REVERSE-NOT

Summary
Form:  ( DEFTHM EXISTS-LIST-ELIMINATION-NOT ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION EXISTS-LIST<NOT>)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION ALL-LIST)
        (:INDUCTION EXISTS-LIST<NOT>)
        (:REWRITE ALL-LIST-ENDP)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
EXISTS-LIST-ELIMINATION-NOT

Summary
Form:  ( DEFTHM FILTER-LIST-TRUE-LIST-NOT ...)
Rules: ((:TYPE-PRESCRIPTION FILTER-LIST<NOT>))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-LIST-TRUE-LIST-NOT

Summary
Form:  ( DEFTHM FILTER-LIST-MEMBERSHIP-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION ENDP)
        (:DEFINITION FILTER-LIST<NOT>)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART ALL-LIST<NOT>)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FILTER-LIST<NOT>)
        (:INDUCTION IN-LIST)
        (:REWRITE ALL-LIST-ENDP)
        (:REWRITE ALL-LIST-IN-2)
        (:REWRITE ALL-LIST-IN-2-NOT)
        (:REWRITE IN-LIST-CONS)
        (:REWRITE IN-LIST-ON-SET)
        (:REWRITE NEVER-IN-EMPTY))
Warnings:  None
Time:  0.04 seconds (prove: 0.04, print: 0.00, other: 0.00)
FILTER-LIST-MEMBERSHIP-NOT

Summary
Form:  ( DEFTHM FILTER-LIST-ALL-LIST-NOT ...)
Rules: ((:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION FILTER-LIST<NOT>)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART ALL-LIST<NOT>)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION FILTER-LIST<NOT>)
        (:REWRITE ALL-LIST-CDR-NOT)
        (:REWRITE ALL-LIST-CONS-NOT)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT)
        (:TYPE-PRESCRIPTION FILTER-LIST-TRUE-LIST-NOT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FILTER-LIST-ALL-LIST-NOT

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

Summary
Form:  ( DEFTHM ALL-SFIX-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT>)
        (: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)
ALL-SFIX-NOT

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

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

Summary
Form:  ( DEFTHM ALL-IN-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION IN)
        (:REWRITE ALL-EMPTY-NOT)
        (: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)
ALL-IN-NOT

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

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

Summary
Form:  ( DEFTHM ALL-DELETE-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION DELETE)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION DELETE)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE ALL-TAIL-NOT)
        (:REWRITE DELETE-NONMEMBER-CANCEL)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-DELETE-NOT

Summary
Form:  ( DEFTHM ALL-DELETE-2-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION DELETE)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION DELETE)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-IN-2)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE DELETE-NONMEMBER-CANCEL)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
ALL-DELETE-2-NOT

Summary
Form:  ( DEFTHM ALL-UNION-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION ALL<NOT>)
        (:DEFINITION UNION)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION UNION)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE ALL-SFIX-NOT)
        (:REWRITE UNION-EMPTY-X)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-UNION-NOT

Summary
Form:  ( DEFTHM ALL-INTERSECT-X-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION INTERSECT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION INTERSECT)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE ALL-TAIL-NOT)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE INTERSECT-SYMMETRIC)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.08 seconds (prove: 0.08, print: 0.00, other: 0.00)
ALL-INTERSECT-X-NOT

Summary
Form:  ( DEFTHM ALL-INTERSECT-Y-NOT ...)
Rules: ((:REWRITE ALL-INTERSECT-X-NOT)
        (:REWRITE INTERSECT-SYMMETRIC)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-INTERSECT-Y-NOT

Summary
Form:  ( DEFTHM ALL-DIFFERENCE-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION DIFFERENCE)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION DIFFERENCE)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE ALL-TAIL-NOT)
        (:REWRITE DIFFERENCE-EMPTY-X)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE SUBSET-DIFFERENCE)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.07 seconds (prove: 0.07, print: 0.00, other: 0.00)
ALL-DIFFERENCE-NOT

Summary
Form:  ( DEFTHM ALL-DIFFERENCE-2-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION ALL<NOT>)
        (:DEFINITION DIFFERENCE)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION DIFFERENCE)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-IN-2-NOT)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE DIFFERENCE-EMPTY-X)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
ALL-DIFFERENCE-2-NOT

Summary
Form:  ( DEFTHM EXISTS-ELIMINATION-NOT ...)
Rules: ((:DEFINITION ALL)
        (:DEFINITION EXISTS<NOT>)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION ALL)
        (:INDUCTION EXISTS<NOT>)
        (:REWRITE ALL-EMPTY)
        (:TYPE-PRESCRIPTION ALL-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
EXISTS-ELIMINATION-NOT

Summary
Form:  ( DEFTHM FIND-SFIX-NOT ...)
Rules: ((:DEFINITION FIND<NOT>)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FIND<NOT>)
        (: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)
FIND-SFIX-NOT

Summary
Form:  ( DEFTHM FIND-WITNESS-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION ALL<NOT>)
        (:DEFINITION FIND)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FORWARD-CHAINING SUBSET-TAIL)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION FIND)
        (:INDUCTION IN)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE IN-HEAD)
        (:REWRITE SUBSET-IN)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (: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)
FIND-WITNESS-NOT

Summary
Form:  ( DEFTHM FILTER-SET-NOT ...)
Rules: ((:DEFINITION FILTER<NOT>)
        (:INDUCTION FILTER<NOT>)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-PRODUCES-SET)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-SET-NOT

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: 

("Subgoal 2'"
   (:USE ((:FUNCTIONAL-INSTANCE
               ALL-BY-MEMBERSHIP
               (ALL-HYPS (LAMBDA NIL T))
               (ALL-SET (LAMBDA NIL (FILTER<NOT> (SFIX X))))
               (ALL (LAMBDA (COMPUTED-HINTS::?X)
                            (SUBSET COMPUTED-HINTS::?X (FILTER<NOT> X))))
               (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                  (IN COMPUTED-HINTS::?X (FILTER<NOT> X))))))
         :EXPAND ((SUBSET-TRIGGER (FILTER<NOT> (SFIX X))
                                  (FILTER<NOT> X)))))


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

Summary
Form:  ( DEFTHM FILTER-IN-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION FILTER<NOT>)
        (:DEFINITION IN)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION FILTER<NOT>)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-IN-2)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:REWRITE IN-INSERT)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.03, print: 0.00, other: 0.00)
FILTER-IN-NOT

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


Summary
Form:  ( DEFTHM FILTER-SUBSET-NOT ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:REWRITE FILTER-IN-NOT)
        (: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)
FILTER-SUBSET-NOT

Summary
Form:  ( DEFTHM FILTER-ALL-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION FILTER<NOT>)
        (:EXECUTABLE-COUNTERPART NOT)
        (:INDUCTION FILTER<NOT>)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE ALL-TAIL-NOT)
        (:REWRITE EMPTY-SFIX-CANCEL)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FILTER-ALL-NOT

Summary
Form:  ( DEFTHM FILTER-ALL-2-NOT ...)
Rules: ((:DEFINITION ALL<NOT>)
        (:DEFINITION FILTER<NOT>)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT>)
        (:INDUCTION FILTER<NOT>)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE ALL-IN-NOT)
        (:REWRITE IN-HEAD)
        (:REWRITE INSERT-HEAD-TAIL)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE SFIX-SET-IDENTITY)
        (:REWRITE TAIL-PRODUCES-SET)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FILTER-ALL-2-NOT

Summary
Form:  ( DEFTHM ALL-MERGESORT-NOT ...)
Rules: ((:CONGRUENCE IFF-IMPLIES-EQUAL-NOT)
        (:DEFINITION ALL-LIST<NOT>)
        (:DEFINITION ENDP)
        (:DEFINITION MERGESORT)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART ALL<NOT>)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST<NOT>)
        (:INDUCTION MERGESORT)
        (:REWRITE ALL-INSERT-NOT)
        (:REWRITE ALL-LIST-ENDP-NOT))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ALL-MERGESORT-NOT
[SGC for 4519 CONS pages..(12918 writable)..(T=3).GC finished]

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

Summary
Form:  ( ENCAPSULATE NIL (DEFTHM ALL-LIST-TYPE ...) ...)
Rules: NIL
Warnings:  None
Time:  0.98 seconds (prove: 0.91, print: 0.00, other: 0.07)
T

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

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

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

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

Summary
Form:  ( DEFTHM WITNESS-LEMMA ...)
Rules: ((:DEFINITION ALL-LIST)
        (:DEFINITION ENDP)
        (:DEFINITION FIND-LIST<NOT>)
        (:DEFINITION IN-LIST)
        (:DEFINITION NOT)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL-LIST)
        (:INDUCTION FIND-LIST<NOT>)
        (:INDUCTION IN-LIST)
        (:REWRITE ALL-LIST-ENDP)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE)
        (:TYPE-PRESCRIPTION IN-LIST))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
WITNESS-LEMMA

Summary
Form:  ( DEFTHM ALL-LIST-BY-MEMBERSHIP ...)
Rules: ((:DEFINITION NOT)
        (:REWRITE WITNESS-LEMMA)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFTHMD ALL-LIST-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:  ( DEFCONST *FINAL-THEOREMS* ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
*FINAL-THEOREMS*

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

Summary
Form:  ( DEFTHM CARDINALITY-FILTER ...)
Rules: ((:DEFINITION CARDINALITY)
        (:DEFINITION FILTER)
        (:DEFINITION FILTER<NOT>)
        (:EXECUTABLE-COUNTERPART BINARY-+)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION CARDINALITY)
        (:INDUCTION FILTER)
        (:INDUCTION FILTER<NOT>)
        (:REWRITE ALL-EMPTY)
        (:REWRITE ALL-EMPTY-NOT)
        (:REWRITE CARDINALITY-SFIX-CANCEL)
        (:REWRITE COMMUTATIVITY-OF-+)
        (:REWRITE FILTER-ALL-2)
        (:REWRITE FILTER-ALL-2-NOT)
        (:REWRITE FILTER-IN)
        (:REWRITE FILTER-IN-NOT)
        (:REWRITE HEAD-UNIQUE)
        (:REWRITE INSERT-CARDINALITY)
        (:TYPE-PRESCRIPTION CARDINALITY-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
CARDINALITY-FILTER

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

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

Summary
Form:  ( ENCAPSULATE NIL (DEFTHM CARDINALITY-FILTER ...) ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
T

Summary
Form:  ( VERIFY-GUARDS FILTER)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:REWRITE FILTER-SET)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER

Summary
Form:  ( VERIFY-GUARDS FILTER<NOT>)
Rules: ((:EXECUTABLE-COUNTERPART IF)
        (:REWRITE FILTER-SET-NOT)
        (:REWRITE TAIL-PRODUCES-SET))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER<NOT>

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

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

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

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

Summary
Form:  ( DEFUN QUANTIFY-SIMPLE-PREDICATE ...)
Rules: NIL
Warnings:  None
Time:  0.06 seconds (prove: 0.00, print: 0.00, other: 0.06)
QUANTIFY-SIMPLE-PREDICATE

Summary
Form:  ( DEFMACRO QUANTIFY-PREDICATE ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
QUANTIFY-PREDICATE

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

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

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/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 0x9805000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
[SGC for 771 STRING pages..(13557 writable)..(T=3).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o
start address -T 0x9756000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o
[SGC for 121 SYMBOL pages..(15593 writable)..(T=4).GC finished]

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

;; Note: Tail-recursive call of ALL-LIST was replaced by iteration.
;; Note: Tail-recursive call of EXISTS-LIST was replaced by iteration.
;; Note: Tail-recursive call of FIND-LIST was replaced by iteration.
;; Note: Tail-recursive call of FILTER-LIST was replaced by iteration.
;; Note: Tail-recursive call of ALL was replaced by iteration.
;; Note: Tail-recursive call of EXISTS was replaced by iteration.
;; Note: Tail-recursive call of FIND was replaced by iteration.
;; Note: Tail-recursive call of FILTER was replaced by iteration.
;; Note: Tail-recursive call of ALL-LIST<NOT> was replaced by iteration.
;; Note: Tail-recursive call of EXISTS-LIST<NOT> was replaced by iteration.
;; Note: Tail-recursive call of FIND-LIST<NOT> was replaced by iteration.
;; Note: Tail-recursive call of FILTER-LIST<NOT> was replaced by iteration.
;; Note: Tail-recursive call of ALL<NOT> was replaced by iteration.
;; Note: Tail-recursive call of EXISTS<NOT> was replaced by iteration.
;; Note: Tail-recursive call of FIND<NOT> was replaced by iteration.
;; Note: Tail-recursive call of FILTER<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/quantify.o.

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

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

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

ACL2>