GCL (GNU Common Lisp) 2.6.6 CLtL1 Jan 19 2005 20:24:14 Source License: LGPL(gcl,gmp), GPL(unexec,bfd) Binary License: GPL due to GPL'ed components: (BFD UNEXEC) Modifications of this banner must retain notice of a compatible license Dedicated to the memory of W. Schelter Use (help) to get some basic information on how to use GCL. ACL2 Version 2.9.3 built August 2, 2005 18:40:53. Copyright (C) 2005 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES* NIL). See the documentation topic note-2-9-3 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. NOTE!! Proof trees are disabled in ACL2. To enable them in emacs, look under the ACL2 source directory in interface/emacs/README.doc; and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 command loop. Look in the ACL2 documentation under PROOF-TREE. ACL2 Version 2.9.3. Level 1. Cbd "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2> #<"ACL2" package> ACL2> ACL2 Version 2.9.3. Level 1. Cbd "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT) ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2> ACL2 Version 2.9.3. Level 1. Cbd "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 Version 2.9.3. Level 2. Cbd "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>> Summary Form: ( DEFPKG "INSTANCE" ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) "INSTANCE" ACL2 !>> Summary Form: ( DEFPKG "COMPUTED-HINTS" ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) "COMPUTED-HINTS" ACL2 !>>[SGC for 444 CONS pages..(8302 writable)..(T=0).GC finished] Summary Form: ( DEFPKG "SETS" ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) "SETS" ACL2 !>>Bye. :EOF ACL2 !>[SGC for 444 CONS pages..(8306 writable)..(T=0).GC finished] [SGC for 12 STRING pages..(9027 writable)..(T=1).GC finished] [SGC for 12 STRING pages..(9027 writable)..(T=2).GC finished] [SGC for 20 CFUN pages..(9062 writable)..(T=1).GC finished] [SGC for 20 CFUN pages..(9066 writable)..(T=1).GC finished] Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o start address -T 0x91e9000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o [SGC for 1281 CONS pages..(9200 writable)..(T=1).GC finished] Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o start address -T 0x9e95000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o start address -T 0x89e1000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o start address -T 0x93f4000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o [SGC for 25 FIXNUM pages..(9534 writable)..(T=1).GC finished] Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o start address -T 0x89e2300 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o Summary Form: ( INCLUDE-BOOK "fast" ...) Rules: NIL Warnings: None Time: 0.38 seconds (prove: 0.00, print: 0.00, other: 0.38) "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.lisp" 2 Summary Form: ( DEFUN DELETE ...) Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DELETE Summary Form: ( DEFTHM DELETE-SET ...) Rules: ((:DEFINITION DELETE) (:EXECUTABLE-COUNTERPART SETP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DELETE) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE TAIL-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) DELETE-SET Summary Form: ( VERIFY-GUARDS DELETE) Rules: ((:EXECUTABLE-COUNTERPART IF) (:REWRITE DELETE-SET) (:REWRITE TAIL-PRODUCES-SET)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DELETE Summary Form: ( DEFTHM DELETE-PRESERVES-EMPTY ...) Rules: ((:DEFINITION DELETE) (:EXECUTABLE-COUNTERPART EMPTY) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DELETE-PRESERVES-EMPTY Summary Form: ( DEFTHM DELETE-IN ...) Rules: ((:DEFINITION DELETE) (:DEFINITION IN) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART EMPTY) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:INDUCTION DELETE) (:INDUCTION IN) (:REWRITE HEAD-UNIQUE) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE NEVER-IN-EMPTY) (:REWRITE SUBSET-IN) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) DELETE-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: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (DELETE A (SFIX X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A X)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A X)))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (SFIX X)) (DELETE A 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 (DELETE A X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (SFIX X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (SFIX X))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A X) (DELETE A (SFIX X)))))) Summary Form: ( DEFTHM DELETE-SFIX-CANCEL ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-SET) (:REWRITE IN-SFIX-CANCEL) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SFIX-SET-IDENTITY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.03 seconds (prove: 0.03, print: 0.00, other: 0.00) DELETE-SFIX-CANCEL 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 (NOT (IN A X)))) (ALL-SET (LAMBDA NIL (DELETE A X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X X))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X X))))) :EXPAND ((SUBSET-TRIGGER (DELETE A X) 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 (NOT (IN A X)))) (ALL-SET (LAMBDA NIL X)) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A X)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A X)))))) :EXPAND ((SUBSET-TRIGGER X (DELETE A X))))) Summary Form: ( DEFTHM DELETE-NONMEMBER-CANCEL ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SFIX-PRODUCES-SET) (:REWRITE SUBSET-SFIX-CANCEL-X) (:REWRITE SUBSET-SFIX-CANCEL-Y) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) DELETE-NONMEMBER-CANCEL 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 (DELETE A (DELETE B X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE B (DELETE A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE B (DELETE A X))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (DELETE B X)) (DELETE B (DELETE A 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 (DELETE B (DELETE A X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (DELETE B X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (DELETE B X))))))) :EXPAND ((SUBSET-TRIGGER (DELETE B (DELETE A X)) (DELETE A (DELETE B X)))))) Summary Form: ( DEFTHM DELETE-DELETE ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.06 seconds (prove: 0.06, print: 0.00, other: 0.00) DELETE-DELETE Summary Form: ( DEFTHM REPEATED-DELETE ...) Rules: ((:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-NONMEMBER-CANCEL) (:REWRITE DELETE-SET) (:REWRITE SFIX-SET-IDENTITY)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) REPEATED-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 (DELETE A (INSERT A X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A X)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A X)))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (INSERT A X)) (DELETE A 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 (DELETE A X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (INSERT A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (INSERT A X))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A X) (DELETE A (INSERT A X)))))) Summary Form: ( DEFTHM DELETE-INSERT-CANCEL ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.05 seconds (prove: 0.05, print: 0.00, other: 0.00) DELETE-INSERT-CANCEL 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 (DELETE A X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT A X)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT A X)))))) :EXPAND ((SUBSET-TRIGGER (DELETE A X) (INSERT A 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 X)) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT A (DELETE A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT A (DELETE A X))))))) :EXPAND ((SUBSET-TRIGGER X (INSERT A (DELETE A X)))))) Summary Form: ( DEFTHM INSERT-DELETE-CANCEL ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SUBSET-INSERT-X) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.03 seconds (prove: 0.03, print: 0.00, other: 0.00) INSERT-DELETE-CANCEL 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 A X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X X))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X X))))) :EXPAND ((SUBSET-TRIGGER (DELETE A X) X)))) Summary Form: ( DEFTHM SUBSET-DELETE ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:REWRITE DELETE-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) SUBSET-DELETE Summary Form: ( DEFUN UNION ...) 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) UNION Summary Form: ( DEFTHM UNION-SET ...) Rules: ((:DEFINITION UNION) (:INDUCTION UNION) (: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) UNION-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 (UNION (SFIX X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Y)))))) :EXPAND ((SUBSET-TRIGGER (UNION (SFIX X) Y) (UNION X Y))))) Summary Form: ( DEFTHM UNION-SFIX-CANCEL-X ...) Rules: ((:DEFINITION UNION) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION UNION) (: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.01, print: 0.00, other: 0.00) UNION-SFIX-CANCEL-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (UNION X (SFIX Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Y)))))) :EXPAND ((SUBSET-TRIGGER (UNION X (SFIX Y)) (UNION X Y))))) Summary Form: ( DEFTHM UNION-SFIX-CANCEL-Y ...) Rules: ((:DEFINITION UNION) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION UNION) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-PRODUCES-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-INSERT) (:REWRITE SUBSET-INSERT-X) (:REWRITE SUBSET-TRANSITIVE) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) UNION-SFIX-CANCEL-Y Summary Form: ( DEFTHM UNION-EMPTY-X ...) Rules: ((:DEFINITION UNION) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) UNION-EMPTY-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (EMPTY Y))) (ALL-SET (LAMBDA NIL (UNION X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X X))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X X))))) :EXPAND ((SUBSET-TRIGGER (UNION X Y) X)))) Summary Form: ( DEFTHM UNION-EMPTY-Y ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION UNION) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:INDUCTION UNION) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE EMPTY-SUBSET-2) (:REWRITE HEAD-UNIQUE) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-PRODUCES-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-IN-2) (:REWRITE SUBSET-INSERT) (:REWRITE SUBSET-INSERT-X) (:REWRITE SUBSET-TRANSITIVE) (:REWRITE TAIL-PRODUCES-SET) (:REWRITE UNION-EMPTY-X) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) UNION-EMPTY-Y Summary Form: ( DEFTHM UNION-EMPTY ...) Rules: ((:DEFINITION UNION) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION UNION) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE UNION-EMPTY-X) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) UNION-EMPTY Summary Form: ( DEFTHM UNION-IN ...) Rules: ((:DEFINITION IN) (:DEFINITION UNION) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:INDUCTION IN) (:INDUCTION UNION) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE IN-SFIX-CANCEL) (:REWRITE NEVER-IN-EMPTY) (:REWRITE SUBSET-IN) (:REWRITE UNION-EMPTY-X) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) UNION-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: ("Subgoal 2.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (SETP X) (EMPTY X)))) (ALL-SET (LAMBDA NIL Y)) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (FAST-UNION X Y 'NIL)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (FAST-UNION X Y 'NIL)))))) :EXPAND ((SUBSET-TRIGGER Y (FAST-UNION X Y 'NIL))))) 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (SETP X) (EMPTY X)))) (ALL-SET (LAMBDA NIL (FAST-UNION X Y 'NIL))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X Y))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X Y))))) :EXPAND ((SUBSET-TRIGGER (FAST-UNION X Y 'NIL) 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (NOT (EMPTY X))))) (ALL-SET (LAMBDA NIL (UNION (TAIL X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (FAST-UNION X Y 'NIL)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (FAST-UNION X Y 'NIL)))))) :EXPAND ((SUBSET-TRIGGER (UNION (TAIL X) Y) (FAST-UNION X Y 'NIL))))) [SGC for 2708 CONS pages..(10962 writable)..(T=2).GC finished] 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (NOT (EMPTY X))))) (ALL-SET (LAMBDA NIL (FAST-UNION X Y 'NIL))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT (HEAD X) (UNION (TAIL X) Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT (HEAD X) (UNION (TAIL X) Y))))))) :EXPAND ((SUBSET-TRIGGER (FAST-UNION X Y 'NIL) (INSERT (HEAD X) (UNION (TAIL X) Y)))))) Summary Form: ( VERIFY-GUARDS UNION ...) Rules: ((:DEFINITION IN) (:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE FAST-UNION-MEMBERSHIP) (:REWRITE FAST-UNION-SET) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE IN-SET) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NEVER-IN-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-IN) (:REWRITE SUBSET-INSERT-X) (:REWRITE UNION-IN) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SETP-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.10 seconds (prove: 0.10, print: 0.00, other: 0.00) 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: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (UNION X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION Y X)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION Y X)))))) :EXPAND ((SUBSET-TRIGGER (UNION X Y) (UNION Y 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 (UNION Y X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Y)))))) :EXPAND ((SUBSET-TRIGGER (UNION Y X) (UNION X Y))))) Summary Form: ( DEFTHM UNION-SYMMETRIC ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.05 seconds (prove: 0.04, print: 0.00, other: 0.01) UNION-SYMMETRIC We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Goal'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL X)) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Y)))))) :EXPAND ((SUBSET-TRIGGER X (UNION X Y))))) Summary Form: ( DEFTHM UNION-SUBSET-X ...) Rules: ((:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) UNION-SUBSET-X We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Goal'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL Y)) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Y)))))) :EXPAND ((SUBSET-TRIGGER Y (UNION X Y))))) Summary Form: ( DEFTHM UNION-SUBSET-Y ...) Rules: ((:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) UNION-SUBSET-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (UNION Y (INSERT A X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT A (UNION X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT A (UNION X Y))))))) :EXPAND ((SUBSET-TRIGGER (UNION Y (INSERT A X)) (INSERT A (UNION X 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 X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION Y (INSERT A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION Y (INSERT A X))))))) :EXPAND ((SUBSET-TRIGGER (UNION X Y) (UNION Y (INSERT A X)))))) Summary Form: ( DEFTHM UNION-INSERT-X ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SUBSET-INSERT-X) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:REWRITE UNION-SYMMETRIC) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.06 seconds (prove: 0.05, print: 0.00, other: 0.01) UNION-INSERT-X We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (UNION X (INSERT A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT A (UNION X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT A (UNION X Y))))))) :EXPAND ((SUBSET-TRIGGER (UNION X (INSERT A Y)) (INSERT A (UNION X 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 X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X (INSERT A Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X (INSERT A Y))))))) :EXPAND ((SUBSET-TRIGGER (UNION X Y) (UNION X (INSERT A Y)))))) Summary Form: ( DEFTHM UNION-INSERT-Y ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SUBSET-INSERT-X) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.04 seconds (prove: 0.04, print: 0.00, other: 0.00) UNION-INSERT-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 2.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A Y))) (ALL-SET (LAMBDA NIL (UNION Y (DELETE A X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Y)))))) :EXPAND ((SUBSET-TRIGGER (UNION Y (DELETE A X)) (UNION X 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 2.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A Y))) (ALL-SET (LAMBDA NIL (UNION X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION Y (DELETE A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION Y (DELETE A X))))))) :EXPAND ((SUBSET-TRIGGER (UNION X Y) (UNION Y (DELETE A 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A Y)))) (ALL-SET (LAMBDA NIL (UNION Y (DELETE A X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (UNION X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (UNION X Y))))))) :EXPAND ((SUBSET-TRIGGER (UNION Y (DELETE A X)) (DELETE A (UNION X 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A Y)))) (ALL-SET (LAMBDA NIL (DELETE A (UNION X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION Y (DELETE A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION Y (DELETE A X))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (UNION X Y)) (UNION Y (DELETE A X)))))) Summary Form: ( DEFTHM UNION-DELETE-X ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:REWRITE UNION-SYMMETRIC) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.14 seconds (prove: 0.14, print: 0.00, other: 0.00) UNION-DELETE-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 2.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A X))) (ALL-SET (LAMBDA NIL (UNION X (DELETE A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Y)))))) :EXPAND ((SUBSET-TRIGGER (UNION X (DELETE A Y)) (UNION X Y))))) [SGC for 2708 CONS pages..(10963 writable)..(T=3).GC finished] 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A X))) (ALL-SET (LAMBDA NIL (UNION X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X (DELETE A Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X (DELETE A Y))))))) :EXPAND ((SUBSET-TRIGGER (UNION X Y) (UNION X (DELETE A 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A X)))) (ALL-SET (LAMBDA NIL (UNION X (DELETE A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (UNION X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (UNION X Y))))))) :EXPAND ((SUBSET-TRIGGER (UNION X (DELETE A Y)) (DELETE A (UNION X 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A X)))) (ALL-SET (LAMBDA NIL (DELETE A (UNION X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X (DELETE A Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X (DELETE A Y))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (UNION X Y)) (UNION X (DELETE A Y)))))) Summary Form: ( DEFTHM UNION-DELETE-Y ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.14 seconds (prove: 0.14, print: 0.00, other: 0.00) UNION-DELETE-Y We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Goal''" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (UNION X X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X X))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X X))))) :EXPAND ((SUBSET-TRIGGER (UNION X X) X)))) Summary Form: ( DEFTHM UNION-SELF ...) Rules: ((:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SFIX-PRODUCES-SET) (:REWRITE SUBSET-SFIX-CANCEL-X) (:REWRITE SUBSET-SFIX-CANCEL-Y) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:REWRITE UNION-SUBSET-Y) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) UNION-SELF 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 (UNION Z (UNION X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X (UNION Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X (UNION Y Z))))))) :EXPAND ((SUBSET-TRIGGER (UNION Z (UNION X Y)) (UNION X (UNION Y Z)))))) 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 X (UNION Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION Z (UNION X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION Z (UNION X Y))))))) :EXPAND ((SUBSET-TRIGGER (UNION X (UNION Y Z)) (UNION Z (UNION X Y)))))) Summary Form: ( DEFTHM UNION-ASSOCIATIVE ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:REWRITE UNION-SYMMETRIC) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.08 seconds (prove: 0.08, print: 0.00, other: 0.00) UNION-ASSOCIATIVE 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 (UNION X (UNION Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION Y (UNION X Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION Y (UNION X Z))))))) :EXPAND ((SUBSET-TRIGGER (UNION X (UNION Y Z)) (UNION Y (UNION X Z)))))) 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 Y (UNION X Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X (UNION Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X (UNION Y Z))))))) :EXPAND ((SUBSET-TRIGGER (UNION Y (UNION X Z)) (UNION X (UNION Y Z)))))) Summary Form: ( DEFTHM UNION-COMMUTATIVE ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.07 seconds (prove: 0.07, print: 0.00, other: 0.00) UNION-COMMUTATIVE 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 (UNION X (UNION X Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X Z)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X Z)))))) :EXPAND ((SUBSET-TRIGGER (UNION X (UNION X Z)) (UNION X Z))))) Summary Form: ( DEFTHM UNION-OUTER-CANCEL ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:REWRITE UNION-SUBSET-Y) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) UNION-OUTER-CANCEL Summary Form: ( DEFUN INTERSECT ...) 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) INTERSECT Summary Form: ( DEFTHM INTERSECT-SET ...) Rules: ((:DEFINITION INTERSECT) (:INDUCTION INTERSECT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-PRODUCES-SET) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SETP-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) INTERSECT-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 (INTERSECT (SFIX X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X Y)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT (SFIX X) Y) (INTERSECT X Y))))) Summary Form: ( DEFTHM INTERSECT-SFIX-CANCEL-X ...) Rules: ((:DEFINITION INTERSECT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION INTERSECT) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-PRODUCES-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE TAIL-PRODUCES-SET) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) INTERSECT-SFIX-CANCEL-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (INTERSECT X (SFIX Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X Y)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X (SFIX Y)) (INTERSECT X Y))))) Summary Form: ( DEFTHM INTERSECT-SFIX-CANCEL-Y ...) Rules: ((:DEFINITION INTERSECT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION INTERSECT) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-SET) (:REWRITE IN-SFIX-CANCEL) (:REWRITE INTERSECT-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-TRANSITIVE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) INTERSECT-SFIX-CANCEL-Y Summary Form: ( DEFTHM INTERSECT-EMPTY-X ...) Rules: ((:DEFINITION INTERSECT) (:REWRITE EMPTY-SFIX-CANCEL) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) INTERSECT-EMPTY-X Summary Form: ( DEFTHM INTERSECT-EMPTY-Y ...) Rules: ((:DEFINITION INTERSECT) (:INDUCTION INTERSECT) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE NEVER-IN-EMPTY) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) INTERSECT-EMPTY-Y Summary Form: ( DEFTHM INTERSECT-IN-Y ...) Rules: ((:DEFINITION INTERSECT) (:DEFINITION NOT) (:INDUCTION INTERSECT) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE IN-INSERT) (: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) INTERSECT-IN-Y [SGC for 2708 CONS pages..(10963 writable)..(T=2).GC finished] Summary Form: ( DEFTHM INTERSECT-IN-X ...) Rules: ((:DEFINITION IN) (:DEFINITION INTERSECT) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:INDUCTION IN) (:INDUCTION INTERSECT) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE IN-INSERT) (:REWRITE NEVER-IN-EMPTY) (:REWRITE SUBSET-IN) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.04 seconds (prove: 0.03, print: 0.00, other: 0.01) INTERSECT-IN-X Summary Form: ( DEFTHM INTERSECT-IN ...) Rules: ((:DEFINITION IN) (:DEFINITION INTERSECT) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION IN) (:INDUCTION INTERSECT) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE HEAD-UNIQUE) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE INTERSECT-IN-X) (:REWRITE INTERSECT-IN-Y) (: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) INTERSECT-IN Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: None Time: 0.07 seconds (prove: 0.06, print: 0.00, other: 0.01) T 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (NOT (EMPTY X)) (NOT (IN (HEAD X) Y))))) (ALL-SET (LAMBDA NIL (INTERSECT (TAIL X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (FAST-INTERSECT X Y 'NIL)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (FAST-INTERSECT X Y 'NIL)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT (TAIL X) Y) (FAST-INTERSECT X Y 'NIL))))) 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (NOT (EMPTY X)) (NOT (IN (HEAD X) Y))))) (ALL-SET (LAMBDA NIL (FAST-INTERSECT X Y 'NIL))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT (TAIL X) Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT (TAIL X) Y)))))) :EXPAND ((SUBSET-TRIGGER (FAST-INTERSECT X Y 'NIL) (INTERSECT (TAIL X) 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (NOT (EMPTY X)) (IN (HEAD X) Y)))) (ALL-SET (LAMBDA NIL (INTERSECT (TAIL X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (FAST-INTERSECT X Y 'NIL)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (FAST-INTERSECT X Y 'NIL)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT (TAIL X) Y) (FAST-INTERSECT X Y 'NIL))))) 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (NOT (EMPTY X)) (IN (HEAD X) Y)))) (ALL-SET (LAMBDA NIL (FAST-INTERSECT X Y 'NIL))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT (HEAD X) (INTERSECT (TAIL X) Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT (HEAD X) (INTERSECT (TAIL X) Y))))))) :EXPAND ((SUBSET-TRIGGER (FAST-INTERSECT X Y 'NIL) (INSERT (HEAD X) (INTERSECT (TAIL X) Y)))))) Summary Form: ( VERIFY-GUARDS INTERSECT ...) Rules: ((:DEFINITION IN) (:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE FAST-INTERSECT-EMPTY) (:REWRITE FAST-INTERSECT-MEMBERSHIP) (:REWRITE FAST-INTERSECT-SET) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE IN-SET) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-IN) (:REWRITE SUBSET-INSERT-X) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SETP-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.14 seconds (prove: 0.13, print: 0.00, other: 0.01) 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: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (INTERSECT X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT Y X)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT Y X)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X Y) (INTERSECT Y 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 (INTERSECT Y X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X Y)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT Y X) (INTERSECT X Y))))) Summary Form: ( DEFTHM INTERSECT-SYMMETRIC ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.05 seconds (prove: 0.05, print: 0.00, other: 0.00) INTERSECT-SYMMETRIC 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 (INTERSECT X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X X))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X X))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X Y) X)))) Summary Form: ( DEFTHM INTERSECT-SUBSET-X ...) Rules: ((:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:REWRITE INTERSECT-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) INTERSECT-SUBSET-X We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Goal'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (INTERSECT X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X Y))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X Y))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X Y) Y)))) Summary Form: ( DEFTHM INTERSECT-SUBSET-Y ...) Rules: ((:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:REWRITE INTERSECT-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) INTERSECT-SUBSET-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A Y)))) (ALL-SET (LAMBDA NIL (INTERSECT Y (INSERT A X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X Y)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT Y (INSERT A X)) (INTERSECT X 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 (NOT (IN A Y)))) (ALL-SET (LAMBDA NIL (INTERSECT X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT Y (INSERT A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT Y (INSERT A X))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X Y) (INTERSECT Y (INSERT A X)))))) Summary Form: ( DEFTHM INTERSECT-INSERT-X ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE INTERSECT-SYMMETRIC) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.05 seconds (prove: 0.05, print: 0.00, other: 0.00) INTERSECT-INSERT-X We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A X)))) (ALL-SET (LAMBDA NIL (INTERSECT X (INSERT A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X Y)))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X (INSERT A Y)) (INTERSECT X 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 (NOT (IN A X)))) (ALL-SET (LAMBDA NIL (INTERSECT X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X (INSERT A Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X (INSERT A Y))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X Y) (INTERSECT X (INSERT A Y)))))) Summary Form: ( DEFTHM INTERSECT-INSERT-Y ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.05 seconds (prove: 0.05, print: 0.00, other: 0.00) INTERSECT-INSERT-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (INTERSECT Y (DELETE A X)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (INTERSECT X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (INTERSECT X Y))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT Y (DELETE A X)) (DELETE A (INTERSECT X 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 (DELETE A (INTERSECT X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT Y (DELETE A X))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT Y (DELETE A X))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (INTERSECT X Y)) (INTERSECT Y (DELETE A X)))))) Summary Form: ( DEFTHM INTERSECT-DELETE-X ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE INTERSECT-SYMMETRIC) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.10 seconds (prove: 0.10, print: 0.00, other: 0.00) INTERSECT-DELETE-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (INTERSECT X (DELETE A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (INTERSECT X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (INTERSECT X Y))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X (DELETE A Y)) (DELETE A (INTERSECT X 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 (DELETE A (INTERSECT X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X (DELETE A Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X (DELETE A Y))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (INTERSECT X Y)) (INTERSECT X (DELETE A Y)))))) Summary Form: ( DEFTHM INTERSECT-DELETE-Y ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.06 seconds (prove: 0.06, print: 0.00, other: 0.00) INTERSECT-DELETE-Y We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Goal''" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL X)) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X X)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X X)))))) :EXPAND ((SUBSET-TRIGGER X (INTERSECT X X))))) Summary Form: ( DEFTHM INTERSECT-SELF ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE INTERSECT-SUBSET-Y) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SFIX-PRODUCES-SET) (:REWRITE SUBSET-SFIX-CANCEL-X) (:REWRITE SUBSET-SFIX-CANCEL-Y) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) INTERSECT-SELF 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 (INTERSECT Z (INTERSECT X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X (INTERSECT Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X (INTERSECT Y Z))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT Z (INTERSECT X Y)) (INTERSECT X (INTERSECT Y Z)))))) 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 (INTERSECT X (INTERSECT Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT Z (INTERSECT X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT Z (INTERSECT X Y))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X (INTERSECT Y Z)) (INTERSECT Z (INTERSECT X Y)))))) Summary Form: ( DEFTHM INTERSECT-ASSOCIATIVE ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE INTERSECT-SYMMETRIC) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.12 seconds (prove: 0.12, print: 0.00, other: 0.00) INTERSECT-ASSOCIATIVE 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 (UNION X (INTERSECT Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT (UNION X Y) (UNION X Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT (UNION X Y) (UNION X Z))))))) :EXPAND ((SUBSET-TRIGGER (UNION X (INTERSECT Y Z)) (INTERSECT (UNION X Y) (UNION X Z)))))) 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 (INTERSECT (UNION X Y) (UNION X Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION X (INTERSECT Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION X (INTERSECT Y Z))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT (UNION X Y) (UNION X Z)) (UNION X (INTERSECT Y Z)))))) Summary Form: ( DEFTHM UNION-OVER-INTERSECT ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.13 seconds (prove: 0.13, print: 0.00, other: 0.00) UNION-OVER-INTERSECT [SGC for 5237 CONS pages..(13492 writable)..(T=3).GC finished] 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 (INTERSECT X (UNION Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X (INTERSECT (UNION X Y) (INTERSECT (UNION X Z) (UNION Y Z))))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X (INTERSECT (UNION X Y) (INTERSECT (UNION X Z) (UNION Y Z))))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X (UNION Y Z)) (INTERSECT X (INTERSECT (UNION X Y) (INTERSECT (UNION X Z) (UNION Y Z)))))))) 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 (INTERSECT X (INTERSECT (UNION X Y) (INTERSECT (UNION X Z) (UNION Y Z)))))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X (UNION Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X (UNION Y Z))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X (INTERSECT (UNION X Y) (INTERSECT (UNION X Z) (UNION Y Z)))) (INTERSECT X (UNION Y Z)))))) Summary Form: ( DEFTHM INTERSECT-OVER-UNION ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-ASSOCIATIVE) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE INTERSECT-SFIX-CANCEL-X) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-OVER-INTERSECT) (:REWRITE UNION-SELF) (:REWRITE UNION-SYMMETRIC) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.27 seconds (prove: 0.27, print: 0.00, other: 0.00) INTERSECT-OVER-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: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (INTERSECT X (INTERSECT Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT Y (INTERSECT X Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT Y (INTERSECT X Z))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X (INTERSECT Y Z)) (INTERSECT Y (INTERSECT X Z)))))) 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 (INTERSECT Y (INTERSECT X Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X (INTERSECT Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X (INTERSECT Y Z))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT Y (INTERSECT X Z)) (INTERSECT X (INTERSECT Y Z)))))) Summary Form: ( DEFTHM INTERSECT-COMMUTATIVE ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.09 seconds (prove: 0.09, print: 0.00, other: 0.00) INTERSECT-COMMUTATIVE 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 (INTERSECT X Z))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT X (INTERSECT X Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT X (INTERSECT X Z))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT X Z) (INTERSECT X (INTERSECT X Z)))))) Summary Form: ( DEFTHM INTERSECT-OUTER-CANCEL ...) Rules: ((:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE INTERSECT-SUBSET-Y) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.05 seconds (prove: 0.05, print: 0.00, other: 0.00) INTERSECT-OUTER-CANCEL Summary Form: ( DEFUN DIFFERENCE ...) 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) DIFFERENCE Summary Form: ( DEFTHM DIFFERENCE-SET ...) Rules: ((:DEFINITION DIFFERENCE) (:INDUCTION DIFFERENCE) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-PRODUCES-SET) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SETP-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DIFFERENCE-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 (DIFFERENCE (SFIX X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X Y)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE (SFIX X) Y) (DIFFERENCE X Y))))) Summary Form: ( DEFTHM DIFFERENCE-SFIX-X ...) Rules: ((:DEFINITION DIFFERENCE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DIFFERENCE) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-PRODUCES-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE TAIL-PRODUCES-SET) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) DIFFERENCE-SFIX-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (DIFFERENCE X (SFIX Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X Y)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X (SFIX Y)) (DIFFERENCE X Y))))) Summary Form: ( DEFTHM DIFFERENCE-SFIX-Y ...) Rules: ((:DEFINITION DIFFERENCE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DIFFERENCE) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE IN-SET) (:REWRITE IN-SFIX-CANCEL) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-INSERT) (:REWRITE SUBSET-INSERT-X) (:REWRITE SUBSET-TRANSITIVE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) DIFFERENCE-SFIX-Y Summary Form: ( DEFTHM DIFFERENCE-EMPTY-X ...) Rules: ((:DEFINITION DIFFERENCE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DIFFERENCE-EMPTY-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (EMPTY Y))) (ALL-SET (LAMBDA NIL (DIFFERENCE X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X X))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X X))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X Y) X)))) Summary Form: ( DEFTHM DIFFERENCE-EMPTY-Y ...) Rules: ((:DEFINITION DIFFERENCE) (:DEFINITION NOT) (:DEFINITION SUBSET) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:INDUCTION DIFFERENCE) (:REWRITE DIFFERENCE-EMPTY-X) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE HEAD-UNIQUE) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NEVER-IN-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-IN-2) (:REWRITE SUBSET-INSERT) (:REWRITE SUBSET-INSERT-X) (:REWRITE SUBSET-TRANSITIVE) (:REWRITE TAIL-PRODUCES-SET) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) DIFFERENCE-EMPTY-Y Summary Form: ( DEFTHM DIFFERENCE-IN-X ...) Rules: ((:DEFINITION DIFFERENCE) (:DEFINITION IN) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:INDUCTION DIFFERENCE) (:INDUCTION IN) (:REWRITE DIFFERENCE-EMPTY-X) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE NEVER-IN-EMPTY) (:REWRITE SUBSET-IN) (: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) DIFFERENCE-IN-X Summary Form: ( DEFTHM DIFFERENCE-IN-Y ...) Rules: ((:DEFINITION DIFFERENCE) (:DEFINITION NOT) (:INDUCTION DIFFERENCE) (:REWRITE DIFFERENCE-EMPTY-X) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE IN-INSERT) (: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) DIFFERENCE-IN-Y Summary Form: ( DEFTHM DIFFERENCE-IN ...) Rules: ((:DEFINITION DIFFERENCE) (:DEFINITION IN) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DIFFERENCE) (:INDUCTION IN) (:REWRITE DIFFERENCE-IN-X) (:REWRITE DIFFERENCE-IN-Y) (:REWRITE IN-INSERT) (:REWRITE IN-TAIL-OR-HEAD) (:REWRITE INSERT-IDENTITY) (: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) DIFFERENCE-IN Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: None Time: 0.03 seconds (prove: 0.03, print: 0.00, other: 0.00) T 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (NOT (EMPTY X)) (NOT (IN (HEAD X) Y))))) (ALL-SET (LAMBDA NIL (DIFFERENCE (TAIL X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (FAST-DIFFERENCE X Y 'NIL)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (FAST-DIFFERENCE X Y 'NIL)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE (TAIL X) Y) (FAST-DIFFERENCE X Y 'NIL))))) 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (SETP Y) (NOT (EMPTY X)) (NOT (IN (HEAD X) Y))))) (ALL-SET (LAMBDA NIL (FAST-DIFFERENCE X Y 'NIL))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT (HEAD X) (DIFFERENCE (TAIL X) Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT (HEAD X) (DIFFERENCE (TAIL X) Y))))))) :EXPAND ((SUBSET-TRIGGER (FAST-DIFFERENCE X Y 'NIL) (INSERT (HEAD X) (DIFFERENCE (TAIL X) 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (NOT (EMPTY X)) (IN (HEAD X) Y)))) (ALL-SET (LAMBDA NIL (DIFFERENCE (TAIL X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (FAST-DIFFERENCE X Y 'NIL)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (FAST-DIFFERENCE X Y 'NIL)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE (TAIL X) Y) (FAST-DIFFERENCE X Y 'NIL))))) 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (AND (NOT (EMPTY X)) (IN (HEAD X) Y)))) (ALL-SET (LAMBDA NIL (FAST-DIFFERENCE X Y 'NIL))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE (TAIL X) Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE (TAIL X) Y)))))) :EXPAND ((SUBSET-TRIGGER (FAST-DIFFERENCE X Y 'NIL) (DIFFERENCE (TAIL X) Y))))) Summary Form: ( VERIFY-GUARDS DIFFERENCE ...) Rules: ((:DEFINITION IN) (:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:REWRITE DIFFERENCE-IN) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE FAST-DIFFERENCE-EMPTY) (:REWRITE FAST-DIFFERENCE-MEMBERSHIP) (:REWRITE FAST-DIFFERENCE-SET) (:REWRITE IN-HEAD) (:REWRITE IN-INSERT) (:REWRITE IN-SET) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-IN) (:REWRITE SUBSET-INSERT-X) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SETP-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.12 seconds (prove: 0.11, print: 0.00, other: 0.01) DIFFERENCE 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 X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X X))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X X))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X Y) X)))) Summary Form: ( DEFTHM DIFFERENCE-SUBSET-X ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:REWRITE DIFFERENCE-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) DIFFERENCE-SUBSET-X Summary Form: ( DEFTHM SUBSET-DIFFERENCE ...) Rules: ((:DEFINITION DIFFERENCE) (:DEFINITION SUBSET) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DIFFERENCE) (:INDUCTION SUBSET) (:REWRITE DIFFERENCE-EMPTY-X) (:REWRITE EMPTY-SFIX-CANCEL) (:REWRITE EMPTY-SUBSET) (:REWRITE INSERT-NEVER-EMPTY) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) SUBSET-DIFFERENCE 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 (DIFFERENCE X (UNION Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INTERSECT (DIFFERENCE X Y) (DIFFERENCE X Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INTERSECT (DIFFERENCE X Y) (DIFFERENCE X Z))))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X (UNION Y Z)) (INTERSECT (DIFFERENCE X Y) (DIFFERENCE X Z)))))) 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 (INTERSECT (DIFFERENCE X Y) (DIFFERENCE X Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X (UNION Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X (UNION Y Z))))))) :EXPAND ((SUBSET-TRIGGER (INTERSECT (DIFFERENCE X Y) (DIFFERENCE X Z)) (DIFFERENCE X (UNION Y Z)))))) [SGC for 5237 CONS pages..(13492 writable)..(T=3).GC finished] Summary Form: ( DEFTHM DIFFERENCE-OVER-UNION ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DIFFERENCE-IN) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE INTERSECT-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.21 seconds (prove: 0.21, print: 0.00, other: 0.00) DIFFERENCE-OVER-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: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (DIFFERENCE X (INTERSECT Y Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (UNION (DIFFERENCE X Y) (DIFFERENCE X Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (UNION (DIFFERENCE X Y) (DIFFERENCE X Z))))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X (INTERSECT Y Z)) (UNION (DIFFERENCE X Y) (DIFFERENCE X Z)))))) 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 (DIFFERENCE X Y) (DIFFERENCE X Z)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X (INTERSECT Y Z))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X (INTERSECT Y Z))))))) :EXPAND ((SUBSET-TRIGGER (UNION (DIFFERENCE X Y) (DIFFERENCE X Z)) (DIFFERENCE X (INTERSECT Y Z)))))) Summary Form: ( DEFTHM DIFFERENCE-OVER-INTERSECT ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DIFFERENCE-IN) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE INTERSECT-IN) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE UNION-IN) (:REWRITE UNION-SET) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.23 seconds (prove: 0.23, print: 0.00, other: 0.00) DIFFERENCE-OVER-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: ("Subgoal 2.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A Y))) (ALL-SET (LAMBDA NIL (DIFFERENCE (INSERT A X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X Y)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE (INSERT A X) Y) (DIFFERENCE X 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 2.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A Y))) (ALL-SET (LAMBDA NIL (DIFFERENCE X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE (INSERT A X) Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE (INSERT A X) Y)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X Y) (DIFFERENCE (INSERT A X) 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A Y)))) (ALL-SET (LAMBDA NIL (DIFFERENCE (INSERT A X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT A (DIFFERENCE X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT A (DIFFERENCE X Y))))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE (INSERT A X) Y) (INSERT A (DIFFERENCE X 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A Y)))) (ALL-SET (LAMBDA NIL (DIFFERENCE X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE (INSERT A X) Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE (INSERT A X) Y)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X Y) (DIFFERENCE (INSERT A X) Y))))) Summary Form: ( DEFTHM DIFFERENCE-INSERT-X ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DIFFERENCE-IN) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SUBSET-INSERT-X) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.20 seconds (prove: 0.20, print: 0.00, other: 0.00) DIFFERENCE-INSERT-X We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Subgoal 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (DIFFERENCE X (INSERT A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (DIFFERENCE X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (DIFFERENCE X Y))))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X (INSERT A Y)) (DELETE A (DIFFERENCE X 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 (DELETE A (DIFFERENCE X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X (INSERT A Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X (INSERT A Y))))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (DIFFERENCE X Y)) (DIFFERENCE X (INSERT A Y)))))) Summary Form: ( DEFTHM DIFFERENCE-INSERT-Y ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DIFFERENCE-IN) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE IN-INSERT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.12 seconds (prove: 0.12, print: 0.00, other: 0.00) DIFFERENCE-INSERT-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 2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL T)) (ALL-SET (LAMBDA NIL (DIFFERENCE (DELETE A X) Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A (DIFFERENCE X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A (DIFFERENCE X Y))))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE (DELETE A X) Y) (DELETE A (DIFFERENCE X 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 (DELETE A (DIFFERENCE X Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE (DELETE A X) Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE (DELETE A X) Y)))))) :EXPAND ((SUBSET-TRIGGER (DELETE A (DIFFERENCE X Y)) (DIFFERENCE (DELETE A X) Y))))) Summary Form: ( DEFTHM DIFFERENCE-DELETE-X ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE DELETE-SET) (:REWRITE DIFFERENCE-IN) (:REWRITE DIFFERENCE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.08 seconds (prove: 0.07, print: 0.00, other: 0.01) DIFFERENCE-DELETE-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 2.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A X))) (ALL-SET (LAMBDA NIL (DIFFERENCE X (DELETE A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (INSERT A (DIFFERENCE X Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (INSERT A (DIFFERENCE X Y))))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X (DELETE A Y)) (INSERT A (DIFFERENCE X 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 2.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (IN A X))) (ALL-SET (LAMBDA NIL (DIFFERENCE X Y))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X (DELETE A Y))))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X (DELETE A Y))))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X Y) (DIFFERENCE X (DELETE A 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.2'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A X)))) (ALL-SET (LAMBDA NIL (DIFFERENCE X (DELETE A Y)))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE X Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE X Y)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X (DELETE A Y)) (DIFFERENCE X Y))))) [SGC for 5237 CONS pages..(13492 writable)..(T=3).GC finished] 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.1'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (NOT (IN A X)))) (ALL-SET (LAMBDA NIL (DIFFERENCE X Y))