sundance:/projects/acl2/devel/books/misc> cd sundance:~> cd /u/www/users/moore/acl2/seminar/ sundance:/u/www/users/moore/acl2/seminar> cd 2006.02.15-kaufmann/ sundance:/u/www/users/moore/acl2/seminar/2006.02.15-kaufmann> acl2 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.4 built January 30, 2006 23:10:57. Copyright (C) 2006 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*). See the documentation topic note-2-9-4 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.4. Level 1. Cbd "/v/filer2/moore/public_html/acl2/seminar/2006.02.15-kaufmann/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defpkg "HANOI" (set-difference-equal (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*) '(PUSH POP GET))) Summary Form: ( DEFPKG "HANOI" ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) "HANOI" ACL2 !>:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(defpkg "HANOI" (set-difference-equal (union-eq *acl2-exports* *common-lisp-symbols-from-main-lisp-package*) '(PUSH POP GET))) [SGC for 21 STRING pages..(8313 writable)..(T=2).GC finished] Summary Form: ( DEFPKG "HANOI" ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) "HANOI" ACL2 !>(rebuild "/projects/acl2/devel/books/misc/hanoi.lisp" t) ACL2 loading "/projects/acl2/devel/books/misc/hanoi.lisp". "HANOI" MEM APP DEL PERM PERM-OPENER APP-ASSOC APP-RIGHT-ID GET PUT [SGC for 20 CFUN pages..(8324 writable)..(T=1).GC finished] GET-PUT PUT-GET PUT-PUT-1 PUT-PUT-2 TRUE-LISTP-PUT LEN-PUT PUSH POP TOP H HANOI [SGC for 20 CFUN pages..(8329 writable)..(T=1).GC finished] A B LEGAL-SYNTAXP LEGAL-MOVEP DO-MOVE PLAY TOWER ACL2 Warning [Non-rec] in ( DEFTHM EXAMPLES ...): A :REWRITE rule generated from EXAMPLES will be triggered only by terms containing the non-recursive function symbol HANOI. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Non-rec] in ( DEFTHM EXAMPLES ...): A :REWRITE rule generated from EXAMPLES will be triggered only by terms containing the non-recursive function symbol HANOI. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Non-rec] in ( DEFTHM EXAMPLES ...): A :REWRITE rule generated from EXAMPLES will be triggered only by terms containing the non-recursive function symbol HANOI. Unless this function is disabled, this rule is unlikely ever to be used. EXAMPLES TRUE-LISTP-TOWER PLAY-APP BIG-TOPS [SGC for 21 STRING pages..(8330 writable)..(T=0).GC finished] INDUCTION-HINT H-LEMMA ACL2 Warning [Non-rec] in ( DEFTHM HANOI-CORRECT ...): A :REWRITE rule generated from HANOI-CORRECT will be triggered only by terms containing the non-recursive function symbol HANOI. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM HANOI-CORRECT ...): A newly proposed :REWRITE rule generated from HANOI-CORRECT probably subsumes the previously added :REWRITE rule EXAMPLES, in the sense that the new rule will now probably be applied whenever the old rule would have been. HANOI-CORRECT Finished loading "/projects/acl2/devel/books/misc/hanoi.lisp". T ACL2 !>"HANOI" "HANOI" HANOI !>:ubt! h-lemma L 33:x(DEFUN INDUCTION-HINT (A B C N S) ...) HANOI !>:start-proof-tree Proof tree output is now enabled. Note that :START-PROOF-TREE works by removing 'proof-tree from the inhibit-output-lst; see :DOC set- inhibit-output-lst. HANOI !>(defmacro proof-term () '(implies (and (natp n) (true-listp s) (equal (len s) 3) (perm (list a b c) '(0 1 2)) (big-tops a b c n s)) (equal (play (h a b c n) (put (app (tower n) (get a s)) a s)) (put (app (tower n) (get c s)) c s)))) Summary Form: ( DEFMACRO PROOF-TERM ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.00) PROOF-TERM HANOI !>(defmacro do-proof () `(defthm h-lemma (proof-term) :rule-classes nil :hints (("Goal" :induct (induction-hint a b c n s))))) Summary Form: ( DEFMACRO DO-PROOF ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.00) DO-PROOF HANOI !>(do-proof) << Starting proof tree logging >> [Note: A hint was supplied for our processing of the goal above. Thanks!] Name the formula above *1. We have been told to use induction. One induction scheme is suggested by the induction hint. We will induct according to a scheme suggested by (INDUCTION-HINT A B C N S). This suggestion was produced using the :induction rule INDUCTION-HINT. If we let (:P A B C N S) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP N)) (:P A C B (+ -1 N) (PUT (PUSH N (GET A S)) A S)) (:P B A C (+ -1 N) (PUT (PUSH N (GET C S)) C S))) (:P A B C N S)) (IMPLIES (ZP N) (:P A B C N S))). This induction is justified by the same argument used to admit INDUCTION- HINT, namely, the measure (ACL2-COUNT N) is decreasing according to the relation O< (which is known to be well-founded on the domain recognized by O-P). Note, however, that the unmeasured variables C, A, B and S are being instantiated. When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ZP N)) (IMPLIES (AND (NATP (+ -1 N)) (TRUE-LISTP (PUT (PUSH N (GET A S)) A S)) (EQUAL (LEN (PUT (PUSH N (GET A S)) A S)) 3) (PERM (LIST A C B) '(0 1 2)) (BIG-TOPS A C B (+ -1 N) (PUT (PUSH N (GET A S)) A S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET A (PUT (PUSH N (GET A S)) A S))) A (PUT (PUSH N (GET A S)) A S))) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (PUSH N (GET A S)) A S))) B (PUT (PUSH N (GET A S)) A S)))) (IMPLIES (AND (NATP (+ -1 N)) (TRUE-LISTP (PUT (PUSH N (GET C S)) C S)) (EQUAL (LEN (PUT (PUSH N (GET C S)) C S)) 3) (PERM (LIST B A C) '(0 1 2)) (BIG-TOPS B A C (+ -1 N) (PUT (PUSH N (GET C S)) C S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (PUSH N (GET C S)) C S))) B (PUT (PUSH N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (PUSH N (GET C S)) C S))) C (PUT (PUSH N (GET C S)) C S))))) (IMPLIES (AND (NATP N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (PERM (LIST A B C) '(0 1 2)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S)))). By the simple :definitions NATP and PUSH and the simple :rewrite rules PERM-OPENER and PUT-PUT-2 we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (IMPLIES (AND (NATP (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET A S)) A S)) (EQUAL (LEN (PUT (CONS N (GET A S)) A S)) 3) (PERM (LIST A C B) '(0 1 2)) (BIG-TOPS A C B (+ -1 N) (PUT (CONS N (GET A S)) A S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET A (PUT (CONS N (GET A S)) A S))) A S)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET A S)) A S))) B (PUT (CONS N (GET A S)) A S)))) (IMPLIES (AND (NATP (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET C S)) C S)) (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3) (PERM (LIST B A C) '(0 1 2)) (BIG-TOPS B A C (+ -1 N) (PUT (CONS N (GET C S)) C S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). [SGC for 442 CONS pages..(8347 writable)..(T=0).GC finished] [SGC for 442 CONS pages..(8347 writable)..(T=0).GC finished] [SGC for 442 CONS pages..(8347 writable)..(T=1).GC finished] [SGC for 25 FIXNUM pages..(10387 writable)..(T=2).GC finished] This simplifies, using the :compound-recognizer rules ACL2::NATP-COMPOUND- RECOGNIZER and ACL2::ZP-COMPOUND-RECOGNIZER, the :definitions A, APP, B, BIG-TOPS, DO-MOVE, GET, H, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH, TOP and TOWER, the :executable-counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules APP-ASSOC, CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PERM-OPENER, PLAY-APP, PUT-PUT- 1 and TRUE-LISTP-PUT, to the following 109 conjectures. (By the way, the case limit affected this analysis. See :DOC case-split-limitations.) Subgoal *1/2.109 (IMPLIES (AND (NOT (ZP N)) (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (NATP (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET C S)) C S)) (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3) (PERM (LIST B A C) '(0 1 2)) (IMPLIES (BIG-TOPS B A C (+ -1 N) (PUT (CONS N (GET C S)) C S)) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). By the simple :definition NATP and the simple :rewrite rule PERM-OPENER we reduce the conjecture to Subgoal *1/2.109' (IMPLIES (AND (NOT (ZP N)) (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (INTEGERP (+ -1 N)) (<= 0 (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET C S)) C S)) (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (IMPLIES (BIG-TOPS B A C (+ -1 N) (PUT (CONS N (GET C S)) C S)) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). [SGC for 25 FIXNUM pages..(10387 writable)..(T=1).GC finished] This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions BIG-TOPS, H and TOWER, the :executable- counterpart of EQUAL, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, GET-PUT, LEN-PUT and TRUE-LISTP-PUT, to the following 16 conjectures. Subgoal *1/2.109.16 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (NOT (CONSP (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.15 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.15' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.14 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.13 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.13' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.12 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (NOT (CONSP (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.11 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.11' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions A, APP, B, DO-MOVE, GET, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH and TOP, the :executable- counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PUT-GET, PUT-PUT-1 and PUT-PUT-2, to the following four conjectures. Subgoal *1/2.109.11.4 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (NOT (EQUAL A 0)) (NOT (EQUAL A 1)) (NOT (EQUAL A 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.11.3 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 0 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 0 S))) 0 S)) (PUT (CONS N (GET 0 S)) 0 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 0)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 0 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 0 S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 0) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.11.2 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 2 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 2 S))) 2 S)) (PUT (CONS N (GET 2 S)) 2 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 2)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 2 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 2 S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 2) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.11.1 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 1 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 1 S))) 1 S)) (PUT (CONS N (GET 1 S)) 1 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 1)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 1 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 1 S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 1) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.10 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.9 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.9' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions A, APP, B, DO-MOVE, GET, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH and TOP, the :executable- counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PUT-GET, PUT-PUT-1 and PUT-PUT-2, to the following four conjectures. Subgoal *1/2.109.9.4 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N)) (NOT (EQUAL A 0)) (NOT (EQUAL A 1)) (NOT (EQUAL A 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.9.3 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 0 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 0 S))) 0 S)) (PUT (CONS N (GET 0 S)) 0 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 0)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 0 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 0 S))) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 0) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.9.2 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 2 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 2 S))) 2 S)) (PUT (CONS N (GET 2 S)) 2 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 2)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 2 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 2 S))) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 2) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.9.1 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 1 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 1 S))) 1 S)) (PUT (CONS N (GET 1 S)) 1 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 1)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 1 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 1 S))) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 1) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.8 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (NOT (CONSP (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.7 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.7' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions A, APP, B, DO-MOVE, GET, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH and TOP, the :executable- counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PUT-GET, PUT-PUT-1 and PUT-PUT-2, to the following four conjectures. Subgoal *1/2.109.7.4 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (NOT (EQUAL A 0)) (NOT (EQUAL A 1)) (NOT (EQUAL A 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.7.3 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 0 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 0 S))) 0 S)) (PUT (CONS N (GET 0 S)) 0 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 0)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 0 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET 0 S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 0) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.7.2 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 2 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 2 S))) 2 S)) (PUT (CONS N (GET 2 S)) 2 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 2)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 2 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET 2 S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 2) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.7.1 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 1 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 1 S))) 1 S)) (PUT (CONS N (GET 1 S)) 1 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 1)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 1 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET 1 S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 1) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.6 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.5 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.5' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions A, APP, B, DO-MOVE, GET, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH and TOP, the :executable- counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PUT-GET, PUT-PUT-1 and PUT-PUT-2, to the following four conjectures. Subgoal *1/2.109.5.4 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET C S))) (NOT (ZP N)) (NOT (EQUAL A 0)) (NOT (EQUAL A 1)) (NOT (EQUAL A 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.5.3 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 0 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 0 S))) 0 S)) (PUT (CONS N (GET 0 S)) 0 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 0)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 0 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET 0 S))) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 0) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.5.2 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 2 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 2 S))) 2 S)) (PUT (CONS N (GET 2 S)) 2 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 2)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 2 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET 2 S))) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 2) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.5.1 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 1 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 1 S))) 1 S)) (PUT (CONS N (GET 1 S)) 1 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 1)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 1 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET 1 S))) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 1) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.4 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.3 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.3' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions A, APP, B, DO-MOVE, GET, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH and TOP, the :executable- counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PUT-GET, PUT-PUT-1 and PUT-PUT-2, to the following four conjectures. Subgoal *1/2.109.3.4 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET C S))) (NOT (ZP N)) (NOT (EQUAL A 0)) (NOT (EQUAL A 1)) (NOT (EQUAL A 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.3.3 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 0 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 0 S))) 0 S)) (PUT (CONS N (GET 0 S)) 0 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 0)) (NOT (EQUAL B C)) (NOT (CONSP (GET 0 S))) (EQUAL (PLAY (H B 0 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 0) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.3.2 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 2 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 2 S))) 2 S)) (PUT (CONS N (GET 2 S)) 2 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 2)) (NOT (EQUAL B C)) (NOT (CONSP (GET 2 S))) (EQUAL (PLAY (H B 2 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 2) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.3.1 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 1 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 1 S))) 1 S)) (PUT (CONS N (GET 1 S)) 1 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 1)) (NOT (EQUAL B C)) (NOT (CONSP (GET 1 S))) (EQUAL (PLAY (H B 1 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 1) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.2 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.109.1 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.109.1' (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions A, APP, B, DO-MOVE, GET, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH and TOP, the :executable- counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PUT-GET, PUT-PUT-1 and PUT-PUT-2, to the following four conjectures. Subgoal *1/2.109.1.4 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (NOT (CONSP (GET A S))) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET C S))) (NOT (ZP N)) (NOT (EQUAL A 0)) (NOT (EQUAL A 1)) (NOT (EQUAL A 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.1.3 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 0 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 0 S))) 0 S)) (PUT (CONS N (GET 0 S)) 0 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 0)) (NOT (EQUAL B C)) (NOT (CONSP (GET 0 S))) (EQUAL (PLAY (H B 0 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 0) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.1.2 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 2 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 2 S))) 2 S)) (PUT (CONS N (GET 2 S)) 2 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 2)) (NOT (EQUAL B C)) (NOT (CONSP (GET 2 S))) (EQUAL (PLAY (H B 2 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 2) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.109.1.1 (IMPLIES (AND (NOT (CONSP (GET B S))) (EQUAL (PLAY (H 1 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 1 S))) 1 S)) (PUT (CONS N (GET 1 S)) 1 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 1)) (NOT (EQUAL B C)) (NOT (CONSP (GET 1 S))) (EQUAL (PLAY (H B 1 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET C S))) (NOT (ZP N)) (EQUAL A 1) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.108 (IMPLIES (AND (NOT (ZP N)) (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (NOT (PERM (LIST B A C) '(0 1 2))) (IMPLIES NIL (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). But simplification reduces this to T, using the :executable-counterpart of NOT, primitive type reasoning and the :rewrite rule PERM-OPENER. Subgoal *1/2.107 (IMPLIES (AND (NOT (ZP N)) (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (NOT (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3)) (IMPLIES NIL (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). But simplification reduces this to T, using the :executable-counterpart of EQUAL, linear arithmetic and the :rewrite rule LEN-PUT. Subgoal *1/2.106 (IMPLIES (AND (NOT (ZP N)) (NOT (CONSP (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (NOT (TRUE-LISTP (PUT (CONS N (GET C S)) C S))) (IMPLIES NIL (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). But simplification reduces this to T, using linear arithmetic and the :rewrite rule TRUE-LISTP-PUT. Subgoal *1/2.105 (IMPLIES (AND (NOT (ZP N)) (CONSP (GET B S)) (<= (CAR (GET B S)) (+ -1 N)) (NATP (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET C S)) C S)) (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3) (PERM (LIST B A C) '(0 1 2)) (IMPLIES (BIG-TOPS B A C (+ -1 N) (PUT (CONS N (GET C S)) C S)) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). By the simple :definition NATP and the simple :rewrite rule PERM-OPENER we reduce the conjecture to Subgoal *1/2.105' (IMPLIES (AND (NOT (ZP N)) (CONSP (GET B S)) (<= (CAR (GET B S)) (+ -1 N)) (INTEGERP (+ -1 N)) (<= 0 (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET C S)) C S)) (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (IMPLIES (BIG-TOPS B A C (+ -1 N) (PUT (CONS N (GET C S)) C S)) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). [SGC for 3151 CONS pages..(11169 writable)..(T=2).GC finished] But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER, the :definition BIG-TOPS, the :executable- counterpart of EQUAL, linear arithmetic, primitive type reasoning and the :rewrite rules GET-PUT, LEN-PUT and TRUE-LISTP-PUT. Subgoal *1/2.104 (IMPLIES (AND (NOT (ZP N)) (CONSP (GET B S)) (<= (CAR (GET B S)) (+ -1 N)) (NOT (PERM (LIST B A C) '(0 1 2))) (IMPLIES NIL (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). But simplification reduces this to T, using the :executable-counterpart of NOT, primitive type reasoning and the :rewrite rule PERM-OPENER. Subgoal *1/2.103 (IMPLIES (AND (NOT (ZP N)) (CONSP (GET B S)) (<= (CAR (GET B S)) (+ -1 N)) (NOT (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3)) (IMPLIES NIL (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). But simplification reduces this to T, using the :executable-counterpart of EQUAL, linear arithmetic and the :rewrite rule LEN-PUT. Subgoal *1/2.102 (IMPLIES (AND (NOT (ZP N)) (CONSP (GET B S)) (<= (CAR (GET B S)) (+ -1 N)) (NOT (TRUE-LISTP (PUT (CONS N (GET C S)) C S))) (IMPLIES NIL (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). But simplification reduces this to T, using linear arithmetic and the :rewrite rule TRUE-LISTP-PUT. Subgoal *1/2.101 (IMPLIES (AND (NOT (ZP N)) (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (NATP (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET C S)) C S)) (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3) (PERM (LIST B A C) '(0 1 2)) (IMPLIES (BIG-TOPS B A C (+ -1 N) (PUT (CONS N (GET C S)) C S)) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL A B)) (NOT (EQUAL A C)) (NOT (EQUAL B C)) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). By the simple :definition NATP and the simple :rewrite rule PERM-OPENER we reduce the conjecture to Subgoal *1/2.101' (IMPLIES (AND (NOT (ZP N)) (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (INTEGERP (+ -1 N)) (<= 0 (+ -1 N)) (TRUE-LISTP (PUT (CONS N (GET C S)) C S)) (EQUAL (LEN (PUT (CONS N (GET C S)) C S)) 3) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (IMPLIES (BIG-TOPS B A C (+ -1 N) (PUT (CONS N (GET C S)) C S)) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B (PUT (CONS N (GET C S)) C S))) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (GET C (PUT (CONS N (GET C S)) C S))) C S))) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (BIG-TOPS A B C N S)) (EQUAL (PLAY (H A B C N) (PUT (APP (TOWER N) (GET A S)) A S)) (PUT (APP (TOWER N) (GET C S)) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions BIG-TOPS, H and TOWER, the :executable- counterpart of EQUAL, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, GET-PUT, LEN-PUT and TRUE-LISTP-PUT, to the following 16 conjectures. Subgoal *1/2.101.16 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.101.15 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.101.15' (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.101.14 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET B S))) (< N (CAR (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.101.13 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET B S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.101.13' (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (CONSP (GET A S)) (<= (CAR (GET A S)) (+ -1 N)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (< N (CAR (GET A S))) (< N (CAR (GET B S))) (< N (CAR (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.101.12 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (ZP N)) (EQUAL (PLAY NIL (PUT (APP NIL (GET A S)) A S)) (PUT (APP NIL (GET C S)) C S))). But simplification reduces this to T, using the :compound-recognizer rule ACL2::ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2.101.11 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (APP (H A C B (+ -1 N)) (CONS (LIST 'MOVE A C) (H B A C (+ -1 N)))) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET A S)) A S)) (PUT (APP (APP (TOWER (+ -1 N)) (LIST N)) (GET C S)) C S))). By the simple :rewrite rules APP-ASSOC and PLAY-APP we reduce the conjecture to Subgoal *1/2.101.11' (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (INTEGERP N) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N))) (EQUAL (PLAY (CONS (LIST 'MOVE A C) (H B A C (+ -1 N))) (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET A S))) A S))) (PUT (APP (TOWER (+ -1 N)) (APP (LIST N) (GET C S))) C S))). This simplifies, using the :compound-recognizer rule ACL2::ZP-COMPOUND- RECOGNIZER, the :definitions A, APP, B, DO-MOVE, GET, LEGAL-MOVEP, LEGAL-SYNTAXP, LEN, MEM, PLAY, POP, PUSH and TOP, the :executable- counterparts of <, BINARY-+, CAR, CDR, CONSP, EQUAL, INTEGERP, LEN, NOT and ZP, linear arithmetic, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS, GET-PUT, LEN-PUT, PUT-GET, PUT-PUT-1 and PUT-PUT-2, to the following four conjectures. Subgoal *1/2.101.11.4 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET A S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (NOT (EQUAL A 0)) (NOT (EQUAL A 1)) (NOT (EQUAL A 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.101.11.3 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H 0 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 0 S))) 0 S)) (PUT (CONS N (GET 0 S)) 0 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 0)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 0 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 0 S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 0) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.101.11.2 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H 2 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 2 S))) 2 S)) (PUT (CONS N (GET 2 S)) 2 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 2)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 2 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 2 S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 2) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.101.11.1 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H 1 C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET 1 S))) 1 S)) (PUT (CONS N (GET 1 S)) 1 (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B 1)) (NOT (EQUAL B C)) (< (+ -1 N) N) (EQUAL (PLAY (H B 1 C (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (GET B S)) B (PUT (CONS N (GET C S)) C S))) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S)) (<= 0 N) (TRUE-LISTP S) (EQUAL (LEN S) 3) (NOT (CONSP (GET 1 S))) (< N (CAR (GET B S))) (NOT (CONSP (GET C S))) (NOT (ZP N)) (EQUAL A 1) (NOT (EQUAL C 0)) (NOT (EQUAL C 1)) (NOT (EQUAL C 2))) (EQUAL NIL (PUT (APP (TOWER (+ -1 N)) (CONS N (GET C S))) C S))). But simplification reduces this to T, using linear arithmetic. Subgoal *1/2.101.10 (IMPLIES (AND (< (+ -1 N) (CAR (GET B S))) (EQUAL (PLAY (H A C B (+ -1 N)) (PUT (APP (TOWER (+ -1 N)) (CONS N (GET A S))) A S)) (PUT (CONS N (GET A S)) A (PUT (APP (TOWER (+ -1 N)) (GET B S)) B S))) (<= 0 (+ -1 N)) (INTEGERP B) (<= 0 B) (<= B 2) (INTEGERP A) (<= 0 A) (<= A 2) (INTEGERP C) (<= 0 C) (<= C 2) (NOT (EQUAL B A)) (NOT (EQUAL B C)) (NOT (EQUAL A C)) (< (+ -1 N) N) (EQUAL (PLAY (H B A C (+ -1 N))