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

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

 ACL2 Version 2.9.3 built August 2, 2005  18:40:53.
 Copyright (C) 2005  University of Texas at Austin
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the GNU General Public License.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*
                      NIL).
 See the documentation topic note-2-9-3 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

 NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
 look under the ACL2 source directory in interface/emacs/README.doc; 
 and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
 command loop.   Look in the ACL2 documentation under PROOF-TREE.

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

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

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

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

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

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

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

Summary
Form:  ( DEFPKG "SETS" ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 "SETS"
ACL2 !>>Bye.
 :EOF
ACL2 !>[SGC for 444 CONS pages..(8307 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8895 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8895 writable)..(T=1).GC finished]
[SGC for 20 CFUN pages..(9158 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
[SGC for 20 CFUN pages..(9187 writable)..(T=1).GC finished]
[SGC for 1281 CONS pages..(9498 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
[SGC for 12 SYMBOL pages..(9642 writable)..(T=2).GC finished]
[SGC for 25 FIXNUM pages..(9855 writable)..(T=2).GC finished]
[SGC for 25 FIXNUM pages..(9925 writable)..(T=1).GC finished]
[SGC for 2708 CONS pages..(11088 writable)..(T=2).GC finished]
[SGC for 2708 CONS pages..(11088 writable)..(T=2).GC finished]
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:  ( INCLUDE-BOOK "quantify" ...)
Rules: NIL
Warnings:  None
Time:  0.91 seconds (prove: 0.00, print: 0.00, other: 0.91)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/quantify.lisp"
2

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

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

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

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

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

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

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

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

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

Summary
Form:  ( ENCAPSULATE NIL (DEFUN MAP-LIST ...) ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
T
[SGC for 4519 CONS pages..(12964 writable)..(T=3).GC finished]
[SGC for 4519 CONS pages..(12983 writable)..(T=3).GC finished]

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

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

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

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

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

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

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

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

Summary
Form:  ( DEFUN ALL-LIST<NOT-INVERSEP> ...)
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-INVERSEP>

Summary
Form:  ( DEFUN EXISTS-LIST<NOT-INVERSEP> ...)
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-INVERSEP>

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

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

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

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

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

Summary
Form:  ( DEFUN FILTER<NOT-INVERSEP> ...)
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-INVERSEP>

Summary
Form:  ( ENCAPSULATE NIL (DEFUN ALL-LIST<INVERSEP> ...) ...)
Rules: NIL
Warnings:  None
Time:  0.06 seconds (prove: 0.00, print: 0.00, other: 0.06)
T
[SGC for 121 SYMBOL pages..(14140 writable)..(T=4).GC finished]
[SGC for 7128 CONS pages..(15676 writable)..(T=4).GC finished]
[SGC for 7128 CONS pages..(15676 writable)..(T=5).GC finished]

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

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

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

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

Summary
Form:  ( DEFTHM ALL-LIST-IN-2<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-IN-2<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-CONS<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-CONS<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-APPEND<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ALL-LIST-APPEND<INVERSEP>

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

Summary
Form:  ( DEFTHM ALL-LIST-REVAPPEND<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-REVAPPEND<INVERSEP>

Summary
Form:  ( ENCAPSULATE NIL (DEFTHM ALL-LIST-REVAPPEND<INVERSEP> ...)
...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
T

Summary
Form:  ( DEFTHM ALL-LIST-REVERSE<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-REVERSE<INVERSEP>

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

Summary
Form:  ( DEFTHM FILTER-LIST-TRUE-LIST<INVERSEP> ...)
Rules: ((:DEFINITION ENDP)
        (:DEFINITION FILTER-LIST<INVERSEP>)
        (:DEFINITION INVERSEP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-LIST-TRUE-LIST<INVERSEP>

Summary
Form:  ( DEFTHM FILTER-LIST-MEMBERSHIP<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-LIST-MEMBERSHIP<INVERSEP>

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

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

Summary
Form:  ( DEFTHM ALL-SFIX<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-SFIX<INVERSEP>

Summary
Form:  ( DEFTHM ALL-TAIL<INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-TYPE<INVERSEP>))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ALL-TAIL<INVERSEP>

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

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

Summary
Form:  ( DEFTHM ALL-IN-2<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-IN-2<INVERSEP>

Summary
Form:  ( DEFTHM ALL-INSERT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-INSERT<INVERSEP>

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

Summary
Form:  ( DEFTHM ALL-DELETE-2<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ALL-DELETE-2<INVERSEP>

Summary
Form:  ( DEFTHM ALL-UNION<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-UNION<INVERSEP>

Summary
Form:  ( DEFTHM ALL-INTERSECT-X<INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-TYPE<INVERSEP>))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-INTERSECT-X<INVERSEP>

Summary
Form:  ( DEFTHM ALL-INTERSECT-Y<INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-TYPE<INVERSEP>))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-INTERSECT-Y<INVERSEP>

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

Summary
Form:  ( DEFTHM ALL-DIFFERENCE-2<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ALL-DIFFERENCE-2<INVERSEP>

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

Summary
Form:  ( DEFTHM FIND-SFIX<INVERSEP> ...)
Rules: ((:DEFINITION FIND<INVERSEP>)
        (:DEFINITION INVERSEP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FIND-SFIX<INVERSEP>

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

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

Summary
Form:  ( DEFTHM FILTER-SFIX<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-SFIX<INVERSEP>

Summary
Form:  ( DEFTHM FILTER-IN<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-IN<INVERSEP>

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

Summary
Form:  ( DEFTHM FILTER-ALL<INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-TYPE<INVERSEP>))
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
FILTER-ALL<INVERSEP>
[SGC for 354 FIXNUM pages..(15897 writable)..(T=4).GC finished]

Summary
Form:  ( DEFTHM FILTER-ALL-2<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.04 seconds (prove: 0.04, print: 0.00, other: 0.00)
FILTER-ALL-2<INVERSEP>

Summary
Form:  ( DEFTHM ALL-MERGESORT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-MERGESORT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-APPLIED-TO-SET<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-APPLIED-TO-SET<INVERSEP>

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

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

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

Summary
Form:  ( DEFTHM ALL-LIST-IN-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-IN-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-IN-2-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-IN-2-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-CONS-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-CONS-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-APPEND-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-APPEND-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-NTH-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-NTH-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-REVAPPEND-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-REVAPPEND-NOT<INVERSEP>

Summary
Form:  ( ENCAPSULATE NIL (DEFTHM ALL-LIST-REVAPPEND-NOT<INVERSEP> ...)
...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
T

Summary
Form:  ( DEFTHM ALL-LIST-REVERSE-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-REVERSE-NOT<INVERSEP>

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

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

Summary
Form:  ( DEFTHM FILTER-LIST-MEMBERSHIP-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-LIST-MEMBERSHIP-NOT<INVERSEP>

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

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

Summary
Form:  ( DEFTHM ALL-SFIX-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-SFIX-NOT<INVERSEP>

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

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

Summary
Form:  ( DEFTHM ALL-IN-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-IN-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-IN-2-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-IN-2-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-INSERT-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ALL-INSERT-NOT<INVERSEP>

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

Summary
Form:  ( DEFTHM ALL-DELETE-2-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-DELETE-2-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-UNION-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-UNION-NOT<INVERSEP>

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

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

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

Summary
Form:  ( DEFTHM ALL-DIFFERENCE-2-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-DIFFERENCE-2-NOT<INVERSEP>

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

Summary
Form:  ( DEFTHM FIND-SFIX-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
FIND-SFIX-NOT<INVERSEP>

Summary
Form:  ( DEFTHM FIND-WITNESS-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FIND-WITNESS-NOT<INVERSEP>

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

Summary
Form:  ( DEFTHM FILTER-SFIX-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-SFIX-NOT<INVERSEP>

Summary
Form:  ( DEFTHM FILTER-IN-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-IN-NOT<INVERSEP>

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

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

Summary
Form:  ( DEFTHM FILTER-ALL-2-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FILTER-ALL-2-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-MERGESORT-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ALL-MERGESORT-NOT<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-APPLIED-TO-SET-NOT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-APPLIED-TO-SET-NOT<INVERSEP>

Summary
Form:  ( ENCAPSULATE NIL (DEFTHM ALL-LIST-TYPE<INVERSEP> ...) ...)
Rules: NIL
Warnings:  None
Time:  0.25 seconds (prove: 0.07, print: 0.00, other: 0.18)
T

Summary
Form:  ( DEFUN ALL-TRIGGER<INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-TYPE<INVERSEP>))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND ALL-TRIGGER<INVERSEP>)

Summary
Form:  ( DEFUN ALL-TRIGGER<NOT-INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-TYPE-NOT<INVERSEP>))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND ALL-TRIGGER<NOT-INVERSEP>)

Summary
Form:  ( DEFUN ALL-LIST-TRIGGER<INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-LIST-TYPE<INVERSEP>))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
(:DEFUND ALL-LIST-TRIGGER<INVERSEP>)

Summary
Form:  ( DEFUN ALL-LIST-TRIGGER<NOT-INVERSEP> ...)
Rules: ((:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT<INVERSEP>))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
[SGC for 354 FIXNUM pages..(15897 writable)..(T=4).GC finished]
(:DEFUND ALL-LIST-TRIGGER<NOT-INVERSEP>)

Summary
Form:  ( DEFTHM ALL-STRATEGY<INVERSEP> ...)
Rules: ((:DEFINITION ALL-TRIGGER<INVERSEP>)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART IF))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-STRATEGY<INVERSEP>

Summary
Form:  ( DEFTHM ALL-STRATEGY<NOT-INVERSEP> ...)
Rules: ((:DEFINITION ALL-TRIGGER<NOT-INVERSEP>)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART IF))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-STRATEGY<NOT-INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-STRATEGY<INVERSEP> ...)
Rules: ((:DEFINITION ALL-LIST-TRIGGER<INVERSEP>)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART IF))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-STRATEGY<INVERSEP>

Summary
Form:  ( DEFTHM ALL-LIST-STRATEGY<NOT-INVERSEP> ...)
Rules: ((:DEFINITION ALL-LIST-TRIGGER<NOT-INVERSEP>)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART IF))
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-STRATEGY<NOT-INVERSEP>

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

Summary
Form:  ( ENCAPSULATE NIL (DEFUN ALL-BY-MEMBERSHIP-HINT<INVERSEP> ...)
...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
T

Summary
Form:  ( DEFUN ALL-BY-MEMBERSHIP-HINT<NOT-INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-BY-MEMBERSHIP-HINT<NOT-INVERSEP>
((PICK-A-POINT-SUBSET-HINT ID CLAUSE
                           WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-BY-MEMBERSHIP-HINT<INVERSEP> ID CLAUSE
                                   WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-BY-MEMBERSHIP-HINT<NOT-INVERSEP> ID CLAUSE
                                       WORLD STABLE-UNDER-SIMPLIFICATIONP))

Summary
Form:  ( ENCAPSULATE NIL (DEFUN ALL-BY-MEMBERSHIP-HINT<NOT-INVERSEP>
...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
T

Summary
Form:  ( DEFUN ALL-LIST-BY-MEMBERSHIP-HINT<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-BY-MEMBERSHIP-HINT<INVERSEP>
((PICK-A-POINT-SUBSET-HINT ID CLAUSE
                           WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-BY-MEMBERSHIP-HINT<INVERSEP> ID CLAUSE
                                   WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-BY-MEMBERSHIP-HINT<NOT-INVERSEP> ID CLAUSE
                                       WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-LIST-BY-MEMBERSHIP-HINT<INVERSEP> ID CLAUSE
                                        WORLD STABLE-UNDER-SIMPLIFICATIONP))

Summary
Form:  ( ENCAPSULATE NIL (DEFUN ALL-LIST-BY-MEMBERSHIP-HINT<INVERSEP>
...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
T

Summary
Form:  ( DEFUN ALL-LIST-BY-MEMBERSHIP-HINT<NOT-INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ALL-LIST-BY-MEMBERSHIP-HINT<NOT-INVERSEP>
((PICK-A-POINT-SUBSET-HINT ID CLAUSE
                           WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-BY-MEMBERSHIP-HINT<INVERSEP> ID CLAUSE
                                   WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-BY-MEMBERSHIP-HINT<NOT-INVERSEP> ID CLAUSE
                                       WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-LIST-BY-MEMBERSHIP-HINT<INVERSEP> ID CLAUSE
                                        WORLD STABLE-UNDER-SIMPLIFICATIONP)
 (ALL-LIST-BY-MEMBERSHIP-HINT<NOT-INVERSEP>
      ID CLAUSE
      WORLD STABLE-UNDER-SIMPLIFICATIONP))

Summary
Form:  ( ENCAPSULATE NIL (DEFUN ALL-LIST-BY-MEMBERSHIP-HINT<NOT-INVERSEP>
...) ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
T

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

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

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

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

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

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

Summary
Form:  ( DEFTHEORY THEORY<INVERSEP> ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
121
[SGC for 10240 CONS pages..(19087 writable)..(T=6).GC finished]
[SGC for 10240 CONS pages..(19087 writable)..(T=6).GC finished]
[SGC for 10240 CONS pages..(19087 writable)..(T=6).GC finished]

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

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

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

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

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


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

Summary
Form:  ( DEFTHM MAP-IN ...)
Rules: ((:DEFINITION ALL<NOT-INVERSEP>)
        (:DEFINITION INVERSEP)
        (:DEFINITION MAP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION ALL<NOT-INVERSEP>)
        (:INDUCTION MAP)
        (:REWRITE ALL-EMPTY-NOT<INVERSEP>)
        (:REWRITE IN-INSERT)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT<INVERSEP>)
        (:TYPE-PRESCRIPTION EMPTY-TYPE)
        (:TYPE-PRESCRIPTION IN-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MAP-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 (SUBSET X Y)))
                     (ALL-SET (LAMBDA NIL (MAP X)))
                     (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                  (SUBSET COMPUTED-HINTS::?X (MAP Y))))
                     (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                        (IN COMPUTED-HINTS::?X (MAP Y))))))
               :EXPAND ((SUBSET-TRIGGER (MAP X) (MAP Y)))))


Summary
Form:  ( DEFTHM MAP-SUBSET ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-SUBSET-NOT<INVERSEP>)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT<INVERSEP>)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
MAP-SUBSET

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


Summary
Form:  ( DEFTHM MAP-INSERT ...)
Rules: ((:DEFINITION INVERSEP)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-INSERT-NOT<INVERSEP>)
        (:REWRITE DOUBLE-CONTAINMENT)
        (:REWRITE IN-INSERT)
        (:REWRITE INSERT-NEVER-EMPTY)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-SETP)
        (:REWRITE MAP-SUBSET)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE NONEMPTY-MEANS-SET)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:REWRITE SUBSET-INSERT)
        (:REWRITE SUBSET-INSERT-X)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.04 seconds (prove: 0.04, print: 0.00, other: 0.00)
MAP-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 (DELETE (TRANSFORM A) (MAP X))))
                (ALL (LAMBDA (COMPUTED-HINTS::?X)
                             (SUBSET COMPUTED-HINTS::?X (MAP (DELETE A X)))))
                (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                   (IN COMPUTED-HINTS::?X
                                       (MAP (DELETE A X)))))))
          :EXPAND ((SUBSET-TRIGGER (DELETE (TRANSFORM A) (MAP X))
                                   (MAP (DELETE A X))))))


Summary
Form:  ( DEFTHM MAP-DELETE ...)
Rules: ((:DEFINITION INVERSEP)
        (:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-DELETE-2-NOT<INVERSEP>)
        (:REWRITE DELETE-IN)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.04 seconds (prove: 0.04, print: 0.00, other: 0.00)
MAP-DELETE

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

("Subgoal 1'"
     (:USE ((:FUNCTIONAL-INSTANCE
                 ALL-BY-MEMBERSHIP
                 (ALL-HYPS (LAMBDA NIL T))
                 (ALL-SET (LAMBDA NIL (UNION (MAP X) (MAP Y))))
                 (ALL (LAMBDA (COMPUTED-HINTS::?X)
                              (SUBSET COMPUTED-HINTS::?X (MAP (UNION X Y)))))
                 (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                    (IN COMPUTED-HINTS::?X
                                        (MAP (UNION X Y)))))))
           :EXPAND ((SUBSET-TRIGGER (UNION (MAP X) (MAP Y))
                                    (MAP (UNION X Y))))))


Summary
Form:  ( DEFTHM MAP-UNION ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-UNION-NOT<INVERSEP>)
        (:REWRITE DOUBLE-CONTAINMENT)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-SETP)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:REWRITE UNION-IN)
        (:REWRITE UNION-SET))
Warnings:  None
Time:  0.20 seconds (prove: 0.20, print: 0.00, other: 0.00)
MAP-UNION

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


Summary
Form:  ( DEFTHM MAP-INTERSECT ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-SUBSET-NOT<INVERSEP>)
        (:REWRITE INTERSECT-IN)
        (:REWRITE INTERSECT-SUBSET-X)
        (:REWRITE INTERSECT-SUBSET-Y)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT<INVERSEP>)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.05 seconds (prove: 0.05, print: 0.00, other: 0.00)
MAP-INTERSECT

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


Summary
Form:  ( DEFTHM MAP-DIFFERENCE ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-DIFFERENCE-2-NOT<INVERSEP>)
        (:REWRITE DIFFERENCE-IN)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION ALL-TYPE-NOT<INVERSEP>)
        (:TYPE-PRESCRIPTION SUBSET-TYPE))
Warnings:  None
Time:  0.11 seconds (prove: 0.11, print: 0.00, other: 0.00)
MAP-DIFFERENCE

Summary
Form:  ( DEFTHM MAP-CARDINALITY ...)
Rules: ((:DEFINITION CARDINALITY)
        (:DEFINITION MAP)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART CARDINALITY)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION CARDINALITY)
        (:INDUCTION MAP)
        (:REWRITE INSERT-CARDINALITY)
        (:REWRITE MAP-IN)
        (:TYPE-PRESCRIPTION CARDINALITY-TYPE)
        (:TYPE-PRESCRIPTION EMPTY-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MAP-CARDINALITY

Summary
Form:  ( DEFTHM MAP-LIST-IN-LIST ...)
Rules: ((:DEFINITION ALL-LIST<NOT-INVERSEP>)
        (:DEFINITION ENDP)
        (:DEFINITION INVERSEP)
        (:DEFINITION MAP-LIST)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART EMPTY)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART SETP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION EXISTS-LIST<INVERSEP>)
        (:INDUCTION MAP-LIST)
        (:REWRITE ALL-LIST-CDR-NOT<INVERSEP>)
        (:REWRITE ALL-LIST-ENDP-NOT<INVERSEP>)
        (:REWRITE EXISTS-LIST-ELIMINATION<INVERSEP>)
        (:REWRITE IN-LIST-CONS)
        (:REWRITE IN-LIST-ON-SET)
        (:REWRITE NEVER-IN-EMPTY)
        (:TYPE-PRESCRIPTION ALL-LIST-TYPE-NOT<INVERSEP>)
        (:TYPE-PRESCRIPTION IN-LIST))
Warnings:  None
Time:  0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
MAP-LIST-IN-LIST

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

("Subgoal 1'"
 (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP
                              (ALL-HYPS (LAMBDA NIL T))
                              (ALL-SET (LAMBDA NIL (MERGESORT (MAP-LIST X))))
                              (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                           (SUBSET COMPUTED-HINTS::?X
                                                   (MAP (MERGESORT X)))))
                              (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                                 (IN COMPUTED-HINTS::?X
                                                     (MAP (MERGESORT X)))))))
       :EXPAND ((SUBSET-TRIGGER (MERGESORT (MAP-LIST X))
                                (MAP (MERGESORT X))))))


Summary
Form:  ( DEFTHM MAP-MERGESORT ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-MERGESORT-NOT<INVERSEP>)
        (:REWRITE DOUBLE-CONTAINMENT)
        (:REWRITE EXISTS-LIST-ELIMINATION<INVERSEP>)
        (:REWRITE IN-MERGESORT)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-LIST-IN-LIST)
        (:REWRITE MAP-SETP)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE MERGESORT-SET)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY))
