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))) (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)))))) Summary Form: ( DEFTHM DIFFERENCE-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 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.19 seconds (prove: 0.18, print: 0.00, other: 0.01) DIFFERENCE-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 (SUBSET X Y))) (ALL-SET (LAMBDA NIL (DIFFERENCE X Z))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DIFFERENCE Y Z)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DIFFERENCE Y Z)))))) :EXPAND ((SUBSET-TRIGGER (DIFFERENCE X Z) (DIFFERENCE Y Z))))) Summary Form: ( DEFTHM DIFFERENCE-PRESERVES-SUBSET ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DIFFERENCE-IN) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SUBSET-IN) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.03 seconds (prove: 0.03, print: 0.00, other: 0.00) DIFFERENCE-PRESERVES-SUBSET Summary Form: ( DEFUN CARDINALITY ...) Rules: ((:BUILT-IN-CLAUSE TAIL-COUNT-BUILT-IN) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) CARDINALITY Summary Form: ( VERIFY-GUARDS CARDINALITY ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION EMPTY) (:DEFINITION LEN) (:DEFINITION LENGTH) (:DEFINITION NOT) (:DEFINITION SETP) (:DEFINITION TAIL) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CARDINALITY) (:EXECUTABLE-COUNTERPART EMPTY) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART LENGTH) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION SETP) (:INDUCTION TRUE-LISTP) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SETS-ARE-TRUE-LISTS) (:REWRITE SFIX-SET-IDENTITY) (:TYPE-PRESCRIPTION <<-TYPE) (:TYPE-PRESCRIPTION SETP-TYPE) (:TYPE-PRESCRIPTION TRUE-LISTP)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) CARDINALITY Summary Form: ( DEFTHM CARDINALITY-TYPE ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION CARDINALITY)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) CARDINALITY-TYPE Summary Form: ( DEFTHM CARDINALITY-ZERO-EMPTY ...) Rules: ((:DEFINITION CARDINALITY) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION CARDINALITY) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) CARDINALITY-ZERO-EMPTY Summary Form: ( DEFTHM CARDINALITY-SFIX-CANCEL ...) Rules: ((:DEFINITION CARDINALITY) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION CARDINALITY) (: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) CARDINALITY-SFIX-CANCEL Summary Form: ( DEFTHM CARDINALITY-INSERT-EMPTY ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE TAIL-INSERT-EMPTY) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) CARDINALITY-INSERT-EMPTY Summary Form: ( DEFTHM INSERT-CARDINALITY ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION IN) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING SUBSET-TAIL) (:INDUCTION CARDINALITY) (:INDUCTION IN) (:INDUCTION USE-WEAK-INSERT-INDUCTION) (:INDUCTION WEAK-INSERT-INDUCTION) (:REWRITE CARDINALITY-INSERT-EMPTY) (:REWRITE INSERT-IDENTITY) (:REWRITE INSERT-NEVER-EMPTY) (:REWRITE NEVER-IN-EMPTY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE SFIX-SET-IDENTITY) (:REWRITE SUBSET-IN) (:REWRITE WEAK-INSERT-INDUCTION-HELPER-2) (:REWRITE WEAK-INSERT-INDUCTION-HELPER-3) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) INSERT-CARDINALITY Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) T Summary Form: ( DEFTHM DELETE-CARDINALITY ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION DELETE) (:DEFINITION IN) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION CARDINALITY) (:INDUCTION DELETE) (:INDUCTION IN) (:REWRITE CARDINALITY-SFIX-CANCEL) (:REWRITE DELETE-IN) (:REWRITE DELETE-NONMEMBER-CANCEL) (:REWRITE HEAD-UNIQUE) (:REWRITE IN-HEAD) (:REWRITE IN-TAIL-OR-HEAD) (:REWRITE INSERT-CARDINALITY) (:REWRITE NEVER-IN-EMPTY) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DELETE-CARDINALITY Summary Form: ( DEFUN DOUBLE-DELETE-INDUCTION ...) Rules: ((:DEFINITION DELETE) (:DEFINITION O-FINP) (:DEFINITION O<) (:EXECUTABLE-COUNTERPART IF) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:LINEAR TAIL-COUNT) (:REWRITE DELETE-SET) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION EMPTY-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) DOUBLE-DELETE-INDUCTION We suspect this conjecture sould be proven by functional instantiation of ALL-BY-MEMBERSHIP. This suspicion is caused by PICK-A-POINT-SUBSET- STRATEGY, so if this is not what you want to do, then you should disable PICK-A-POINT-SUBSET-STRATEGY. Accordingly, we suggest the following hint: ("Goal'" (:USE ((:FUNCTIONAL-INSTANCE ALL-BY-MEMBERSHIP (ALL-HYPS (LAMBDA NIL (SUBSET X Y))) (ALL-SET (LAMBDA NIL (DELETE A X))) (ALL (LAMBDA (COMPUTED-HINTS::?X) (SUBSET COMPUTED-HINTS::?X (DELETE A Y)))) (PREDICATE (LAMBDA (COMPUTED-HINTS::?X) (IN COMPUTED-HINTS::?X (DELETE A Y)))))) :EXPAND ((SUBSET-TRIGGER (DELETE A X) (DELETE A Y))))) Summary Form: ( DEFTHM SUBSET-DOUBLE-DELETE ...) Rules: ((:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SUBSET-TRIGGER) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-IN) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SUBSET-IN) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) (:DEFTHMD SUBSET-DOUBLE-DELETE) Summary Form: ( DEFTHM SUBSET-CARDINALITY-LEMMA ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION DELETE) (:DEFINITION NOT) (:DEFINITION SUBSET) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DELETE-CARDINALITY) (:REWRITE IN-HEAD) (:REWRITE SUBSET-DELETE) (:REWRITE SUBSET-IN) (:REWRITE SUBSET-REFLEXIVE) (:REWRITE SUBSET-TRANSITIVE) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) SUBSET-CARDINALITY-LEMMA Summary Form: ( DEFTHM SUBSET-CARDINALITY ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION DELETE) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DOUBLE-DELETE-INDUCTION) (:REWRITE DELETE-CARDINALITY) (:REWRITE EMPTY-SUBSET) (:REWRITE EMPTY-SUBSET-2) (:REWRITE IN-HEAD) (:REWRITE SUBSET-CARDINALITY-LEMMA) (:REWRITE SUBSET-IN) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) SUBSET-CARDINALITY Summary Form: ( ENCAPSULATE NIL (LOCAL ...) ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00) T Summary Form: ( DEFTHM EQUAL-CARDINALITY-SUBSET-IS-EQUALITY ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION DELETE) (:DEFINITION IN) (:DEFINITION NOT) (:DEFINITION SUBSET) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DOUBLE-DELETE-INDUCTION) (:REWRITE CARDINALITY-ZERO-EMPTY) (:REWRITE DELETE-CARDINALITY) (:REWRITE DELETE-SET) (:REWRITE DOUBLE-CONTAINMENT) (:REWRITE EMPTY-SUBSET) (:REWRITE EMPTY-SUBSET-2) (:REWRITE HEAD-UNIQUE) (:REWRITE IN-HEAD) (:REWRITE IN-SET) (:REWRITE INSERT-DELETE-CANCEL) (:REWRITE INSERT-HEAD-TAIL) (:REWRITE INSERT-IDENTITY) (:REWRITE NONEMPTY-MEANS-SET) (:REWRITE PICK-A-POINT-SUBSET-STRATEGY) (:REWRITE SUBSET-DELETE) (:REWRITE SUBSET-IN) (:REWRITE SUBSET-MEMBERSHIP-TAIL-2) (:REWRITE SUBSET-REFLEXIVE) (:REWRITE SUBSET-TRANSITIVE) (:REWRITE TAIL-PRODUCES-SET) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE) (:TYPE-PRESCRIPTION SETP-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.06 seconds (prove: 0.06, print: 0.00, other: 0.00) [SGC for 25 FIXNUM pages..(13495 writable)..(T=3).GC finished] (:DEFTHMD EQUAL-CARDINALITY-SUBSET-IS-EQUALITY) Summary Form: ( DEFTHM INTERSECT-CARDINALITY-X ...) Rules: ((:REWRITE INTERSECT-SUBSET-X) (:REWRITE SUBSET-CARDINALITY)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) INTERSECT-CARDINALITY-X Summary Form: ( DEFTHM INTERSECT-CARDINALITY-Y ...) Rules: ((:REWRITE INTERSECT-SUBSET-Y) (:REWRITE SUBSET-CARDINALITY)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) INTERSECT-CARDINALITY-Y Summary Form: ( DEFTHM EXPAND-CARDINALITY-OF-UNION ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION FIX) (:DEFINITION INTERSECT) (:DEFINITION UNION) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION CARDINALITY) (:INDUCTION INTERSECT) (:INDUCTION UNION) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE CARDINALITY-SFIX-CANCEL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE HEAD-UNIQUE) (:REWRITE INSERT-CARDINALITY) (:REWRITE INSERT-IDENTITY) (:REWRITE INTERSECT-IN) (:REWRITE UNICITY-OF-0) (:REWRITE UNION-EMPTY-X) (:REWRITE UNION-IN) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.03 seconds (prove: 0.03, print: 0.00, other: 0.00) EXPAND-CARDINALITY-OF-UNION Summary Form: ( DEFTHM EXPAND-CARDINALITY-OF-DIFFERENCE ...) Rules: ((:DEFINITION CARDINALITY) (:DEFINITION DIFFERENCE) (:DEFINITION INTERSECT) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART UNARY--) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION CARDINALITY) (:INDUCTION DIFFERENCE) (:INDUCTION INTERSECT) (:LINEAR EXPAND-CARDINALITY-OF-UNION) (:REWRITE ASSOCIATIVITY-OF-+) (:REWRITE CARDINALITY-SFIX-CANCEL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE DIFFERENCE-EMPTY-X) (:REWRITE DIFFERENCE-IN) (:REWRITE HEAD-UNIQUE) (:REWRITE INSERT-CARDINALITY) (:REWRITE INTERSECT-IN) (:REWRITE UNION-SYMMETRIC) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION EMPTY-TYPE) (:TYPE-PRESCRIPTION IN-TYPE)) Warnings: None Time: 0.19 seconds (prove: 0.19, print: 0.00, other: 0.00) EXPAND-CARDINALITY-OF-DIFFERENCE Summary Form: ( DEFTHM INTERSECT-CARDINALITY-SUBSET ...) Rules: ((:DEFINITION CARDINALITY) (:FAKE-RUNE-FOR-LINEAR NIL) (:LINEAR EXPAND-CARDINALITY-OF-DIFFERENCE) (:REWRITE SUBSET-DIFFERENCE) (:REWRITE SUBSET-REFLEXIVE) (:REWRITE SUBSET-TRANSITIVE) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) INTERSECT-CARDINALITY-SUBSET Summary Form: ( DEFTHM INTERSECT-CARDINALITY-NON-SUBSET ...) Rules: ((:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:LINEAR EXPAND-CARDINALITY-OF-DIFFERENCE) (:LINEAR INTERSECT-CARDINALITY-X) (:REWRITE CARDINALITY-ZERO-EMPTY) (:REWRITE SUBSET-DIFFERENCE) (:TYPE-PRESCRIPTION CARDINALITY-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) INTERSECT-CARDINALITY-NON-SUBSET Summary Form: ( DEFTHM INTERSECT-CARDINALITY-SUBSET-2 ...) Rules: ((:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:LINEAR INTERSECT-CARDINALITY-NON-SUBSET) (:REWRITE INTERSECT-CARDINALITY-SUBSET) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) INTERSECT-CARDINALITY-SUBSET-2 Summary Form: ( DEFTHM INTERSECT-CARDINALITY-NON-SUBSET-2 ...) Rules: ((:DEFINITION NOT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:LINEAR INTERSECT-CARDINALITY-NON-SUBSET) (:REWRITE INTERSECT-CARDINALITY-SUBSET) (:REWRITE SUBSET-CARDINALITY) (:REWRITE SUBSET-REFLEXIVE) (:TYPE-PRESCRIPTION CARDINALITY-TYPE) (:TYPE-PRESCRIPTION SUBSET-TYPE)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) INTERSECT-CARDINALITY-NON-SUBSET-2 Summary Form: ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2::ACL2-DEFAULTS-TABLE Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o start address -T 0x93f4a70 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.o Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o start address -T 0x9e16000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o start address -T 0x9e18160 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o start address -T 0x9945000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.o Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o start address -T 0x94582c0 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.o Summary Form: ( INCLUDE-BOOK "outer" ...) Rules: NIL Warnings: None Time: 0.37 seconds (prove: 0.00, print: 0.00, other: 0.37) Compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.lisp. End of Pass 1. ;; Note: Tail-recursive call of DOUBLE-DELETE-INDUCTION was replaced by iteration. End of Pass 2. OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3 Finished compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o. "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o" Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o start address -T 0x9688880 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.o Summary Form: (CERTIFY-BOOK "outer" ...) Rules: NIL Warnings: None Time: 0.66 seconds (prove: 0.26, print: 0.00, other: 0.40) "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/outer.lisp" ACL2 !> Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ACL2>