Warnings:  None
Time:  0.06 seconds (prove: 0.06, print: 0.00, other: 0.00)
MAP-MERGESORT

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

("Subgoal 1'"
 (:USE
  ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP
                         (ALL-HYPS (LAMBDA NIL (SETP X)))
                         (ALL-SET (LAMBDA NIL (MAP X)))
                         (ALL (LAMBDA (COMPUTED-HINTS::?X)
                                      (SUBSET COMPUTED-HINTS::?X
                                              (MERGESORT (MAP-LIST X)))))
                         (PREDICATE (LAMBDA (COMPUTED-HINTS::?X)
                                            (IN COMPUTED-HINTS::?X
                                                (MERGESORT (MAP-LIST X)))))))
  :EXPAND ((SUBSET-TRIGGER (MAP X)
                           (MERGESORT (MAP-LIST X))))))


Summary
Form:  ( DEFTHM MAP-MBE-EQUIVALENCE ...)
Rules: ((:DEFINITION NOT)
        (:DEFINITION SUBSET)
        (:DEFINITION SUBSET-TRIGGER)
        (:DEFINITION SYNP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE ALL-LIST-APPLIED-TO-SET-NOT<INVERSEP>)
        (:REWRITE DOUBLE-CONTAINMENT)
        (:REWRITE EXISTS-LIST-ELIMINATION<INVERSEP>)
        (:REWRITE IN-MERGESORT)
        (:REWRITE MAP-IN)
        (:REWRITE MAP-LIST-IN-LIST)
        (:REWRITE MAP-SETP)
        (:REWRITE MAP-SUBSET-HELPER)
        (:REWRITE MERGESORT-SET)
        (:REWRITE PICK-A-POINT-SUBSET-STRATEGY)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.03 seconds (prove: 0.02, print: 0.00, other: 0.01)
MAP-MBE-EQUIVALENCE

Summary
Form:  ( DEFTHM MAP-LIST-CONS ...)
Rules: ((:DEFINITION MAP-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)
MAP-LIST-CONS

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

Summary
Form:  ( DEFTHM MAP-LIST-NTH ...)
Rules: ((:COMPOUND-RECOGNIZER ACL2::ZP-COMPOUND-RECOGNIZER)
        (:DEFINITION ENDP)
        (:DEFINITION LEN)
        (:DEFINITION MAP-LIST)
        (:DEFINITION NOT)
        (:DEFINITION NTH)
        (:EXECUTABLE-COUNTERPART <)
        (:EXECUTABLE-COUNTERPART INTEGERP)
        (:EXECUTABLE-COUNTERPART NOT)
        (:EXECUTABLE-COUNTERPART ZP)
        (:FAKE-RUNE-FOR-LINEAR NIL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION LEN)
        (:INDUCTION MAP-LIST)
        (:INDUCTION NTH)
        (:REWRITE CDR-CONS)
        (:REWRITE NTH-0-CONS)
        (:TYPE-PRESCRIPTION MAP-LIST))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MAP-LIST-NTH

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

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

Summary
Form:  ( ENCAPSULATE NIL (DEFTHM MAP-SETP ...) ...)
Rules: NIL
Warnings:  None
Time:  0.62 seconds (prove: 0.60, print: 0.00, other: 0.02)
T

Summary
Form:  ( VERIFY-GUARDS MAP)
Rules: ((:DEFINITION MAP)
        (:DEFINITION NOT)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:REWRITE MAP-MBE-EQUIVALENCE)
        (:REWRITE SETS-ARE-TRUE-LISTS)
        (:TYPE-PRESCRIPTION MAP-LIST)
        (:TYPE-PRESCRIPTION SETP-TYPE))
Warnings:  None
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MAP

Summary
Form:  ( DEFUN MAP-FUNCTION-FN ...)
Rules: NIL
Warnings:  None
Time:  0.03 seconds (prove: 0.00, print: 0.00, other: 0.03)
MAP-FUNCTION-FN

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

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

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

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..(19569 writable)..(T=6).GC finished]
[SGC for 0 RELOCATABLE-BLOCKS pages..(19569 writable)..(T=5).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o
start address -T 0x9e183c0 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/sets.o
[SGC for 10240 CONS pages..(52077 writable)..(T=6).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/quantify.o
start address -T 0x9f46540 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/quantify.o
[SGC for 10240 CONS pages..(52077 writable)..(T=7).GC finished]
[SGC for 10240 CONS pages..(52077 writable)..(T=6).GC finished]
[SGC for 10240 CONS pages..(52077 writable)..(T=6).GC finished]

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

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

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

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

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

ACL2>