mac:~$ cd class-demo-2008-10-30 mac:~/class-demo-2008-10-30$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defun foo (x) x) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (EQUAL (FOO X) X). Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.02) FOO ACL2 !>(defun bar (x) x) Since BAR is non-recursive, its admission is trivial. We observe that the type of BAR is described by the theorem (EQUAL (BAR X) X). Summary Form: ( DEFUN BAR ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) BAR ACL2 !>(defthm foo-is-bar (equal (foo x) (bar x))) ACL2 Warning [Non-rec] in ( DEFTHM FOO-IS-BAR ...): A :REWRITE rule generated from FOO-IS-BAR will be triggered only by terms containing the non-recursive function symbol FOO. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM FOO-IS-BAR ...): A newly proposed :REWRITE rule generated from FOO-IS-BAR probably subsumes the previously added :REWRITE rule FOO, in the sense that the new rule will now probably be applied whenever the old rule would have been. ACL2 Warning [Subsume] in ( DEFTHM FOO-IS-BAR ...): The previously added rule FOO subsumes a newly proposed :REWRITE rule generated from FOO-IS-BAR, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. But we reduce the conjecture to T, by the simple :definitions BAR and FOO. Q.E.D. Summary Form: ( DEFTHM FOO-IS-BAR ...) Rules: ((:DEFINITION BAR) (:DEFINITION FOO)) Warnings: Subsume and Non-rec Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FOO-IS-BAR ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN FOO (X) ...) L 2 (DEFUN BAR (X) ...) 3:x(DEFTHM FOO-IS-BAR ...) ACL2 !>(defun h (x) (declare (xargs :mode :program)) x) Summary Form: ( DEFUN H ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN FOO (X) ...) L 2 (DEFUN BAR (X) ...) 3 (DEFTHM FOO-IS-BAR ...) P 4:x(DEFUN H (X) ...) ACL2 !>:ubt 2 ACL2 Query (:UBT): The command (DEFUN H (X) (DECLARE (XARGS :MODE :PROGRAM)) ...) introduced the :program name H. Do you wish to re-execute this command after the :UBT? (Y, N, Y!, N!, Q or ?): ? ACL2 Query (:UBT): We are undoing some commands. We have encountered a command, printed above, that introduced a :program function symbol. It is unusual to use :UBT while defining :program functions, since redefinition is permitted. Therefore, we suspect that you are mixing :program and :logic definitions, as when one is developing utilities for the prover. When undoing through such a mixed session, it is often intended that the :logic functions be undone while the :program ones not be, since the latter ones are just utilities. While we cannot selectively undo commands, we do offer to redo selected commands when we have finished undoing. The situation is complicated by the fact that :programs can become :logic functions after the introductory event and that the same name can be redefined several times. Unless noted in the question above, the functions discussed are all still :program. The commands we offer for re-execution are those responsible for introducing the most recent definitions of :program names, whether the names are still :program or not. That is, if in the region undone there is more than one :program definition of a name, we will offer to redo the chronologica\ lly latest one. If you answer Y, the command printed above will be re-executed. If you answer N, it will not be. The answer Y! means the same thing as answering Y to this and all subsequent queries in this :UBT The answer N! is analogous. Finally, Q means to abort the :UBT without undoing anything. (Y, N, Y!, N! or Q): n L 1:x(DEFUN FOO (X) ...) ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1:x(DEFUN FOO (X) ...) ACL2 !>Bye. mac:~/class-demo-2008-10-30$ mkdir scratch mac:~/class-demo-2008-10-30$ ls Makefile isort-is-msort.out Makefile.~1~ isort.cert README isort.lisp README.~1~ isort.out convert-perm-to-how-many-annotated.cert msort.cert convert-perm-to-how-many-annotated.lisp msort.lisp convert-perm-to-how-many-annotated.out msort.out convert-perm-to-how-many.cert ordered-perms.cert convert-perm-to-how-many.lisp ordered-perms.lisp convert-perm-to-how-many.out ordered-perms.out isort-is-msort.cert scratch isort-is-msort.lisp mac:~/class-demo-2008-10-30$ cp -p isort.lisp scratch/ mac:~/class-demo-2008-10-30$ cd scratch/ mac:~/class-demo-2008-10-30/scratch$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/scratch/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(ld "isort.lisp") ACL2 Version 3.4. Level 2. Cbd "/Users/kaufmann/class-demo-2008-10-30/scratch/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>> "ACL2" ACL2 !>> Summary Form: ( INCLUDE-BOOK "sorting/perm" ...) Rules: NIL Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) "/Users/kaufmann/acl2/v3-4/acl2-sources/books/sorting/perm.lisp" ACL2 !>> ACL2 Error in ( INCLUDE-BOOK "convert-perm-to-how-many" ...): There is no file named "/Users/kaufmann/class-demo-2008-10-30/scratch/convert-perm-to-how-many.lisp" that can be opened for input. Summary Form: ( INCLUDE-BOOK "convert-perm-to-how-many" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( INCLUDE-BOOK "convert-perm-to-how-many" ...): See :DOC failure. ******** FAILED ******** :ERROR ACL2 !>Bye. mac:~/class-demo-2008-10-30/scratch$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/scratch/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(ld "isort.lisp") ACL2 Version 3.4. Level 2. Cbd "/Users/kaufmann/class-demo-2008-10-30/scratch/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>> "ACL2" ACL2 !>> Summary Form: ( INCLUDE-BOOK "sorting/perm" ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) "/Users/kaufmann/acl2/v3-4/acl2-sources/books/sorting/perm.lisp" ACL2 !>> Summary Form: ( INCLUDE-BOOK "../convert-perm-to-how-many" ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) "/Users/kaufmann/class-demo-2008-10-30/convert-perm-to-how-many.lisp" ACL2 !>> Summary Form: ( INCLUDE-BOOK "../ordered-perms" ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) "/Users/kaufmann/class-demo-2008-10-30/ordered-perms.lisp" ACL2 !>> The admission of INSERT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of INSERT is described by the theorem (CONSP (INSERT E X)). We used primitive type reasoning. Summary Form: ( DEFUN INSERT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) INSERT ACL2 !>> The admission of ISORT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of ISORT is described by the theorem (OR (CONSP (ISORT X)) (EQUAL (ISORT X) NIL)). We used the :type-prescription rule INSERT. Summary Form: ( DEFUN ISORT ...) Rules: ((:TYPE-PRESCRIPTION INSERT)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ISORT ACL2 !>> I-AM-HERE :ERROR ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) 1 (INCLUDE-BOOK "sorting/perm" :DIR ...) 2 (INCLUDE-BOOK "../convert-perm-to-how-many") d 3 (INCLUDE-BOOK "../ordered-perms") L 4 (DEFUN INSERT (E X) ...) L 5:x(DEFUN ISORT (X) ...) ACL2 !>:ubt! 1 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(ld "isort.lisp" :ld-skip-proofsp t) ACL2 Version 3.4. Level 2. Cbd "/Users/kaufmann/class-demo-2008-10-30/scratch/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !s>> "ACL2" ACL2 !s>> "/Users/kaufmann/acl2/v3-4/acl2-sources/books/sorting/perm.lisp" ACL2 !s>> "/Users/kaufmann/class-demo-2008-10-30/convert-perm-to-how-many.lisp" ACL2 !s>> "/Users/kaufmann/class-demo-2008-10-30/ordered-perms.lisp" ACL2 !s>> INSERT ACL2 !s>> ISORT ACL2 !s>> I-AM-HERE :ERROR ACL2 !>:ubt! 1 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(rebuild "isort.lisp" t) ACL2 loading "isort.lisp". "ACL2" "/Users/kaufmann/acl2/v3-4/acl2-sources/books/sorting/perm.lisp" "/Users/kaufmann/class-demo-2008-10-30/convert-perm-to-how-many.lisp" "/Users/kaufmann/class-demo-2008-10-30/ordered-perms.lisp" INSERT ISORT I-AM-HERE Finished loading "isort.lisp". T ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) 1 (INCLUDE-BOOK "sorting/perm" :DIR ...) 2 (INCLUDE-BOOK "../convert-perm-to-how-many") d 3 (INCLUDE-BOOK "../ordered-perms") L 4 (DEFUN INSERT (E X) ...) L 5:x(DEFUN ISORT (X) ...) ACL2 !>:ubt! 1 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(rebuild "isort.lisp" 'insert) ACL2 loading "isort.lisp". "ACL2" "/Users/kaufmann/acl2/v3-4/acl2-sources/books/sorting/perm.lisp" "/Users/kaufmann/class-demo-2008-10-30/convert-perm-to-how-many.lisp" "/Users/kaufmann/class-demo-2008-10-30/ordered-perms.lisp" INSERT Finished loading "isort.lisp". T ACL2 !>:ubt! 1 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(rebuild "isort.lisp" nil) ACL2 Error in LD: NIL is an illegal value for the state global variable LD-PRE-EVAL-FILTER. See :DOC LD-PRE-EVAL-FILTER. T ACL2 !>:trans1 (rebuild "isort.lisp" 'insert) (REBUILD-FN "isort.lisp" 'INSERT T NIL STATE) ACL2 !>:pe insert ACL2 Error in :PE: The object INSERT is not a logical name. See :DOC logical-name. ACL2 !>:oops Installing the requested world. L 4:x(DEFUN INSERT (E X) ...) ACL2 !>:pe insert L 4:x(DEFUN INSERT (E X) (IF (ENDP X) (CONS E X) (IF (LEXORDER E (CAR X)) (CONS E X) (CONS (CAR X) (INSERT E (CDR X)))))) ACL2 !>:doc pe | PE print the events named by a logical name | | | Example: | :pe fn ; sketches the command that introduced fn and | ; prints in full the event within it that created fn. | | See :DOC LOGICAL-NAME. (type :more for more, :more! for the rest) ACL2 !>:more! | Pe takes one argument, a logical name, and prints in full the event | corresponding to the name. Pe also sketches the command responsible | for that event if the command is different from the event itself. | See :DOC PC for a description of the format used to display a command. To | remind you that the event is inferior to the command, i.e., you can only | undo the entire command, not just the event, the event is indented | slightly from the command and a slash (meant to suggest a tree branch) | connects them. | | If the given logical name corresponds to more than one event, then :pe | will print the above information for every such event. Here is an | example of such behavior. | | ACL2 !>:pe nth | -4270 (ENCAPSULATE NIL ...) | \ | >V (VERIFY-TERMINATION NTH) | | Additional events for the logical name NTH: | PV -4949 (DEFUN NTH (N L) | "Documentation available via :doc" | (DECLARE (XARGS :GUARD (AND (INTEGERP N) | (>= N 0) | (TRUE-LISTP L)))) | (IF (ENDP L) | NIL | (IF (ZP N) | (CAR L) | (NTH (- N 1) (CDR L))))) | ACL2 !> | | If you prefer to see only the formula for the given name, for example if it | is part of a large mutual-recursion, see :DOC PF. *- ACL2 !>Bye. mac:~/class-demo-2008-10-30/scratch$ acl2 Welcome to Clozure Common Lisp Version 1.2-r10991M-trunk (DarwinX8664)! ; *hons-init-hook*: Setting (ccl::lisp-heap-gc-threshold) to 134,217,728 bytes. ACL2 Version 3.4 built October 5, 2008 16:40:06. Copyright (C) 2008 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*). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-3-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. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2h-e4/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/scratch/". Distributed books directory "/Users/kaufmann/acl2h-e4/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>Bye. mac:~/class-demo-2008-10-30/scratch$ acl2-34 bash: acl2-34: command not found mac:~/class-demo-2008-10-30/scratch$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/scratch/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(thm (equal x x)) But we reduce the conjecture to T, by primitive type reasoning. Q.E.D. Summary Form: ( THM ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Proof succeeded. ACL2 !>(verify (equal (append (append x y) z) (append x (append y z)))) ->: p (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z)) ->: help | :HELP (macro) | proof-checker help facility | | | Examples: | | (help rewrite) -- partial documentation on the rewrite command; the | rest is available using more or more! | | (help! rewrite) -- full documentation on the rewrite command | | help, help! -- this documentation (in part, or in totality, | respectively) (type :more for more, :more! for the rest) ->: more! | General Forms: | (help &optional command) | (help! &optional command) | more | more! | | The proof checker supports the same kind of documentation as does | ACL2 proper. The main difference is that you need to type | | (help command) | | in a list rather than :doc command. So, to get all the | documentation on command, type (help! command) inside the | interactive loop, but to get only a one-line description of the | command together with some examples, type (help command). In the | latter case, you can get the rest of the help by typing more!; or | type more if you don't necessarily want all the rest of the help at | once. (Then keep typing more if you want to keep getting more of | the help for that command.) | | To summarize: as with ACL2, you can type either of the following: | | more, more! | -- to obtain more (or, all the rest of) the documentation last | requested by help (or, outside the proof-checker's loop, :doc) | | It has been arranged that the use of (help command) will tell you | just about everything you could want to know about command, almost | always by way of examples. For more details about a command, use | help!, more, or more!. | | We use the word ``command'' to refer to the name itself, e.g. | rewrite. We use the word ``instruction'' to refer to an input to | the interactive system, e.g. (rewrite foo) or (help split). Of | course, we allow commands with no arguments as instructions in many | cases, e.g. rewrite. In such cases, command is treated identically | to (command). *- ->: th *** Top-level hypotheses: There are no top-level hypotheses. The current subterm is: (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z)) ->: goals MAIN ->: (induct (append x y)) ***** Now entering the theorem prover ***** [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 (BINARY-APPEND X Y). This suggestion was produced using the :induction rule BINARY-APPEND. If we let (:P X Y Z) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y Z)) (:P X Y Z)) (IMPLIES (ENDP X) (:P X Y Z))). This induction is justified by the same argument used to admit BINARY-APPEND. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) Y Z))) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))). But we have been asked to pretend that this goal is subsumed by the as-yet-to-be-proved |PROOF-CHECKER Subgoal *1/2|. Subgoal *1/1 (IMPLIES (ENDP X) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))). But we have been asked to pretend that this goal is subsumed by the as-yet-to-be-proved |PROOF-CHECKER Subgoal *1/1|. That completes the proof of *1. Q.E.D. Creating two new goals: (MAIN . 1) and (MAIN . 2). The proof of the current goal, MAIN, has been completed. However, the following subgoals remain to be proved: (MAIN . 1) and (MAIN . 2). Now proving (MAIN . 1). ->: goals (MAIN . 1) (MAIN . 2) ->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) 2. (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) Y Z)) The current subterm is: (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z)) ->: (dv 1 1 0) ->: p (APPEND X Y) ->: x #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: p (CONS (CAR X) (APPEND (CDR X) Y)) ->: p-top (EQUAL (APPEND (*** (CONS (CAR X) (APPEND (CDR X) Y)) ***) Z) (APPEND X Y Z)) ->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) 2. (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) Y Z)) The current subterm is: (CONS (CAR X) (APPEND (CDR X) Y)) ->: top ->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) 2. (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) Y Z)) The current subterm is: (EQUAL (APPEND (CONS (CAR X) (APPEND (CDR X) Y)) Z) (APPEND X Y Z)) ->: 1 ->: p (APPEND (CONS (CAR X) (APPEND (CDR X) Y)) Z) ->: x #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: p (CONS (CAR X) (APPEND (APPEND (CDR X) Y) Z)) ->: p-top (EQUAL (*** (CONS (CAR X) (APPEND (APPEND (CDR X) Y) Z)) ***) (APPEND X Y Z)) ->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) 2. (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) Y Z)) The current subterm is: (CONS (CAR X) (APPEND (APPEND (CDR X) Y) Z)) ->: 2 ->: p (APPEND (APPEND (CDR X) Y) Z) ->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) 2. (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) Y Z)) The current subterm is: (APPEND (APPEND (CDR X) Y) Z) ->: = Using hypothesis #2. ->: p (APPEND (CDR X) Y Z) ->: (drop 2) ->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) The current subterm is: (APPEND (CDR X) Y Z) ->: top ->: th *** Top-level hypotheses: 1. (NOT (ENDP X)) The current subterm is: (EQUAL (CONS (CAR X) (APPEND (CDR X) Y Z)) (APPEND X Y Z)) ->: pp (EQUAL (CONS (CAR X) (BINARY-APPEND (CDR X) (BINARY-APPEND Y Z))) (BINARY-APPEND X (BINARY-APPEND Y Z))) ->: 2 ->: p (APPEND X Y Z) ->: x #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: p (CONS (CAR X) (APPEND (CDR X) Y Z)) ->: top ->: p (EQUAL (CONS (CAR X) (APPEND (CDR X) Y Z)) (CONS (CAR X) (APPEND (CDR X) Y Z))) ->: s The proof of the current goal, (MAIN . 1), has been completed, as have all of its subgoals. Now proving (MAIN . 2). ->: th *** Top-level hypotheses: 1. (ENDP X) The current subterm is: (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z)) ->: prove ***** Now entering the theorem prover ***** By the simple :definition ENDP we reduce the conjecture to Goal' (IMPLIES (NOT (CONSP X)) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))). But simplification reduces this to T, using the :definition BINARY-APPEND and primitive type reasoning. Q.E.D. *!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!* You may wish to exit. ->: (exit append-assoc) (DEFTHM APPEND-ASSOC (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z))) :INSTRUCTIONS ((:INDUCT (APPEND X Y)) (:DV 1 1 0) :X :TOP (:DV 1) :X (:DV 2) := (:DROP 2) :TOP (:DV 2) :X :TOP :S :PROVE)) ACL2 Query (ACL2-PC::EXIT): Do you want to submit this event? Possible replies are: Y (Yes), R (yes and Replay commands), N (No, but exit), A (Abort exiting). (Y, R, N or A): y Summary Form: ( DEFTHM APPEND-ASSOC ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION BINARY-APPEND) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) APPEND-ASSOC ACL2 !>:u 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(DEFTHM APPEND-ASSOC (EQUAL (APPEND (APPEND X Y) Z) (APPEND X (APPEND Y Z))) :INSTRUCTIONS ((:INDUCT (APPEND X Y)) (:DV 1 1 0) :X :TOP (:DV 1) :X (:DV 2) := (:DROP 2) :TOP (:DV 2) :X :TOP :S :PROVE)) Entering the proof-checker.... ->: (:INDUCT (APPEND X Y)) ***** Now entering the theorem prover ***** [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 (BINARY-APPEND X Y). This suggestion was produced using the :induction rule BINARY-APPEND. If we let (:P X Y Z) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y Z)) (:P X Y Z)) (IMPLIES (ENDP X) (:P X Y Z))). This induction is justified by the same argument used to admit BINARY-APPEND. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (EQUAL (APPEND (APPEND (CDR X) Y) Z) (APPEND (CDR X) Y Z))) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))). But we have been asked to pretend that this goal is subsumed by the as-yet-to-be-proved |PROOF-CHECKER Subgoal *1/2|. Subgoal *1/1 (IMPLIES (ENDP X) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))). But we have been asked to pretend that this goal is subsumed by the as-yet-to-be-proved |PROOF-CHECKER Subgoal *1/1|. That completes the proof of *1. Q.E.D. Creating two new goals: (MAIN . 1) and (MAIN . 2). The proof of the current goal, MAIN, has been completed. However, the following subgoals remain to be proved: (MAIN . 1) and (MAIN . 2). Now proving (MAIN . 1). ->: (:DV 1 1 0) ->: :X #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: :TOP ->: (:DV 1) ->: :X #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: (:DV 2) ->: := Using hypothesis #2. ->: (:DROP 2) ->: :TOP ->: (:DV 2) ->: :X #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: :TOP ->: :S The proof of the current goal, (MAIN . 1), has been completed, as have all of its subgoals. Now proving (MAIN . 2). ->: :PROVE ***** Now entering the theorem prover ***** By the simple :definition ENDP we reduce the conjecture to Goal' (IMPLIES (NOT (CONSP X)) (EQUAL (APPEND (APPEND X Y) Z) (APPEND X Y Z))). But simplification reduces this to T, using the :definition BINARY-APPEND and primitive type reasoning. Q.E.D. *!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!* Summary Form: ( DEFTHM APPEND-ASSOC ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION BINARY-APPEND) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) APPEND-ASSOC ACL2 !>Bye. mac:~/class-demo-2008-10-30/scratch$ cd .. mac:~/class-demo-2008-10-30$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>:trans1 (defthmd ordered-perms (implies (and (true-listp a) (true-listp b) (orderedp a) (orderedp b)) (equal (equal a b) (perm a b)))) (PROGN (DEFTHM ORDERED-PERMS (IMPLIES (AND (TRUE-LISTP A) (TRUE-LISTP B) (ORDEREDP A) (ORDEREDP B)) (EQUAL (EQUAL A B) (PERM A B)))) (WITH-OUTPUT :OFF SUMMARY (IN-THEORY (DISABLE ORDERED-PERMS))) (VALUE-TRIPLE '(:DEFTHMD ORDERED-PERMS))) ACL2 !>(defun foo (x) (progn x x)) ACL2 Error in ( DEFUN FOO ...): We do not permit the use of PROGN inside of code to be executed by Common Lisp because its Common Lisp meaning differs from its ACL2 meaning. Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( DEFUN FOO ...): See :DOC failure. ******** FAILED ******** ACL2 !>Bye. mac:~/class-demo-2008-10-30$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(accumulated-persistence t) NIL ACL2 !>:mini-proveall ACL2 Version 3.4. Level 2. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>>:LOGIC The event ( TABLE ACL2-DEFAULTS-TABLE ...) is redundant. See :DOC redundant-events. ACL2 !>>(THM (IMPLIES (AND (TRUE-LISTP X) (TRUE-LISTP Y)) (EQUAL (REVAPPEND (APPEND X Y) Z) (REVAPPEND Y (REVAPPEND X Z))))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Five induction schemes are suggested by this conjecture. These merge into two derived induction schemes. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (REVAPPEND X Z), but modified to accommodate (APPEND X Y). These suggestions were produced using the :induction rules BINARY-APPEND, REVAPPEND and TRUE-LISTP. If we let (:P X Y Z) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X) Y (CONS (CAR X) Z))) (:P X Y Z)) (IMPLIES (ENDP X) (:P X Y Z))). This induction is justified by the same argument used to admit REVAPPEND. Note, however, that the unmeasured variable Z is being instantiated. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION BINARY-APPEND) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION REVAPPEND) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION BINARY-APPEND) (:INDUCTION REVAPPEND) (:INDUCTION TRUE-LISTP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Proof succeeded. ACL2 !>>(DEFUN APP (X Y) (IF (CONSP X) (CONS (CAR X) (APP (CDR X) Y)) Y)) The admission of APP is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of APP is described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive type reasoning. Summary Form: ( DEFUN APP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) APP ACL2 !>>(DEFTHM ASSOC-OF-APP (EQUAL (APP (APP A B) C) (APP A (APP B C)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (APP A B). This suggestion was produced using the :induction rule APP. If we let (:P A B C) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP A)) (:P A B C)) (IMPLIES (AND (CONSP A) (:P (CDR A) B C)) (:P A B C))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM ASSOC-OF-APP ...) Rules: ((:DEFINITION APP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) ASSOC-OF-APP ACL2 !>>(DEFUN REV (X) (IF (CONSP X) (APP (REV (CDR X)) (CONS (CAR X) NIL)) NIL)) The admission of REV is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of REV is described by the theorem (OR (CONSP (REV X)) (EQUAL (REV X) NIL)). We used primitive type reasoning and the :type-prescription rule APP. Summary Form: ( DEFUN REV ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION APP)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) REV ACL2 !>>(DEFTHM TRUE-LISTP-REV (TRUE-LISTP (REV X)) :RULE-CLASSES (:REWRITE :GENERALIZE)) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rule REV. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X)) (IMPLIES (AND (CONSP X) (:P (CDR X))) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1''' Subgoal *1/1'4' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/1' (IMPLIES (AND (CONSP X) (TRUE-LISTP (REV (CDR X)))) (TRUE-LISTP (APP (REV (CDR X)) (LIST (CAR X))))) *1.1 (Subgoal *1/1'4') is pushed for proof by induction. ]) So we now return to *1.1, which is (IMPLIES (TRUE-LISTP RV) (TRUE-LISTP (APP RV (LIST X1)))). Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/1 *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/1' and Goal are COMPLETED! Q.E.D. The storage of TRUE-LISTP-REV depends upon the :type-prescription rule TRUE-LISTP. Summary Form: ( DEFTHM TRUE-LISTP-REV ...) Rules: ((:DEFINITION APP) (:DEFINITION REV) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION REV) (:INDUCTION TRUE-LISTP) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION TRUE-LISTP)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.01, other: 0.00) TRUE-LISTP-REV ACL2 !>>(DEFTHM REV-APP-PROOF-CHECKER (EQUAL (REV (APP A B)) (APP (REV B) (REV A))) :RULE-CLASSES NIL :INSTRUCTIONS (:INDUCT :BASH :INDUCT :BASH :SPLIT (:DV 1) :X :NX (:DV 1) :X :TOP :S :BASH (:DIVE 1 1) := (:DROP 2) :TOP :BASH)) Entering the proof-checker.... ->: :INDUCT ***** Now entering the theorem prover ***** *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. We have been told to use induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (APP A B). This suggestion was produced using the :induction rules APP and REV. If we let (:P A B) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP A)) (:P A B)) (IMPLIES (AND (CONSP A) (:P (CDR A) B)) (:P A B))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2 (IMPLIES (NOT (CONSP A)) (EQUAL (REV (APP A B)) (APP (REV B) (REV A)))) Subgoal *1/2 is subsumed by a goal yet to be proved. ]) Subgoal *1/1 ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/1 (IMPLIES (AND (CONSP A) (EQUAL (REV (APP (CDR A) B)) (APP (REV B) (REV (CDR A))))) (EQUAL (REV (APP A B)) (APP (REV B) (REV A)))) Subgoal *1/1 is subsumed by a goal yet to be proved. ]) *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Creating two new goals: (MAIN . 1) and (MAIN . 2). The proof of the current goal, MAIN, has been completed. However, the following subgoals remain to be proved: (MAIN . 1) and (MAIN . 2). Now proving (MAIN . 1). ->: :BASH ***** Now entering the theorem prover ***** Goal' ([ A key checkpoint: Goal' (IMPLIES (NOT (CONSP A)) (EQUAL (REV B) (APP (REV B) NIL))) Goal' is subsumed by a goal yet to be proved. ]) Q.E.D. Creating one new goal: ((MAIN . 1) . 1). The proof of the current goal, (MAIN . 1), has been completed. However, the following subgoals remain to be proved: ((MAIN . 1) . 1). Now proving ((MAIN . 1) . 1). ->: :INDUCT ***** Now entering the theorem prover ***** *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. We have been told to use induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (REV B). This suggestion was produced using the :induction rule REV. If we let (:P A B) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP B)) (:P A B)) (IMPLIES (AND (CONSP B) (:P A (CDR B))) (:P A B))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2 (IMPLIES (NOT (CONSP B)) (IMPLIES (NOT (CONSP A)) (EQUAL (REV B) (APP (REV B) NIL)))) Subgoal *1/2 is subsumed by a goal yet to be proved. ]) Subgoal *1/1 ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/1 (IMPLIES (AND (CONSP B) (IMPLIES (NOT (CONSP A)) (EQUAL (REV (CDR B)) (APP (REV (CDR B)) NIL)))) (IMPLIES (NOT (CONSP A)) (EQUAL (REV B) (APP (REV B) NIL)))) Subgoal *1/1 is subsumed by a goal yet to be proved. ]) *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Creating two new goals: (((MAIN . 1) . 1) . 1) and (((MAIN . 1) . 1) . 2). The proof of the current goal, ((MAIN . 1) . 1), has been completed. However, the following subgoals remain to be proved: (((MAIN . 1) . 1) . 1) and (((MAIN . 1) . 1) . 2). Now proving (((MAIN . 1) . 1) . 1). ->: :BASH ***** Now entering the theorem prover ***** Goal' Q.E.D. The proof of the current goal, (((MAIN . 1) . 1) . 1), has been completed, as have all of its subgoals. Now proving (((MAIN . 1) . 1) . 2). ->: :SPLIT ***** Now entering the theorem prover ***** Goal' Goal'' ([ A key checkpoint: Goal'' (IMPLIES (AND (CONSP B) (EQUAL (REV (CDR B)) (APP (REV (CDR B)) NIL)) (NOT (CONSP A))) (EQUAL (REV B) (APP (REV B) NIL))) Goal'' is subsumed by a goal yet to be proved. ]) Q.E.D. Creating one new goal: ((((MAIN . 1) . 1) . 2) . 1). The proof of the current goal, (((MAIN . 1) . 1) . 2), has been completed. However, the following subgoals remain to be proved: ((((MAIN . 1) . 1) . 2) . 1). Now proving ((((MAIN . 1) . 1) . 2) . 1). ->: (:DV 1) ->: :X #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: :NX #->: UP #->: 2 ->: (:DV 1) ->: :X #->: (EXPAND T) #->: (SUCCEED (S)) ##->: (S) ->: :TOP ->: :S The proof of the current goal, ((((MAIN . 1) . 1) . 2) . 1), has been completed, as have all of its subgoals. Now proving (MAIN . 2). ->: :BASH ***** Now entering the theorem prover ***** Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (CONSP A) (EQUAL (REV (APP (CDR A) B)) (APP (REV B) (REV (CDR A))))) (EQUAL (APP (REV (APP (CDR A) B)) (LIST (CAR A))) (APP (REV B) (APP (REV (CDR A)) (LIST (CAR A)))))) Goal' is subsumed by a goal yet to be proved. ]) Q.E.D. Creating one new goal: ((MAIN . 2) . 1). The proof of the current goal, (MAIN . 2), has been completed. However, the following subgoals remain to be proved: ((MAIN . 2) . 1). Now proving ((MAIN . 2) . 1). ->: (:DIVE 1 1) ->: := Using hypothesis #2. ->: (:DROP 2) ->: :TOP ->: :BASH ***** Now entering the theorem prover ***** Q.E.D. *!*!*!*!*!*!* All goals have been proved! *!*!*!*!*!*!* Summary Form: ( DEFTHM REV-APP-PROOF-CHECKER ...) Rules: ((:DEFINITION APP) (:DEFINITION NOT) (:DEFINITION REV) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART IF) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION REV) (:REWRITE ASSOC-OF-APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.05 seconds (prove: 0.01, print: 0.02, other: 0.02) REV-APP-PROOF-CHECKER ACL2 !>>(DEFTHM REV-APP (EQUAL (REV (APP A B)) (APP (REV B) (REV A)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (APP A B). This suggestion was produced using the :induction rules APP and REV. If we let (:P A B) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP A)) (:P A B)) (IMPLIES (AND (CONSP A) (:P (CDR A) B)) (:P A B))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2' (IMPLIES (NOT (CONSP A)) (EQUAL (REV B) (APP (REV B) NIL))) *1.1 (Subgoal *1/2''') is pushed for proof by induction. ]) Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1''' Subgoal *1/1'4' So we now return to *1.1, which is (IMPLIES (TRUE-LISTP RV) (EQUAL RV (APP RV NIL))). Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/1 *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/2' and Goal are COMPLETED! Q.E.D. Summary Form: ( DEFTHM REV-APP ...) Rules: ((:DEFINITION APP) (:DEFINITION REV) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:GENERALIZE TRUE-LISTP-REV) (:INDUCTION APP) (:INDUCTION REV) (:INDUCTION TRUE-LISTP) (:REWRITE ASSOC-OF-APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.01, other: 0.00) REV-APP ACL2 !>>(DEFTHM REV-REV (IMPLIES (TRUE-LISTP X) (EQUAL (REV (REV X)) X))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rules REV and TRUE-LISTP. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X)) (IMPLIES (AND (CONSP X) (:P (CDR X))) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM REV-REV ...) Rules: ((:DEFINITION APP) (:DEFINITION REV) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART REV) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:INDUCTION TRUE-LISTP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR) (:REWRITE REV-APP)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) REV-REV ACL2 !>>(ENCAPSULATE (((LT * *) => *)) (LOCAL (DEFUN LT (X Y) (DECLARE (IGNORE X Y)) NIL)) (DEFTHM LT-NON-SYMMETRIC (IMPLIES (LT X Y) (NOT (LT Y X))))) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>>(LOCAL (DEFUN LT (X Y) (DECLARE (IGNORE X Y)) NIL)) Since LT is non-recursive, its admission is trivial. We observe that the type of LT is described by the theorem (EQUAL (LT X Y) NIL). Summary Form: ( DEFUN LT ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) LT ACL2 !>>>(DEFTHM LT-NON-SYMMETRIC (IMPLIES (LT X Y) (NOT (LT Y X)))) ACL2 Warning [Non-rec] in ( DEFTHM LT-NON-SYMMETRIC ...): A :REWRITE rule generated from LT-NON-SYMMETRIC will be triggered only by terms containing the non-recursive function symbol LT. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM LT-NON-SYMMETRIC ...): The previously added rule LT subsumes a newly proposed :REWRITE rule generated from LT-NON-SYMMETRIC, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application\ . Q.E.D. Summary Form: ( DEFTHM LT-NON-SYMMETRIC ...) Rules: ((:TYPE-PRESCRIPTION LT)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) LT-NON-SYMMETRIC End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. The following constraint is associated with the function LT: (IMPLIES (LT X Y) (NOT (LT Y X))) Summary Form: ( ENCAPSULATE (((LT * ...) ...) ...) ...) Rules: NIL Warnings: Subsume and Non-rec Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) T ACL2 !>>(DEFUN INSERT (X LST) (COND ((ATOM LST) (LIST X)) ((LT X (CAR LST)) (CONS X LST)) (T (CONS (CAR LST) (INSERT X (CDR LST)))))) The admission of INSERT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT LST). We observe that the type of INSERT is described by the theorem (CONSP (INSERT X LST)). We used primitive type reasoning. Summary Form: ( DEFUN INSERT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) INSERT ACL2 !>>(DEFUN INSERT-SORT (LST) (COND ((ATOM LST) NIL) (T (INSERT (CAR LST) (INSERT-SORT (CDR LST)))))) The admission of INSERT-SORT is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT LST). We observe that the type of INSERT-SORT is described by the theorem (OR (CONSP (INSERT-SORT LST)) (EQUAL (INSERT-SORT LST) NIL)). We used the :type-prescription rule INSERT. Summary Form: ( DEFUN INSERT-SORT ...) Rules: ((:TYPE-PRESCRIPTION INSERT)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) INSERT-SORT ACL2 !>>(DEFUN DEL (X LST) (COND ((ATOM LST) NIL) ((EQUAL X (CAR LST)) (CDR LST)) (T (CONS (CAR LST) (DEL X (CDR LST)))))) The admission of DEL is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT LST). We could deduce no constraints on the type of DEL. Summary Form: ( DEFUN DEL ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) DEL ACL2 !>>(DEFUN MEM (X LST) (COND ((ATOM LST) NIL) ((EQUAL X (CAR LST)) T) (T (MEM X (CDR LST))))) The admission of MEM is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT LST). We observe that the type of MEM is described by the theorem (OR (EQUAL (MEM X LST) T) (EQUAL (MEM X LST) NIL)). Summary Form: ( DEFUN MEM ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) MEM ACL2 !>>(DEFUN PERM (LST1 LST2) (COND ((ATOM LST1) (ATOM LST2)) ((MEM (CAR LST1) LST2) (PERM (CDR LST1) (DEL (CAR LST1) LST2))) (T NIL))) The admission of PERM is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT LST1). We observe that the type of PERM is described by the theorem (OR (EQUAL (PERM LST1 LST2) T) (EQUAL (PERM LST1 LST2) NIL)). Summary Form: ( DEFUN PERM ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) PERM ACL2 !>>(DEFTHM PERM-REFLEXIVE (PERM X X)) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (PERM X X). This suggestion was produced using the :induction rule PERM. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (MEM (CAR X) X))) (:P X)) (IMPLIES (AND (NOT (ATOM X)) (MEM (CAR X) X) (:P (CDR X))) (:P X)) (IMPLIES (ATOM X) (:P X))). This induction is justified by the same argument used to admit PERM. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of PERM-REFLEXIVE depends upon the :type-prescription rule PERM. Summary Form: ( DEFTHM PERM-REFLEXIVE ...) Rules: ((:DEFINITION ATOM) (:DEFINITION DEL) (:DEFINITION MEM) (:DEFINITION NOT) (:DEFINITION PERM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION PERM) (:TYPE-PRESCRIPTION PERM)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) PERM-REFLEXIVE ACL2 !>>(DEFTHM PERM-CONS (IMPLIES (MEM A X) (EQUAL (PERM X (CONS A Y)) (PERM (DEL A X) Y))) :HINTS (("Goal" :INDUCT (PERM X Y)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. 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 (PERM X Y). This suggestion was produced using the :induction rule PERM. If we let (:P A X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (MEM (CAR X) Y))) (:P A X Y)) (IMPLIES (AND (NOT (ATOM X)) (MEM (CAR X) Y) (:P A (CDR X) (DEL (CAR X) Y))) (:P A X Y)) (IMPLIES (ATOM X) (:P A X Y))). This induction is justified by the same argument used to admit PERM. Note, however, that the unmeasured variable Y is being instantiated. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/2 Subgoal *1/2' Subgoal *1/2.2 Subgoal *1/2.1 Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM PERM-CONS ...) Rules: ((:DEFINITION ATOM) (:DEFINITION DEL) (:DEFINITION MEM) (:DEFINITION NOT) (:DEFINITION PERM) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION PERM) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION MEM)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.00) PERM-CONS ACL2 !>>(DEFTHM PERM-SYMMETRIC (IMPLIES (PERM X Y) (PERM Y X))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. We will choose arbitrarily among these. We will induct according to a scheme suggested by (PERM X Y). This suggestion was produced using the :induction rule PERM. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (MEM (CAR X) Y))) (:P X Y)) (IMPLIES (AND (NOT (ATOM X)) (MEM (CAR X) Y) (:P (CDR X) (DEL (CAR X) Y))) (:P X Y)) (IMPLIES (ATOM X) (:P X Y))). This induction is justified by the same argument used to admit PERM. Note, however, that the unmeasured variable Y is being instantiated. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1/4 Subgoal *1/4' Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of PERM-SYMMETRIC depends upon the :type-prescription rule PERM. Summary Form: ( DEFTHM PERM-SYMMETRIC ...) Rules: ((:DEFINITION ATOM) (:DEFINITION NOT) (:DEFINITION PERM) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION PERM) (:REWRITE PERM-CONS) (:TYPE-PRESCRIPTION MEM) (:TYPE-PRESCRIPTION PERM)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.00) PERM-SYMMETRIC ACL2 !>>(DEFTHM MEM-DEL (IMPLIES (MEM A (DEL B X)) (MEM A X)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ONCE))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (MEM A X), but modified to accommodate (DEL B X). These suggestions were produced using the :induction rules DEL and MEM. If we let (:P A B X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL A (CAR X))) (:P A B (CDR X))) (:P A B X)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL A (CAR X))) (:P A B X)) (IMPLIES (ATOM X) (:P A B X))). This induction is justified by the same argument used to admit MEM. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1/4 Subgoal *1/4' Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of MEM-DEL depends upon the :type-prescription rule MEM. Summary Form: ( DEFTHM MEM-DEL ...) Rules: ((:DEFINITION ATOM) (:DEFINITION DEL) (:DEFINITION MEM) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DEL) (:INDUCTION MEM) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION MEM)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) MEM-DEL ACL2 !>>(DEFTHM PERM-MEM (IMPLIES (AND (PERM X Y) (MEM A X)) (MEM A Y)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ONCE))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into two derived induction schemes. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (MEM A X), but modified to accommodate (PERM X Y). These suggestions were produced using the :induction rules MEM and PERM. If we let (:P A X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL A (CAR X))) (:P A (CDR X) (DEL (CAR X) Y))) (:P A X Y)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL A (CAR X))) (:P A X Y)) (IMPLIES (ATOM X) (:P A X Y))). This induction is justified by the same argument used to admit MEM. Note, however, that the unmeasured variable Y is being instantiated. When applied to the goal at hand the above induction scheme produces five nontautological subgoals. Subgoal *1/5 Subgoal *1/5' Subgoal *1/4 Subgoal *1/4' Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of PERM-MEM depends upon the :type-prescription rule MEM. Summary Form: ( DEFTHM PERM-MEM ...) Rules: ((:DEFINITION ATOM) (:DEFINITION MEM) (:DEFINITION NOT) (:DEFINITION PERM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION MEM) (:INDUCTION PERM) (:REWRITE MEM-DEL) (:TYPE-PRESCRIPTION MEM)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.00) PERM-MEM ACL2 !>>(DEFTHM MEM-DEL2 (IMPLIES (AND (MEM A X) (NOT (EQUAL A B))) (MEM A (DEL B X)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (DEL B X), but modified to accommodate (MEM A X). These suggestions were produced using the :induction rules DEL and MEM. If we let (:P A B X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL B (CAR X))) (:P A B (CDR X))) (:P A B X)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL B (CAR X))) (:P A B X)) (IMPLIES (ATOM X) (:P A B X))). This induction is justified by the same argument used to admit DEL. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1/4 Subgoal *1/4' Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of MEM-DEL2 depends upon the :type-prescription rule MEM. Summary Form: ( DEFTHM MEM-DEL2 ...) Rules: ((:DEFINITION ATOM) (:DEFINITION DEL) (:DEFINITION MEM) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DEL) (:INDUCTION MEM) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION MEM)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) MEM-DEL2 ACL2 !>>(DEFTHM COMM-DEL (EQUAL (DEL A (DEL B X)) (DEL B (DEL A X)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (DEL A X), but modified to accommodate (DEL B X). These suggestions were produced using the :induction rule DEL. If we let (:P A B X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL A (CAR X))) (:P A B (CDR X))) (:P A B X)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL A (CAR X))) (:P A B X)) (IMPLIES (ATOM X) (:P A B X))). This induction is justified by the same argument used to admit DEL. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/2 Subgoal *1/2' Subgoal *1/2.2 Subgoal *1/2.1 Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM COMM-DEL ...) Rules: ((:DEFINITION ATOM) (:DEFINITION DEL) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DEL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) COMM-DEL ACL2 !>>(DEFTHM PERM-DEL (IMPLIES (PERM X Y) (PERM (DEL A X) (DEL A Y)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into two derived induction schemes. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (DEL A X), but modified to accommodate (PERM X Y). These suggestions were produced using the :induction rules DEL and PERM. If we let (:P A X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (EQUAL A (CAR X))) (:P A (CDR X) (DEL (CAR X) Y))) (:P A X Y)) (IMPLIES (AND (NOT (ATOM X)) (EQUAL A (CAR X))) (:P A X Y)) (IMPLIES (ATOM X) (:P A X Y))). This induction is justified by the same argument used to admit DEL. Note, however, that the unmeasured variable Y is being instantiated. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1/4 Subgoal *1/4' Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of PERM-DEL depends upon the :type-prescription rule PERM. Summary Form: ( DEFTHM PERM-DEL ...) Rules: ((:DEFINITION ATOM) (:DEFINITION DEL) (:DEFINITION NOT) (:DEFINITION PERM) (:EXECUTABLE-COUNTERPART PERM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DEL) (:INDUCTION PERM) (:REWRITE COMM-DEL) (:REWRITE MEM-DEL2) (:REWRITE PERM-CONS) (:REWRITE PERM-SYMMETRIC) (:TYPE-PRESCRIPTION MEM) (:TYPE-PRESCRIPTION PERM)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00) PERM-DEL ACL2 !>>(DEFTHM PERM-TRANSITIVE (IMPLIES (AND (PERM X Y) (PERM Y Z)) (PERM X Z)) :RULE-CLASSES ((:REWRITE :MATCH-FREE :ONCE))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into two derived induction schemes. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (PERM X Z), but modified to accommodate (PERM X Y). These suggestions were produced using the :induction rule PERM. If we let (:P X Y Z) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (MEM (CAR X) Z))) (:P X Y Z)) (IMPLIES (AND (NOT (ATOM X)) (MEM (CAR X) Z) (:P (CDR X) (DEL (CAR X) Y) (DEL (CAR X) Z))) (:P X Y Z)) (IMPLIES (ATOM X) (:P X Y Z))). This induction is justified by the same argument used to admit PERM. Note, however, that the unmeasured variables Y and Z are being instantiated. When applied to the goal at hand the above induction scheme produces five nontautological subgoals. Subgoal *1/5 Subgoal *1/5' Subgoal *1/5'' Subgoal *1/4 Subgoal *1/4' Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of PERM-TRANSITIVE depends upon the :type-prescriptio\ n rule PERM. Summary Form: ( DEFTHM PERM-TRANSITIVE ...) Rules: ((:DEFINITION ATOM) (:DEFINITION NOT) (:DEFINITION PERM) (:INDUCTION PERM) (:REWRITE PERM-DEL) (:REWRITE PERM-MEM) (:REWRITE PERM-SYMMETRIC) (:TYPE-PRESCRIPTION MEM) (:TYPE-PRESCRIPTION PERM)) Warnings: None Time: 0.02 seconds (prove: 0.02, print: 0.01, other: 0.00) PERM-TRANSITIVE ACL2 !>>(DEFEQUIV PERM) ACL2 Warning [Equiv] in ( DEFTHM PERM-IS-AN-EQUIVALENCE ...): Any lemma about (PERM X Y), proved before PERM is marked as an equivalence relation, is stored so as to rewrite (PERM X Y) to T. After PERM is known to be an equivalence relation, such a rule would rewrite the left-hand side to the right-hand side, preserving PERM. You have previously proved one possibly problematic rule about PERM, namely PERM-DEL. After PERM is marked as an equivalence relation you should reconsider this problematic rule. If the rule is merely in support of establishing that PERM is an equivalence relation, it may be appropriate to disable it permanently hereafter. If the rule is now intended to rewrite left to right, you must prove the lemma again after PERM is known to be an equivalence relation. Subgoal 3 Subgoal 2 Subgoal 1 Q.E.D. Summary Form: ( DEFTHM PERM-IS-AN-EQUIVALENCE ...) Rules: ((:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER) (:REWRITE PERM-REFLEXIVE) (:REWRITE PERM-SYMMETRIC) (:REWRITE PERM-TRANSITIVE) (:TYPE-PRESCRIPTION PERM)) Warnings: Equiv Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) PERM-IS-AN-EQUIVALENCE ACL2 !>>(IN-THEORY (DISABLE PERM PERM-REFLEXIVE PERM-SYMMETRIC PERM-TRANSITIVE)) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) 2030 ACL2 !>>(DEFCONG PERM PERM (CONS X Y) 2) Q.E.D. Summary Form: ( DEFTHM PERM-IMPLIES-PERM-CONS-2 ...) Rules: ((:DEFINITION DEL) (:DEFINITION MEM) (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE PERM-CONS)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) PERM-IMPLIES-PERM-CONS-2 ACL2 !>>(DEFCONG PERM IFF (MEM X Y) 2) ACL2 Warning [Equiv] in ( DEFTHM PERM-IMPLIES-IFF-MEM-2 ...): The :CONGRUENCE rule PERM-IMPLIES-IFF-MEM-2 can be strengthened by replacing the second equivalence relation, IFF, by EQUAL. See :DOC congruence, in particular (near the end) the Remark on Replacing IFF by EQUAL. Goal' Goal'' Q.E.D. Summary Form: ( DEFTHM PERM-IMPLIES-IFF-MEM-2 ...) Rules: ((:DEFINITION IFF) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE PERM-MEM) (:TYPE-PRESCRIPTION MEM)) Warnings: Equiv Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) PERM-IMPLIES-IFF-MEM-2 ACL2 !>>(DEFTHM ATOM-PERM (IMPLIES (NOT (CONSP X)) (PERM X NIL)) :RULE-CLASSES :FORWARD-CHAINING :HINTS (("Goal" :IN-THEORY (ENABLE PERM)))) ACL2 Observation in ( DEFTHM ATOM-PERM ...): The :TRIGGER- TERMS for the :FORWARD-CHAINING rule ATOM-PERM will consist of the list containing (CONSP X). Q.E.D. Summary Form: ( DEFTHM ATOM-PERM ...) Rules: ((:DEFINITION NOT) (:DEFINITION PERM) (:EXECUTABLE-COUNTERPART CONSP)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) ATOM-PERM ACL2 !>>(DEFTHM INSERT-IS-CONS (PERM (INSERT A X) (CONS A X))) ACL2 Warning [Double-rewrite] in ( DEFTHM INSERT-IS-CONS ...): In a :REWRITE rule generated from INSERT-IS-CONS, equivalence relation PERM is maintained at one problematic occurrence of variable X in the right-hand side, but not at any binding occurrence of X. Consider replacing that occurrence of X in the right-hand side with (DOUBLE-REWRITE X). See :doc double-rewrite for more information on this issue. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (INSERT A X). This suggestion was produced using the :induction rule INSERT. If we let (:P A X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (NOT (LT A (CAR X))) (:P A (CDR X))) (:P A X)) (IMPLIES (AND (NOT (ATOM X)) (LT A (CAR X))) (:P A X)) (IMPLIES (ATOM X) (:P A X))). This induction is justified by the same argument used to admit INSERT. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3.2 Subgoal *1/3.1 Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM INSERT-IS-CONS ...) Rules: ((:CONGRUENCE PERM-IMPLIES-IFF-MEM-2) (:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION ATOM) (:DEFINITION DEL) (:DEFINITION INSERT) (:DEFINITION MEM) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART PERM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ATOM-PERM) (:INDUCTION INSERT) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR) (:REWRITE PERM-CONS) (:REWRITE PERM-MEM)) Warnings: Double-rewrite Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) INSERT-IS-CONS ACL2 !>>(DEFTHM INSERT-SORT-IS-ID (PERM (INSERT-SORT X) X)) ACL2 Warning [Double-rewrite] in ( DEFTHM INSERT-SORT-IS- ID ...): In a :REWRITE rule generated from INSERT-SORT- IS-ID, equivalence relation PERM is maintained at one problematic occurrence of variable X in the right-hand side, but not at any binding occurrence of X. Consider replacing that occurrence of X in the right-hand side with (DOUBLE-REWRITE X). See :doc double-rewrite for more information on this issue. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (INSERT-SORT X). This suggestion was produced using the :induction rule INSERT-SORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ATOM X)) (:P (CDR X))) (:P X)) (IMPLIES (ATOM X) (:P X))). This induction is justified by the same argument used to admit INSERT-SORT. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM INSERT-SORT-IS-ID ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION ATOM) (:DEFINITION INSERT-SORT) (:DEFINITION NOT) (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE) (:EXECUTABLE-COUNTERPART PERM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ATOM-PERM) (:INDUCTION INSERT-SORT) (:REWRITE CONS-CAR-CDR) (:REWRITE INSERT-IS-CONS)) Warnings: Double-rewrite Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) INSERT-SORT-IS-ID ACL2 !>>(DEFCONG PERM PERM (APP X Y) 2) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (APP X Y-EQUIV), but modified to accommodate (APP X Y). These suggestions were produced using the :induction rule APP. If we let (:P X Y Y-EQUIV) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y Y-EQUIV)) (IMPLIES (AND (CONSP X) (:P (CDR X) Y Y-EQUIV)) (:P X Y Y-EQUIV))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM PERM-IMPLIES-PERM-APP-2 ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION APP) (:DEFINITION DEL) (:DEFINITION MEM) (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE PERM-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) PERM-IMPLIES-PERM-APP-2 ACL2 !>>(DEFTHM APP-CONS (PERM (APP A (CONS B C)) (CONS B (APP A C)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. Subsumption reduces that number to one. We will induct according to a scheme suggested by (APP A C). This suggestion was produced using the :induction rule APP. If we let (:P A B C) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP A)) (:P A B C)) (IMPLIES (AND (CONSP A) (:P (CDR A) B C)) (:P A B C))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1''' Subgoal *1/1'4' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM APP-CONS ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION APP) (:DEFINITION DEL) (:DEFINITION MEM) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE PERM-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) APP-CONS ACL2 !>>(DEFTHM APP-COMMUTES (PERM (APP A B) (APP B A))) ACL2 Warning [Double-rewrite] in ( DEFTHM APP-COMMUTES ...): In a :REWRITE rule generated from APP-COMMUTES, equivalence relation PERM is maintained at one problematic occurrence of variable A in the right-hand side, but not at any binding occurrence of A. Consider replacing that occurrence of A in the right-hand side with (DOUBLE-REWRITE A). See :doc double-rewrite for more information on this issue. ACL2 Warning [Subsume] in ( DEFTHM APP-COMMUTES ...): A newly proposed :REWRITE rule generated from APP-COMMUTES probably subsumes the previously added :REWRITE rule APP- CONS, in the sense that the new rule will now probably be applied whenever the old rule would have been. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. We will choose arbitrarily among these. We will induct according to a scheme suggested by (APP A B). This suggestion was produced using the :induction rule APP. If we let (:P A B) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP A)) (:P A B)) (IMPLIES (AND (CONSP A) (:P (CDR A) B)) (:P A B))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2' (IMPLIES (NOT (CONSP A)) (PERM B (APP B NIL))) *1.1 (Subgoal *1/2'') is pushed for proof by induction. ]) Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1''' So we now return to *1.1, which is (PERM B (APP B NIL)). Subgoal *1.1/2 Subgoal *1.1/1 *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/2' and Goal are COMPLETED! Q.E.D. Summary Form: ( DEFTHM APP-COMMUTES ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-APP-2) (:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION APP) (:DEFINITION NOT) (:ELIM CAR-CDR-ELIM) (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE) (:EXECUTABLE-COUNTERPART PERM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ATOM-PERM) (:INDUCTION APP) (:REWRITE APP-CONS) (:REWRITE CONS-CAR-CDR)) Warnings: Subsume and Double-rewrite Time: 0.01 seconds (prove: 0.01, print: 0.01, other: 0.00) APP-COMMUTES ACL2 !>>(DEFCONG PERM PERM (APP X Y) 1 :HINTS (("Goal" :INDUCT (APP Y X)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. 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 (APP Y X). This suggestion was produced using the :induction rule APP. If we let (:P X X-EQUIV Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP Y)) (:P X X-EQUIV Y)) (IMPLIES (AND (CONSP Y) (:P X X-EQUIV (CDR Y))) (:P X X-EQUIV Y))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' Subgoal *1/1'' Subgoal *1/1''' Subgoal *1/1'4' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM PERM-IMPLIES-PERM-APP-1 ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-APP-2) (:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION APP) (:DEFINITION DEL) (:DEFINITION MEM) (:DEFINITION NOT) (:ELIM CAR-CDR-ELIM) (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ATOM-PERM) (:INDUCTION APP) (:REWRITE APP-COMMUTES) (:REWRITE APP-CONS) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE PERM-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) PERM-IMPLIES-PERM-APP-1 ACL2 !>>(DEFTHM REV-IS-ID (PERM (REV X) X)) ACL2 Warning [Double-rewrite] in ( DEFTHM REV-IS-ID ...): In a :REWRITE rule generated from REV-IS-ID, equivalence relation PERM is maintained at one problematic occurrence of variable X in the right-hand side, but not at any binding occurrence of X. Consider replacing that occurrence of X in the right-hand side with (DOUBLE-REWRITE X). See :doc double-rewrite for more information on this issue. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rule REV. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X)) (IMPLIES (AND (CONSP X) (:P (CDR X))) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM REV-IS-ID ...) Rules: ((:CONGRUENCE PERM-IMPLIES-PERM-APP-1) (:CONGRUENCE PERM-IMPLIES-PERM-CONS-2) (:DEFINITION APP) (:DEFINITION REV) (:EQUIVALENCE PERM-IS-AN-EQUIVALENCE) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART PERM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ATOM-PERM) (:INDUCTION REV) (:REWRITE APP-COMMUTES) (:REWRITE APP-CONS) (:REWRITE CONS-CAR-CDR)) Warnings: Double-rewrite Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) REV-IS-ID ACL2 !>>(DEFUN == (X Y) (IF (CONSP X) (IF (CONSP Y) (AND (EQUAL (CAR X) (CAR Y)) (== (CDR X) (CDR Y))) NIL) (NOT (CONSP Y)))) The admission of == is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of == is described by the theorem (OR (EQUAL (== X Y) T) (EQUAL (== X Y) NIL)). Summary Form: ( DEFUN == ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) == ACL2 !>>(DEFTHM ==-SYMMETRIC (== X X)) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (== X X). This suggestion was produced using the :induction rule ==. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X)) (IMPLIES (AND (CONSP X) (CONSP X) (NOT (EQUAL (CAR X) (CAR X)))) (:P X)) (IMPLIES (AND (CONSP X) (CONSP X) (EQUAL (CAR X) (CAR X)) (:P (CDR X))) (:P X))). This induction is justified by the same argument used to admit ==. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of ==-SYMMETRIC depends upon the :type-prescription rule ==. Summary Form: ( DEFTHM ==-SYMMETRIC ...) Rules: ((:DEFINITION ==) (:DEFINITION NOT) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION ==) (:TYPE-PRESCRIPTION ==)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) ==-SYMMETRIC ACL2 !>>(DEFTHM ==-REFLEXIVE (IMPLIES (== X Y) (== Y X))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (== Y X). This suggestion was produced using the :induction rule ==. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP Y)) (:P X Y)) (IMPLIES (AND (CONSP Y) (NOT (CONSP X))) (:P X Y)) (IMPLIES (AND (CONSP Y) (CONSP X) (NOT (EQUAL (CAR Y) (CAR X)))) (:P X Y)) (IMPLIES (AND (CONSP Y) (CONSP X) (EQUAL (CAR Y) (CAR X)) (:P (CDR X) (CDR Y))) (:P X Y))). This induction is justified by the same argument used to admit ==. Note, however, that the unmeasured variable X is being instantiated. When applied to the goal at hand the above induction scheme produces five nontautological subgoals. Subgoal *1/5 Subgoal *1/4 Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of ==-REFLEXIVE depends upon the :type-prescription rule ==. Summary Form: ( DEFTHM ==-REFLEXIVE ...) Rules: ((:DEFINITION ==) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION ==) (:TYPE-PRESCRIPTION ==)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) ==-REFLEXIVE ACL2 !>>(DEFEQUIV ==) Subgoal 3 Subgoal 2 Subgoal 1 ([ A key checkpoint: Subgoal 1 (IMPLIES (AND (== X Y) (== Y Z)) (== X Z)) *1 (Subgoal 1) is pushed for proof by induction. ]) Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (== X Z), but modified to accommodate (== Y Z) and (== X Y). These suggestions were produced using the :induction rule ==. If we let (:P X Y Z) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y Z)) (IMPLIES (AND (CONSP X) (NOT (CONSP Z))) (:P X Y Z)) (IMPLIES (AND (CONSP X) (CONSP Z) (NOT (EQUAL (CAR X) (CAR Z)))) (:P X Y Z)) (IMPLIES (AND (CONSP X) (CONSP Z) (EQUAL (CAR X) (CAR Z)) (:P (CDR X) (CDR Y) (CDR Z))) (:P X Y Z))). This induction is justified by the same argument used to admit ==. Note, however, that the unmeasured variables Y and Z are being instantiated. When applied to the goal at hand the above induction scheme produces six nontautological subgoals. Subgoal *1/6 Subgoal *1/5 Subgoal *1/4 Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Subgoal 1 is COMPLETED! Q.E.D. Summary Form: ( DEFTHM ==-IS-AN-EQUIVALENCE ...) Rules: ((:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER) (:DEFINITION ==) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION ==) (:REWRITE ==-REFLEXIVE) (:REWRITE ==-SYMMETRIC) (:TYPE-PRESCRIPTION ==)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00) ==-IS-AN-EQUIVALENCE ACL2 !>>(IN-THEORY (DISABLE ==-SYMMETRIC ==-REFLEXIVE)) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 2045 ACL2 !>>(DEFCONG == == (CONS X Y) 2) Q.E.D. Summary Form: ( DEFTHM ==-IMPLIES-==-CONS-2 ...) Rules: ((:DEFINITION ==) (:EQUIVALENCE ==-IS-AN-EQUIVALENCE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ==-IMPLIES-==-CONS-2 ACL2 !>>(DEFCONG == IFF (CONSP X) 1) ACL2 Warning [Equiv] in ( DEFTHM ==-IMPLIES-IFF-CONSP-1 ...): The :CONGRUENCE rule ==-IMPLIES-IFF-CONSP-1 can be strengthened by replacing the second equivalence relation, IFF, by EQUAL. See :DOC congruence, in particular (near the end) the Remark on Replacing IFF by EQUAL. Goal' Subgoal 2 Subgoal 1 Q.E.D. Summary Form: ( DEFTHM ==-IMPLIES-IFF-CONSP-1 ...) Rules: ((:DEFINITION ==) (:DEFINITION IFF)) Warnings: Equiv Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ==-IMPLIES-IFF-CONSP-1 ACL2 !>>(DEFCONG == == (APP X Y) 2) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into two derived induction schemes. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (APP X Y-EQUIV), but modified to accommodate (APP X Y). These suggestions were produced using the :induction rule APP. If we let (:P X Y Y-EQUIV) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y Y-EQUIV)) (IMPLIES (AND (CONSP X) (:P (CDR X) Y Y-EQUIV)) (:P X Y Y-EQUIV))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM ==-IMPLIES-==-APP-2 ...) Rules: ((:CONGRUENCE ==-IMPLIES-==-CONS-2) (:DEFINITION ==) (:DEFINITION APP) (:EQUIVALENCE ==-IS-AN-EQUIVALENCE) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) ==-IMPLIES-==-APP-2 ACL2 !>>(DEFCONG == == (APP X Y) 1) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (APP X-EQUIV Y), but modified to accommodate (APP X Y) and (== X X-EQUIV). These suggestions were produced using the :induction rules == and APP. If we let (:P X X-EQUIV Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X-EQUIV)) (:P X X-EQUIV Y)) (IMPLIES (AND (CONSP X-EQUIV) (:P (CDR X) (CDR X-EQUIV) Y)) (:P X X-EQUIV Y))). This induction is justified by the same argument used to admit APP. Note, however, that the unmeasured variable X is being instantiated. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM ==-IMPLIES-==-APP-1 ...) Rules: ((:CONGRUENCE ==-IMPLIES-==-CONS-2) (:CONGRUENCE ==-IMPLIES-IFF-CONSP-1) (:DEFINITION ==) (:DEFINITION APP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION ==) (:INDUCTION APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) ==-IMPLIES-==-APP-1 ACL2 !>>(DEFTHM REV-REV-AGAIN (== (REV (REV X)) X)) ACL2 Warning [Double-rewrite] in ( DEFTHM REV-REV-AGAIN ...): In a :REWRITE rule generated from REV-REV-AGAIN, equivalence relation == is maintained at one problematic occurrence of variable X in the right-hand side, but not at any binding occurrence of X. Consider replacing that occurrence of X in the right-hand side with (DOUBLE-REWRITE X). See :doc double-rewrite for more information on this issue. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (REV X). This suggestion was produced using the :induction rule REV. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X)) (IMPLIES (AND (CONSP X) (:P (CDR X))) (:P X))). This induction is justified by the same argument used to admit REV. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM REV-REV-AGAIN ...) Rules: ((:CONGRUENCE ==-IMPLIES-==-APP-2) (:DEFINITION ==) (:DEFINITION APP) (:DEFINITION REV) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART REV) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION REV) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR) (:REWRITE REV-APP)) Warnings: Double-rewrite Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) REV-REV-AGAIN ACL2 !>>(DEFUN ENDS-IN-A-0 (X) (DECLARE (XARGS :GUARD T)) (IF (CONSP X) (ENDS-IN-A-0 (CDR X)) (EQUAL X 0))) The admission of ENDS-IN-A-0 is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of ENDS-IN-A-0 is described by the theorem (OR (EQUAL (ENDS-IN-A-0 X) T) (EQUAL (ENDS-IN-A-0 X) NIL)). We used primitive type reasoning. Computing the guard conjecture for ENDS-IN-A-0.... The guard conjecture for ENDS-IN-A-0 is trivial to prove. ENDS-IN-A-0 is compliant with Common Lisp. Summary Form: ( DEFUN ENDS-IN-A-0 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ENDS-IN-A-0 ACL2 !>>(DEFUN APP0 (X Y) (DECLARE (XARGS :GUARD (ENDS-IN-A-0 X))) (IF (ENDS-IN-A-0 X) (IF (EQUAL X 0) Y (CONS (CAR X) (APP0 (CDR X) Y))) 'DEFAULT)) For the admission of APP0 we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0))) (O< (ACL2-COUNT (CDR X)) (ACL2-COUNT X))). Goal' Goal'' Goal''' Q.E.D. That completes the proof of the measure theorem for APP0. Thus, we admit this function under the principle of definition. We observe that the type of APP0 is described by the theorem (OR (OR (CONSP (APP0 X Y)) (AND (SYMBOLP (APP0 X Y)) (NOT (EQUAL (APP0 X Y) T)) (NOT (EQUAL (APP0 X Y) NIL)))) (EQUAL (APP0 X Y) Y)). We used primitive type reasoning. Computing the guard conjecture for APP0.... The non-trivial part of the guard conjecture for APP0 is Goal (AND (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0))) (ENDS-IN-A-0 (CDR X))) (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0)) (NOT (CONSP X))) (EQUAL X NIL))). Subgoal 2 Subgoal 1 Q.E.D. That completes the proof of the guard theorem for APP0. APP0 is compliant with Common Lisp. Summary Form: ( DEFUN APP0 ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION ENDS-IN-A-0) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01) APP0 ACL2 !>>(DEFUN REV0 (X) (DECLARE (XARGS :GUARD (ENDS-IN-A-0 X))) (IF (ENDS-IN-A-0 X) (IF (EQUAL X 0) 0 (APP0 (REV0 (CDR X)) (CONS (CAR X) 0))) 'DEFAULT)) For the admission of REV0 we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0))) (O< (ACL2-COUNT (CDR X)) (ACL2-COUNT X))). Goal' Goal'' Goal''' Q.E.D. That completes the proof of the measure theorem for REV0. Thus, we admit this function under the principle of definition. We observe that the type of REV0 is described by the theorem (OR (EQUAL (REV0 X) 0) (CONSP (REV0 X)) (AND (SYMBOLP (REV0 X)) (NOT (EQUAL (REV0 X) T)) (NOT (EQUAL (REV0 X) NIL)))). We used primitive type reasoning and the :type-prescription rule APP0. Computing the guard conjecture for REV0.... The non-trivial part of the guard conjecture for REV0 is Goal (AND (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0))) (ENDS-IN-A-0 (CDR X))) (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0))) (ENDS-IN-A-0 (REV0 (CDR X)))) (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0)) (NOT (CONSP X))) (EQUAL X NIL))). Subgoal 3 Subgoal 2 Subgoal 2' Subgoal 2'' Subgoal 2''' ([ A key checkpoint: Subgoal 2' (IMPLIES (AND (CONSP X) (ENDS-IN-A-0 (CDR X))) (ENDS-IN-A-0 (REV0 (CDR X)))) *1 (Subgoal 2''') is pushed for proof by induction: (IMPLIES (ENDS-IN-A-0 X2) (ENDS-IN-A-0 (REV0 X2))). ]) Subgoal 1 Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (REV0 X2). This suggestion was produced using the :induction rules ENDS-IN-A-0 and REV0. If we let (:P X2) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (ENDS-IN-A-0 X2)) (:P X2)) (IMPLIES (AND (ENDS-IN-A-0 X2) (NOT (EQUAL X2 0)) (:P (CDR X2))) (:P X2)) (IMPLIES (AND (ENDS-IN-A-0 X2) (EQUAL X2 0)) (:P X2))). This induction is justified by the same argument used to admit REV0. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' Subgoal *1/3'5' ([ A key checkpoint while proving *1 (descended from Subgoal 2'): Subgoal *1/3' (IMPLIES (AND (CONSP X2) (ENDS-IN-A-0 (CDR X2)) (ENDS-IN-A-0 (REV0 (CDR X2)))) (ENDS-IN-A-0 (APP0 (REV0 (CDR X2)) (CONS (CAR X2) 0)))) *1.1 (Subgoal *1/3'5') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/1 So we now return to *1.1, which is (IMPLIES (ENDS-IN-A-0 R0) (ENDS-IN-A-0 (APP0 R0 (CONS X3 0)))). Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/1 *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/3' and Subgoal 2' are COMPLETED! Q.E.D. That completes the proof of the guard theorem for REV0. REV0 is compliant with Common Lisp. Summary Form: ( DEFUN REV0 ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION APP0) (:DEFINITION ENDS-IN-A-0) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION REV0) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ENDS-IN-A-0) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART REV0) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP0) (:INDUCTION ENDS-IN-A-0) (:INDUCTION REV0) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION APP0) (:TYPE-PRESCRIPTION ENDS-IN-A-0)) Warnings: None Time: 0.05 seconds (prove: 0.03, print: 0.01, other: 0.01) REV0 ACL2 !>>(DEFTHM APP0-RIGHT-ID (IMPLIES (FORCE (ENDS-IN-A-0 X)) (EQUAL (APP0 X 0) X))) Goal' ([ A key checkpoint: Goal' (IMPLIES (ENDS-IN-A-0 X) (EQUAL (APP0 X 0) X)) *1 (Goal') is pushed for proof by induction. ]) Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (APP0 X '0). This suggestion was produced using the :induction rules APP0 and ENDS-IN-A-0. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (ENDS-IN-A-0 X)) (:P X)) (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0)) (:P (CDR X))) (:P X)) (IMPLIES (AND (ENDS-IN-A-0 X) (EQUAL X 0)) (:P X))). This induction is justified by the same argument used to admit APP0. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal' is COMPLETED! Q.E.D. Summary Form: ( DEFTHM APP0-RIGHT-ID ...) Rules: ((:DEFINITION APP0) (:DEFINITION ENDS-IN-A-0) (:DEFINITION FORCE) (:EXECUTABLE-COUNTERPART APP0) (:EXECUTABLE-COUNTERPART ENDS-IN-A-0) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP0) (:INDUCTION ENDS-IN-A-0) (:REWRITE CONS-CAR-CDR) (:TYPE-PRESCRIPTION ENDS-IN-A-0)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) APP0-RIGHT-ID ACL2 !>>(DEFUN ENDS-IN-A-ZERO (X) (ENDS-IN-A-0 X)) Since ENDS-IN-A-ZERO is non-recursive, its admission is trivial. We observe that the type of ENDS-IN-A-ZERO is described by the theorem (OR (EQUAL (ENDS-IN-A-ZERO X) T) (EQUAL (ENDS-IN-A-ZERO X) NIL)). We used the :type-prescription rule ENDS-IN-A-0. Summary Form: ( DEFUN ENDS-IN-A-ZERO ...) Rules: ((:TYPE-PRESCRIPTION ENDS-IN-A-0)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ENDS-IN-A-ZERO ACL2 !>>(DEFTHM ENDS-IN-A-ZERO-APP0 (IMPLIES (FORCE (ENDS-IN-A-ZERO X)) (ENDS-IN-A-0 (APP0 X (CONS Y 0))))) Goal' ([ A key checkpoint: Goal' (IMPLIES (ENDS-IN-A-0 X) (ENDS-IN-A-0 (APP0 X (CONS Y 0)))) *1 (Goal') is pushed for proof by induction. ]) Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (APP0 X (CONS Y '0)). This suggestion was produced using the :induction rules APP0 and ENDS-IN-A-0. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (ENDS-IN-A-0 X)) (:P X Y)) (IMPLIES (AND (ENDS-IN-A-0 X) (NOT (EQUAL X 0)) (:P (CDR X) Y)) (:P X Y)) (IMPLIES (AND (ENDS-IN-A-0 X) (EQUAL X 0)) (:P X Y))). This induction is justified by the same argument used to admit APP0. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal' is COMPLETED! Q.E.D. The storage of ENDS-IN-A-ZERO-APP0 depends upon the :type- prescription rule ENDS-IN-A-0. Summary Form: ( DEFTHM ENDS-IN-A-ZERO-APP0 ...) Rules: ((:DEFINITION APP0) (:DEFINITION ENDS-IN-A-0) (:DEFINITION ENDS-IN-A-ZERO) (:DEFINITION FORCE) (:EXECUTABLE-COUNTERPART ENDS-IN-A-0) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP0) (:INDUCTION ENDS-IN-A-0) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION ENDS-IN-A-0)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) ENDS-IN-A-ZERO-APP0 ACL2 !>>(IN-THEORY (DISABLE ENDS-IN-A-ZERO)) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 2066 ACL2 !>>(DEFTHM FORCE-TEST (AND (IMPLIES (ENDS-IN-A-0 X) (EQUAL (APP0 (REV0 X) 0) (REV0 X))) (IMPLIES (ENDS-IN-A-0 Y) (EQUAL (APP0 (REV0 Y) 0) (REV0 Y))) (IMPLIES (ENDS-IN-A-0 Z) (EQUAL (APP0 (REV0 Z) 0) (REV0 Z)))) :HINTS (("[2]Goal" :IN-THEORY (ENABLE ENDS-IN-A-ZERO)))) Subgoal 3 Forcing Round 1 is pending (caused first by Subgoal 3). Subgoal 2 Subgoal 1 q.e.d. (given three forced hypotheses) Modulo the following three forced goals, that completes the proof of the input Goal. See :DOC forcing-round. [1]Subgoal 3, below, will focus on (ENDS-IN-A-0 (REV0 Z)), which was forced in Subgoal 1 by applying (:REWRITE APP0-RIGHT-ID) to (APP0 (REV0 Z) 0). [1]Subgoal 2, below, will focus on (ENDS-IN-A-0 (REV0 Y)), which was forced in Subgoal 2 by applying (:REWRITE APP0-RIGHT-ID) to (APP0 (REV0 Y) 0). [1]Subgoal 1, below, will focus on (ENDS-IN-A-0 (REV0 X)), which was forced in Subgoal 3 by applying (:REWRITE APP0-RIGHT-ID) to (APP0 (REV0 X) 0). We now undertake Forcing Round 1. [1]Subgoal 3 ([ A key checkpoint: [1]Subgoal 3 (IMPLIES (ENDS-IN-A-0 Z) (ENDS-IN-A-0 (REV0 Z))) [1]*1 ([1]Subgoal 3) is pushed for proof by induction. ]) [1]Subgoal 2 ([ A key checkpoint: [1]Subgoal 2 (IMPLIES (ENDS-IN-A-0 Y) (ENDS-IN-A-0 (REV0 Y))) [1]*2 ([1]Subgoal 2) is pushed for proof by induction. ]) [1]Subgoal 1 ([ A key checkpoint: [1]Subgoal 1 (IMPLIES (ENDS-IN-A-0 X) (ENDS-IN-A-0 (REV0 X))) [1]*3 ([1]Subgoal 1) is pushed for proof by induction. ]) But the formula above is subsumed by [1]*2, which we'll try to prove later. We therefore regard [1]*3 as proved (pending the proof of the more general [1]*2). [1]Subgoal 1 COMPLETED! But the formula above is subsumed by [1]*1, which we'll try to prove later. We therefore regard [1]*2 as proved (pending the proof of the more general [1]*1). [1]Subgoal 2 COMPLETED! Perhaps we can prove [1]*1 by induction. Two induction schemes are suggested by this conjecture. These merge into one derived induction scheme. We will induct according to a scheme suggested by (REV0 Z). This suggestion was produced using the :induction rules ENDS-IN-A-0 and REV0. If we let (:P Z) denote [1]*1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (ENDS-IN-A-0 Z)) (:P Z)) (IMPLIES (AND (ENDS-IN-A-0 Z) (NOT (EQUAL Z 0)) (:P (CDR Z))) (:P Z)) (IMPLIES (AND (ENDS-IN-A-0 Z) (EQUAL Z 0)) (:P Z))). This induction is justified by the same argument used to admit REV0. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. [1]Subgoal *1/3 Forcing Round 2 is pending (caused first by [1]Subgoal *1/3). [1]Subgoal *1/2 [1]Subgoal *1/1 [1]*1 is COMPLETED! Thus key checkpoint [1]Subgoal 3 is COMPLETED! q.e.d. (given one forced hypothesis) Modulo the following newly forced goal, that completes Forcing Round 1. See :DOC forcing-round. [2]Goal, below, will focus on (ENDS-IN-A-ZERO (REV0 (CDR Z))), which was forced in [1]Subgoal *1/3 by applying (:REWRITE ENDS-IN-A-ZERO-APP0) to (ENDS-IN-A-0 (APP0 (REV0 (CDR Z)) (CONS (CAR Z) 0))). We now undertake Forcing Round 2. [2]Goal Q.E.D. Summary Form: ( DEFTHM FORCE-TEST ...) Rules: ((:DEFINITION ENDS-IN-A-0) (:DEFINITION ENDS-IN-A-ZERO) (:DEFINITION NOT) (:DEFINITION REV0) (:EXECUTABLE-COUNTERPART ENDS-IN-A-0) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART REV0) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION ENDS-IN-A-0) (:INDUCTION REV0) (:REWRITE APP0-RIGHT-ID) (:REWRITE ENDS-IN-A-ZERO-APP0) (:TYPE-PRESCRIPTION ENDS-IN-A-0)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00) FORCE-TEST ACL2 !>>(DEFUN PROPER-CONS-NEST-P (X) (DECLARE (XARGS :GUARD (PSEUDO-TERMP X))) (COND ((SYMBOLP X) NIL) ((FQUOTEP X) (TRUE-LISTP (CADR X))) ((EQ (FFN-SYMB X) 'CONS) (PROPER-CONS-NEST-P (FARGN X 2))) (T NIL))) For the admission of PROPER-CONS-NEST-P we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (NOT (SYMBOLP X)) (NOT (EQ 'QUOTE (CAR X))) (EQ (CAR X) 'CONS)) (O< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). Goal' Goal'' Subgoal 4 Subgoal 3 Subgoal 3' Subgoal 3'' Subgoal 2 Subgoal 2' Subgoal 2'' Subgoal 1 Subgoal 1' Subgoal 1'' Q.E.D. That completes the proof of the measure theorem for PROPER- CONS-NEST-P. Thus, we admit this function under the principle of definition. We observe that the type of PROPER-CONS- NEST-P is described by the theorem (OR (EQUAL (PROPER-CONS-NEST-P X) T) (EQUAL (PROPER-CONS-NEST-P X) NIL)). Computing the guard conjecture for PROPER-CONS-NEST-P.... The non-trivial part of the guard conjecture for PROPER- CONS-NEST-P is Goal (AND (IMPLIES (AND (PSEUDO-TERMP X) (NOT (SYMBOLP X)) (NOT (CONSP X))) (EQUAL X NIL)) (IMPLIES (AND (PSEUDO-TERMP X) (NOT (SYMBOLP X)) (EQ (CAR X) 'CONS) (NOT (CONSP (CDR X)))) (EQUAL (CDR X) NIL)) (IMPLIES (AND (PSEUDO-TERMP X) (NOT (SYMBOLP X)) (NOT (EQ 'QUOTE (CAR X))) (EQ (CAR X) 'CONS)) (PSEUDO-TERMP (CADDR X))) (IMPLIES (AND (PSEUDO-TERMP X) (NOT (SYMBOLP X)) (NOT (EQ 'QUOTE (CAR X))) (EQ (CAR X) 'CONS) (NOT (CONSP (CDDR X)))) (EQUAL (CDDR X) NIL)) (IMPLIES (AND (PSEUDO-TERMP X) (NOT (SYMBOLP X)) (EQ 'QUOTE (CAR X)) (NOT (CONSP (CDR X)))) (EQUAL (CDR X) NIL))). Subgoal 5 Subgoal 4 Subgoal 3 Subgoal 3' Subgoal 3'' Subgoal 3.2 Subgoal 3.2' Subgoal 3.1 Subgoal 3.1' Subgoal 2 Subgoal 1 Q.E.D. That completes the proof of the guard theorem for PROPER- CONS-NEST-P. PROPER-CONS-NEST-P is compliant with Common Lisp. Summary Form: ( DEFUN PROPER-CONS-NEST-P ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION PSEUDO-TERM-LISTP) (:DEFINITION PSEUDO-TERMP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART PSEUDO-TERM-LISTP) (:EXECUTABLE-COUNTERPART PSEUDO-TERMP) (:EXECUTABLE-COUNTERPART SYMBOLP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-CAR) (:REWRITE DEFAULT-CDR) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION PSEUDO-TERM-LISTP)) Warnings: None Time: 0.05 seconds (prove: 0.03, print: 0.01, other: 0.01) PROPER-CONS-NEST-P ACL2 !>>(DEFTHM ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR-TEST (IMPLIES (AND (ORDERED-SYMBOL-ALISTP L) (SYMBOLP KEY) (ASSOC-EQ KEY L)) (ORDERED-SYMBOL-ALISTP (REMOVE-FIRST-PAIR KEY L))) :HINTS (("Goal" :IN-THEORY (DISABLE ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR)))) ACL2 Warning [Subsume] in ( DEFTHM ORDERED-SYMBOL-ALISTP- REMOVE-FIRST-PAIR-TEST ...): A newly proposed :REWRITE rule generated from ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR- TEST probably subsumes the previously added :REWRITE rule ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR, in the sense that the new rule will now probably be applied whenever the old rule would have been. ACL2 Warning [Subsume] in ( DEFTHM ORDERED-SYMBOL-ALISTP- REMOVE-FIRST-PAIR-TEST ...): The previously added rule ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR subsumes a newly proposed :REWRITE rule generated from ORDERED-SYMBOL-ALISTP- REMOVE-FIRST-PAIR-TEST, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. These merge into one derived induction scheme. We will induct according to a scheme suggested by (REMOVE-FIRST-PAIR KEY L). This suggestion was produced using the :induction rules ASSOC-EQ, ORDERED-SYMBOL-ALISTP and REMOVE-FIRST-PAIR. If we let (:P KEY L) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP L)) (NOT (EQ KEY (CAAR L))) (:P KEY (CDR L))) (:P KEY L)) (IMPLIES (AND (NOT (ENDP L)) (EQ KEY (CAAR L))) (:P KEY L)) (IMPLIES (ENDP L) (:P KEY L))). This induction is justified by the same argument used to admit REMOVE-FIRST-PAIR. When applied to the goal at hand the above induction scheme produces five nontautological subgoals. Subgoal *1/5 Subgoal *1/5' Subgoal *1/5.6 Subgoal *1/5.5 Subgoal *1/5.4 Subgoal *1/5.3 Subgoal *1/5.2 Subgoal *1/5.2.2 Subgoal *1/5.2.1 Subgoal *1/5.2.1.2 Subgoal *1/5.2.1.1 Subgoal *1/5.1 Subgoal *1/4 Subgoal *1/4' Subgoal *1/3 Subgoal *1/3' Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/1 Subgoal *1/1' *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. The storage of ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR-TEST depends upon the :type-prescription rule ORDERED-SYMBOL- ALISTP. Summary Form: ( DEFTHM ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR- TEST ...) Rules: ((:DEFINITION ASSOC-EQ) (:DEFINITION ENDP) (:DEFINITION EQ) (:DEFINITION NOT) (:DEFINITION ORDERED-SYMBOL-ALISTP) (:DEFINITION REMOVE-FIRST-PAIR) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART ORDERED-SYMBOL-ALISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP) (:FORWARD-CHAINING EQLABLE-ALISTP-FORWARD-TO-ALISTP) (:FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP) (:FORWARD-CHAINING SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP) (:INDUCTION ASSOC-EQ) (:INDUCTION ORDERED-SYMBOL-ALISTP) (:INDUCTION REMOVE-FIRST-PAIR) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE SYMBOL-<-ASYMMETRIC) (:REWRITE SYMBOL-<-IRREFLEXIVE) (:REWRITE SYMBOL-<-TRANSITIVE) (:REWRITE SYMBOL-<-TRICHOTOMY) (:TYPE-PRESCRIPTION ALISTP) (:TYPE-PRESCRIPTION EQLABLE-ALISTP) (:TYPE-PRESCRIPTION ORDERED-SYMBOL-ALISTP) (:TYPE-PRESCRIPTION SYMBOL-<) (:TYPE-PRESCRIPTION SYMBOL-ALISTP)) Warnings: Subsume Time: 0.48 seconds (prove: 0.46, print: 0.01, other: 0.01) ORDERED-SYMBOL-ALISTP-REMOVE-FIRST-PAIR-TEST ACL2 !>>Bye. :EOF ACL2 !>(show-accumulated-persistence) Accumulated Persistence (15824 :tries useful, 7734 :tries not useful) :frames :tries :ratio rune -------------------------------- 2406 2406 ( 1.00) (:TYPE-PRESCRIPTION PERM) 2246 2246 [useful] 160 160 [useless] -------------------------------- 2144 109 ( 19.66) (:DEFINITION PERM) 564 28 [useful] 1580 81 [useless] -------------------------------- 2105 33 ( 63.78) (:DEFINITION ACL2-COUNT) 1520 8 [useful] 585 25 [useless] -------------------------------- 2093 2027 ( 1.03) (:REWRITE DEFAULT-CAR) 1 1 [useful] 2092 2026 [useless] -------------------------------- 1800 1729 ( 1.04) (:REWRITE DEFAULT-CDR) 1 1 [useful] 1799 1728 [useless] -------------------------------- 1550 1550 ( 1.00) (:TYPE-PRESCRIPTION MEM) 1188 1188 [useful] 362 362 [useless] -------------------------------- 1524 220 ( 6.92) (:DEFINITION MEM) 197 47 [useful] 1327 173 [useless] -------------------------------- 1506 1157 ( 1.30) (:TYPE-PRESCRIPTION APP) 965 686 [useful] 541 471 [useless] -------------------------------- 1222 207 ( 5.90) (:DEFINITION DEL) 308 44 [useful] 914 163 [useless] -------------------------------- 1132 30 ( 37.73) (:DEFINITION ORDERED-SYMBOL-ALISTP) 717 18 [useful] 415 12 [useless] -------------------------------- 1005 1005 ( 1.00) (:TYPE-PRESCRIPTION ENDS-IN-A-0) 975 975 [useful] 30 30 [useless] -------------------------------- 979 252 ( 3.88) (:DEFINITION APP) 135 43 [useful] 844 209 [useless] -------------------------------- 976 488 ( 2.00) (:TYPE-PRESCRIPTION TRUE-LIST-LISTP-FORWARD-TO-TRUE-LISTP-ASSOC-EQ) 0 0 [useful] 976 488 [useless] -------------------------------- 959 959 ( 1.00) (:TYPE-PRESCRIPTION ==) 889 889 [useful] 70 70 [useless] -------------------------------- 945 945 ( 1.00) (:TYPE-PRESCRIPTION ORDERED-SYMBOL-ALISTP) 945 945 [useful] 0 0 [useless] -------------------------------- 942 112 ( 8.41) (:REWRITE PERM-SYMMETRIC) 30 6 [useful] 912 106 [useless] -------------------------------- 865 865 ( 1.00) (:TYPE-PRESCRIPTION REV) 611 611 [useful] 254 254 [useless] -------------------------------- 817 817 ( 1.00) (:TYPE-PRESCRIPTION ACL2-COUNT) 522 522 [useful] 295 295 [useless] -------------------------------- 760 90 ( 8.44) (:DEFINITION REV) 184 19 [useful] 576 71 [useless] -------------------------------- 755 755 ( 1.00) (:DEFINITION NOT) 755 755 [useful] 0 0 [useless] -------------------------------- 734 734 ( 1.00) (:TYPE-PRESCRIPTION SYMBOL-<) 454 454 [useful] 280 280 [useless] -------------------------------- 732 488 ( 1.50) (:TYPE-PRESCRIPTION CONSP-ASSOC-EQ) 244 244 [useful] 488 244 [useless] -------------------------------- 723 723 ( 1.00) (:TYPE-PRESCRIPTION ALISTP) 479 479 [useful] 244 244 [useless] -------------------------------- 717 24 ( 29.87) (:REWRITE PERM-CONS) 250 11 [useful] 467 13 [useless] -------------------------------- 650 171 ( 3.80) (:REWRITE SYMBOL-<-TRICHOTOMY) 23 2 [useful] 627 169 [useless] -------------------------------- 567 567 ( 1.00) (:TYPE-PRESCRIPTION SYMBOL-ALISTP) 567 567 [useful] 0 0 [useless] -------------------------------- 523 523 ( 1.00) (:TYPE-PRESCRIPTION EQLABLE-ALISTP) 523 523 [useful] 0 0 [useless] -------------------------------- 492 95 ( 5.17) (:REWRITE SYMBOL-<-ASYMMETRIC) 6 3 [useful] 486 92 [useless] -------------------------------- 488 488 ( 1.00) (:TYPE-PRESCRIPTION TRUE-LIST-LISTP) 0 0 [useful] 488 488 [useless] -------------------------------- 462 211 ( 2.18) (:REWRITE PERM-MEM) 13 6 [useful] 449 205 [useless] -------------------------------- 457 221 ( 2.06) (:REWRITE DEFAULT-+-2) 0 0 [useful] 457 221 [useless] -------------------------------- 400 69 ( 5.79) (:DEFINITION ==) 102 29 [useful] 298 40 [useless] -------------------------------- 373 280 ( 1.33) (:TYPE-PRESCRIPTION REVAPPEND) 129 97 [useful] 244 183 [useless] -------------------------------- 373 129 ( 2.89) (:DEFINITION ENDS-IN-A-0) 58 26 [useful] 315 103 [useless] -------------------------------- 355 10 ( 35.50) (:DEFINITION PSEUDO-TERMP) 45 5 [useful] 310 5 [useless] -------------------------------- 339 23 ( 14.73) (:DEFINITION REV0) 24 2 [useful] 315 21 [useless] -------------------------------- 296 36 ( 8.22) (:DEFINITION APP0) 12 5 [useful] 284 31 [useless] -------------------------------- 294 221 ( 1.33) (:REWRITE DEFAULT-+-1) 0 0 [useful] 294 221 [useless] -------------------------------- 293 36 ( 8.13) (:DEFINITION LENGTH) 0 0 [useful] 293 36 [useless] -------------------------------- 269 169 ( 1.59) (:REWRITE SYMBOL-<-TRANSITIVE) 1 1 [useful] 268 168 [useless] -------------------------------- 258 258 ( 1.00) (:FORWARD-CHAINING ATOM-PERM) 258 258 [useful] 0 0 [useless] -------------------------------- 242 57 ( 4.24) (:REWRITE ==-REFLEXIVE) 17 4 [useful] 225 53 [useless] -------------------------------- 239 239 ( 1.00) (:REWRITE MEM-DEL) 1 1 [useful] 238 238 [useless] -------------------------------- 205 41 ( 5.00) (:DEFINITION LEN) 0 0 [useful] 205 41 [useless] -------------------------------- 201 32 ( 6.28) (:DEFINITION REMOVE-FIRST-PAIR) 105 13 [useful] 96 19 [useless] -------------------------------- 185 185 ( 1.00) (:TYPE-PRESCRIPTION PSEUDO-TERMP) 177 177 [useful] 8 8 [useless] -------------------------------- 175 175 ( 1.00) (:TYPE-PRESCRIPTION REV0) 35 35 [useful] 140 140 [useless] -------------------------------- 168 42 ( 4.00) (:REWRITE COMMUTATIVITY-OF-+) 0 0 [useful] 168 42 [useless] -------------------------------- 168 42 ( 4.00) (:DEFINITION INTEGER-ABS) 0 0 [useful] 168 42 [useless] -------------------------------- 158 7 ( 22.57) (:DEFINITION PSEUDO-TERM-LISTP) 146 4 [useful] 12 3 [useless] -------------------------------- 156 156 ( 1.00) (:REWRITE CAR-CONS) 131 131 [useful] 25 25 [useless] -------------------------------- 150 49 ( 3.06) (:DEFINITION TRUE-LISTP) 38 13 [useful] 112 36 [useless] -------------------------------- 132 130 ( 1.01) (:TYPE-PRESCRIPTION APP0) 110 108 [useful] 22 22 [useless] -------------------------------- 129 129 ( 1.00) (:REWRITE CDR-CONS) 104 104 [useful] 25 25 [useless] -------------------------------- 115 6 ( 19.16) (:REWRITE MEM-DEL2) 1 1 [useful] 114 5 [useless] -------------------------------- 100 100 ( 1.00) (:TYPE-PRESCRIPTION PSEUDO-TERM-LISTP) 95 95 [useful] 5 5 [useless] -------------------------------- 79 19 ( 4.15) (:DEFINITION ASSOC-EQ) 64 15 [useful] 15 4 [useless] -------------------------------- 72 6 ( 12.00) (:REWRITE COMM-DEL) 11 1 [useful] 61 5 [useless] -------------------------------- 69 53 ( 1.30) (:REWRITE DEFAULT-<-2) 0 0 [useful] 69 53 [useless] -------------------------------- 66 66 ( 1.00) (:FORWARD-CHAINING ORDERED-SYMBOL-ALISTP-FORWARD-TO-SYMBOL-ALISTP) 66 66 [useful] 0 0 [useless] -------------------------------- 66 66 ( 1.00) (:TYPE-PRESCRIPTION LEN) 0 0 [useful] 66 66 [useless] -------------------------------- 62 53 ( 1.16) (:REWRITE DEFAULT-<-1) 0 0 [useful] 62 53 [useless] -------------------------------- 60 2 ( 30.00) (:REWRITE REV-APP) 60 2 [useful] 0 0 [useless] -------------------------------- 51 51 ( 1.00) (:TYPE-PRESCRIPTION O<) 51 51 [useful] 0 0 [useless] -------------------------------- 50 50 ( 1.00) (:TYPE-PRESCRIPTION TRUE-LISTP) 35 35 [useful] 15 15 [useless] -------------------------------- 47 17 ( 2.76) (:REWRITE PERM-TRANSITIVE) 1 1 [useful] 46 16 [useless] -------------------------------- 44 44 ( 1.00) (:FORWARD-CHAINING SYMBOL-ALISTP-FORWARD-TO-EQLABLE-ALISTP) 44 44 [useful] 0 0 [useless] -------------------------------- 44 44 ( 1.00) (:FORWARD-CHAINING EQLABLE-ALISTP-FORWARD-TO-ALISTP) 44 44 [useful] 0 0 [useless] -------------------------------- 44 44 ( 1.00) (:FORWARD-CHAINING ALISTP-FORWARD-TO-TRUE-LISTP) 44 44 [useful] 0 0 [useless] -------------------------------- 44 12 ( 3.66) (:DEFINITION REVAPPEND) 16 3 [useful] 28 9 [useless] -------------------------------- 42 42 ( 1.00) (:REWRITE DEFAULT-UNARY-MINUS) 0 0 [useful] 42 42 [useless] -------------------------------- 40 40 ( 1.00) (:DEFINITION ATOM) 40 40 [useful] 0 0 [useless] -------------------------------- 35 35 ( 1.00) (:FAKE-RUNE-FOR-ANONYMOUS-ENABLED-RULE NIL) 31 31 [useful] 4 4 [useless] -------------------------------- 30 3 ( 10.00) (:REWRITE APP0-RIGHT-ID) 30 3 [useful] 0 0 [useless] -------------------------------- 27 3 ( 9.00) (:DEFINITION O<) 27 3 [useful] 0 0 [useless] -------------------------------- 26 26 ( 1.00) (:REWRITE DEFAULT-COERCE-2) 0 0 [useful] 26 26 [useless] -------------------------------- 26 26 ( 1.00) (:REWRITE DEFAULT-COERCE-1) 0 0 [useful] 26 26 [useless] -------------------------------- 24 3 ( 8.00) (:REWRITE REV-REV) 0 0 [useful] 24 3 [useless] -------------------------------- 21 19 ( 1.10) (:TYPE-PRESCRIPTION INSERT) 7 5 [useful] 14 14 [useless] -------------------------------- 21 21 ( 1.00) (:REWRITE DEFAULT-REALPART) 0 0 [useful] 21 21 [useless] -------------------------------- 21 21 ( 1.00) (:REWRITE DEFAULT-NUMERATOR) 0 0 [useful] 21 21 [useless] -------------------------------- 21 21 ( 1.00) (:REWRITE DEFAULT-IMAGPART) 0 0 [useful] 21 21 [useless] -------------------------------- 21 21 ( 1.00) (:REWRITE DEFAULT-DENOMINATOR) 0 0 [useful] 21 21 [useless] -------------------------------- 19 5 ( 3.80) (:DEFINITION INSERT) 8 3 [useful] 11 2 [useless] -------------------------------- 15 5 ( 3.00) (:REWRITE UNICITY-OF-0) 9 3 [useful] 6 2 [useless] -------------------------------- 15 5 ( 3.00) (:DEFINITION SYMBOL-LISTP) 0 0 [useful] 15 5 [useless] -------------------------------- 13 3 ( 4.33) (:REWRITE ASSOC-OF-APP) 13 3 [useful] 0 0 [useless] -------------------------------- 12 12 ( 1.00) (:DEFINITION EQ) 12 12 [useful] 0 0 [useless] -------------------------------- 12 6 ( 2.00) (:DEFINITION O-FINP) 12 6 [useful] 0 0 [useless] -------------------------------- 11 11 ( 1.00) (:REWRITE CONS-CAR-CDR) 10 10 [useful] 1 1 [useless] -------------------------------- 10 5 ( 2.00) (:REWRITE APP-CONS) 7 4 [useful] 3 1 [useless] -------------------------------- 10 5 ( 2.00) (:DEFINITION FIX) 6 3 [useful] 4 2 [useless] -------------------------------- 9 3 ( 3.00) (:DEFINITION INSERT-SORT) 5 2 [useful] 4 1 [useless] -------------------------------- 8 8 ( 1.00) (:TYPE-PRESCRIPTION ENDS-IN-A-ZERO) 8 8 [useful] 0 0 [useless] -------------------------------- 8 8 ( 1.00) (:FORWARD-CHAINING PSEUDO-TERM-LISTP-FORWARD-TO-TRUE-LISTP) 8 8 [useful] 0 0 [useless] -------------------------------- 8 4 ( 2.00) (:REWRITE APP-COMMUTES) 6 3 [useful] 2 1 [useless] -------------------------------- 7 7 ( 1.00) (:DEFINITION ENDP) 7 7 [useful] 0 0 [useless] -------------------------------- 7 7 ( 1.00) (:TYPE-PRESCRIPTION BINARY-APPEND) 1 1 [useful] 6 6 [useless] -------------------------------- 7 7 ( 1.00) (:REWRITE LT-NON-SYMMETRIC) 0 0 [useful] 7 7 [useless] -------------------------------- 6 3 ( 2.00) (:DEFINITION BINARY-APPEND) 3 2 [useful] 3 1 [useless] -------------------------------- 5 5 ( 1.00) (:TYPE-PRESCRIPTION SYMBOL-LISTP) 0 0 [useful] 5 5 [useless] -------------------------------- 4 4 ( 1.00) (:TYPE-PRESCRIPTION IFF) 4 4 [useful] 0 0 [useless] -------------------------------- 3 1 ( 3.00) (:REWRITE ENDS-IN-A-ZERO-APP0) 3 1 [useful] 0 0 [useless] -------------------------------- 3 2 ( 1.50) (:REWRITE INSERT-IS-CONS) 2 1 [useful] 1 1 [useless] -------------------------------- 2 2 ( 1.00) (:REWRITE SYMBOL-<-IRREFLEXIVE) 2 2 [useful] 0 0 [useless] -------------------------------- 2 2 ( 1.00) (:DEFINITION IFF) 2 2 [useful] 0 0 [useless] -------------------------------- 2 2 ( 1.00) (:DEFINITION FORCE) 2 2 [useful] 0 0 [useless] -------------------------------- 2 2 ( 1.00) (:DEFINITION ENDS-IN-A-ZERO) 2 2 [useful] 0 0 [useless] -------------------------------- 1 1 ( 1.00) (:TYPE-PRESCRIPTION LT) 1 1 [useful] 0 0 [useless] -------------------------------- 1 1 ( 1.00) (:REWRITE PERM-REFLEXIVE) 1 1 [useful] 0 0 [useless] -------------------------------- 1 1 ( 1.00) (:REWRITE PERM-DEL) 1 1 [useful] 0 0 [useless] -------------------------------- 1 1 ( 1.00) (:REWRITE ==-SYMMETRIC) 1 1 [useful] 0 0 [useless] -------------------------------- NIL ACL2 !>Bye. mac:~/class-demo-2008-10-30$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(include-book "arithmetic/top-with-meta") ACL2 Error in ( INCLUDE-BOOK "arithmetic/top-with-meta" ...): There is no file named "/Users/kaufmann/class-demo-2008-10-30/arithmetic/top-with-meta.lisp" that can be opened for input. Summary Form: ( INCLUDE-BOOK "arithmetic/top-with-meta" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( INCLUDE-BOOK "arithmetic/top-with-meta" ...): See :DOC failure. ******** FAILED ******** ACL2 !>(include-book "arithmetic/top-with-meta" :dir :system) Summary Form: ( INCLUDE-BOOK "arithmetic/top-with-meta" ...) Rules: NIL Warnings: None Time: 0.18 seconds (prove: 0.00, print: 0.00, other: 0.18) "/Users/kaufmann/acl2/v3-4/acl2-sources/books/arithmetic/top-with-meta.lisp" ACL2 !>(defthm bad-assoc (equal (+ x (+ y z)) (+ (+ x y) z))) ACL2 Warning [Subsume] in ( DEFTHM BAD-ASSOC ...): A newly proposed :REWRITE rule generated from BAD-ASSOC probably subsumes the previously added :REWRITE rules FOLD-CONSTS- IN-+, MINUS-CANCELLATION-ON-LEFT, MINUS-CANCELLATION-ON- RIGHT and COMMUTATIVITY-2-OF-+, in the sense that the new rule will now probably be applied whenever the old rules would have been. ACL2 Warning [Subsume] in ( DEFTHM BAD-ASSOC ...): The previously added rules COMMUTATIVITY-2-OF-+ and COMMUTATIVITY- OF-+ subsume a newly proposed :REWRITE rule generated from BAD-ASSOC, in the sense that the old rules rewrite more general targets. Because the new rule will be tried first, it may nonetheless find application. Q.E.D. Summary Form: ( DEFTHM BAD-ASSOC ...) Rules: ((:REWRITE ASSOCIATIVITY-OF-+)) Warnings: Subsume Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) BAD-ASSOC ACL2 !>(thm (equal (+ x (+ y z)) (+ (+ x y) z))) HARD ACL2 ERROR in PREPROCESS: The call depth limit of 1000 has been exceeded in the ACL2 preprocessor (a sort of rewriter). There is probably a loop caused by some set of enabled simple rules. To see why the limit was exceeded, execute :brr t and next retry the proof with :hints :do-not '(preprocess) and then follow the directions in the resulting error message. See :DOC rewrite-stack-limit. ACL2 Error in TOP-LEVEL: Evaluation aborted. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>:u d 1:x(INCLUDE-BOOK "arithmetic/top-with-meta" :DIR ...) ACL2 !>(defstub foo (x) t) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>(LOGIC) The event ( TABLE ACL2-DEFAULTS-TABLE ...) is redundant. See :DOC redundant-events. :INVISIBLE ACL2 !>>(LOCAL (DEFUN FOO (X) (DECLARE (IGNORE X)) T)) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (FOO X). Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. Summary Form: ( ENCAPSULATE ((FOO ...) ...) ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) T ACL2 !>(thm (equal (foo (+ 3 (+ 4 x))) (foo (+ 7 x)))) Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-+) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE FOLD-CONSTS-IN-+)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Proof succeeded. ACL2 !>:pe FOLD-CONSTS-IN-+ d 1 (INCLUDE-BOOK "arithmetic/top-with-meta" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/acl2/v3-4/acl2-sources/books/arithmetic/top-with-meta.lisp" "/Users/kaufmann/acl2/v3-4/acl2-sources/books/arithmetic/top.lisp" "/Users/kaufmann/acl2/v3-4/acl2-sources/books/arithmetic/equalities.lisp" ] \ > (DEFTHM FOLD-CONSTS-IN-+ (IMPLIES (AND (SYNTAXP (QUOTEP X)) (SYNTAXP (QUOTEP Y))) (EQUAL (+ X (+ Y Z)) (+ (+ X Y) Z)))) ACL2 !>Bye. mac:~/class-demo-2008-10-30$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(defun foo (x) x) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (EQUAL (FOO X) X). Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FOO ACL2 !>(thm (equal (foo x) (cons x x))) Goal' Goal'' ([ A key checkpoint: Goal'' NIL A goal of NIL, Goal'', has been generated! Obviously, the proof attempt has failed. ]) Summary Form: ( THM ...) Rules: ((:DEFINITION FOO) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) --- The key checkpoint goal, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint- summary-limit. --- *** Key checkpoint at the top level: *** Goal'' NIL ACL2 Error in ( THM ...): See :DOC failure. ******** FAILED ******** ACL2 !>(defun foo (x) (cons x x)) ACL2 Error in ( DEFUN FOO ...): The name FOO is in use as a function. Note that the proposed body for FOO, (CONS X X), differs from the existing body, X. The redefinition feature is currently off. See :DOC ld- redefinition-action. Note: FOO was previously defined at the top level. Summary Form: ( DEFUN FOO ...) Rules: NIL Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) ACL2 Error in ( DEFUN FOO ...): See :DOC failure. ******** FAILED ******** ACL2 !>:redef (:QUERY . :OVERWRITE) ACL2 !>(defun foo (x) (cons x x)) ACL2 Query (:REDEF): The name FOO is in use as a function. Its current defun-mode is :logic. Do you want to redefine it? (N, Y, E, O or ?): y Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (CONSP (FOO X)). We used primitive type reasoning. Summary Form: ( DEFUN FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) FOO ACL2 !>(thm (equal (foo x) (cons x x))) Q.E.D. Summary Form: ( THM ...) Rules: ((:DEFINITION FOO) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Proof succeeded. ACL2 !>:redef! (:WARN! . :OVERWRITE) ACL2 !>(defun foo (x) (+ x x)) Since FOO is non-recursive, its admission is trivial. We observe that the type of FOO is described by the theorem (ACL2-NUMBERP (FOO X)). We used primitive type reasoning. ACL2 Warning [Redef] in ( DEFUN FOO ...): FOO redefined. Summary Form: ( DEFUN FOO ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Redef Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) FOO ACL2 !>Bye. mac:~/class-demo-2008-10-30$ acl2-3.4 Welcome to Clozure Common Lisp Version 1.2-r9226-RC1 (DarwinX8664)! ACL2 Version 3.4 built August 11, 2008 14:18:46. Copyright (C) 2008 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-3-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. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 3.4. Level 1. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(ld "isort-is-msort.lisp") ACL2 Version 3.4. Level 2. Cbd "/Users/kaufmann/class-demo-2008-10-30/". Distributed books directory "/Users/kaufmann/acl2/v3-4/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>> "ACL2" ACL2 !>> Summary Form: ( INCLUDE-BOOK "isort" ...) Rules: NIL Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) "/Users/kaufmann/class-demo-2008-10-30/isort.lisp" ACL2 !>> Summary Form: ( INCLUDE-BOOK "msort" ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) "/Users/kaufmann/class-demo-2008-10-30/msort.lisp" ACL2 !>> The event ( INCLUDE-BOOK "ordered-perms" ...) is redundant. See :DOC redundant-events. Summary Form: ( INCLUDE-BOOK "ordered-perms" ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :REDUNDANT ACL2 !>> *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (ISORT X). This suggestion was produced using the :induction rule ISORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit ISORT. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' Subgoal *1/2'4' Subgoal *1/2'5' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2'' (IMPLIES (AND (CONSP X) (TRUE-LISTP (ISORT (CDR X)))) (TRUE-LISTP (INSERT (CAR X) (ISORT (CDR X))))) *1.1 (Subgoal *1/2'5') is pushed for proof by induction. ]) Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (TRUE-LISTP IT) (TRUE-LISTP (INSERT X1 IT))). Subgoal *1.1/4 Subgoal *1.1/4' Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/2'' Subgoal *1.1/1 Subgoal *1.1/1' *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/2'' and Goal are COMPLETED! Q.E.D. The storage of TRUE-LISTP-ISORT depends upon the :type- prescription rule TRUE-LISTP. Summary Form: ( DEFTHM TRUE-LISTP-ISORT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION INSERT) (:DEFINITION ISORT) (:DEFINITION NOT) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION INSERT) (:INDUCTION ISORT) (:INDUCTION TRUE-LISTP) (:REWRITE LEXORDER-REFLEXIVE) (:REWRITE LEXORDER-TRANSITIVE) (:TYPE-PRESCRIPTION INSERT) (:TYPE-PRESCRIPTION LEXORDER) (:TYPE-PRESCRIPTION TRUE-LISTP)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.01, other: 0.00) TRUE-LISTP-ISORT ACL2 !>> *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (MSORT X). This suggestion was produced using the :induction rule MSORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (EVENS X)) (:P (ODDS X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit MSORT. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' Subgoal *1/3'5' Subgoal *1/3'6' Subgoal *1/3'7' Subgoal *1/3'8' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3''' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (TRUE-LISTP (MSORT (EVENS X))) (TRUE-LISTP (MSORT (EVENS (CDR X))))) (TRUE-LISTP (MERGE2 (MSORT (EVENS X)) (MSORT (EVENS (CDR X)))))) *1.1 (Subgoal *1/3'8') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (AND (TRUE-LISTP MT0) (TRUE-LISTP MT)) (TRUE-LISTP (MERGE2 MT0 MT))). Subgoal *1.1/6 Subgoal *1.1/6' Subgoal *1.1/5 Subgoal *1.1/4 Subgoal *1.1/4' Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/1 Subgoal *1.1/1' *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/3''' and Goal are COMPLETED! Q.E.D. The storage of TRUE-LISTP-MSORT depends upon the :type- prescription rule TRUE-LISTP. Summary Form: ( DEFTHM TRUE-LISTP-MSORT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION MERGE2) (:DEFINITION MSORT) (:DEFINITION NOT) (:DEFINITION ODDS) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION MERGE2) (:INDUCTION MSORT) (:INDUCTION TRUE-LISTP) (:REWRITE LEXORDER-REFLEXIVE) (:REWRITE LEXORDER-TRANSITIVE) (:TYPE-PRESCRIPTION EVENS) (:TYPE-PRESCRIPTION LEXORDER) (:TYPE-PRESCRIPTION MERGE2) (:TYPE-PRESCRIPTION TRUE-LISTP)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00) TRUE-LISTP-MSORT ACL2 !>> ACL2 Warning [Subsume] in ( DEFTHM ISORT-IS-MSORT ...): A newly proposed :REWRITE rule generated from ISORT-IS-MSORT probably subsumes the previously added :REWRITE rule ISORT- PERM, in the sense that the new rule will now probably be applied whenever the old rule would have been. Q.E.D. Summary Form: ( DEFTHM ISORT-IS-MSORT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CONVERT-PERM-TO-HOW-MANY) (:REWRITE HOW-MANY-ISORT) (:REWRITE HOW-MANY-MSORT) (:REWRITE ORDERED-PERMS) (:REWRITE ORDEREDP-ISORT) (:REWRITE ORDEREDP-MSORT) (:REWRITE TRUE-LISTP-ISORT) (:REWRITE TRUE-LISTP-MSORT)) Warnings: Subsume Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) ISORT-IS-MSORT ACL2 !>>Bye. :EOF ACL2 !>:u 4:x(DEFTHM TRUE-LISTP-MSORT ...) ACL2 !>(defthm isort-is-msort (equal (isort x) (msort x))) ACL2 Warning [Subsume] in ( DEFTHM ISORT-IS-MSORT ...): A newly proposed :REWRITE rule generated from ISORT-IS-MSORT probably subsumes the previously added :REWRITE rule ISORT- PERM, in the sense that the new rule will now probably be applied whenever the old rule would have been. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. By considering those suggested by the largest number of non-primitive recursive functions, we narrow the field to one. We will induct according to a scheme suggested by (MSORT X). This suggestion was produced using the :induction rule MSORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (EVENS X)) (:P (ODDS X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit MSORT. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' Subgoal *1/3'5' Subgoal *1/3'6' Subgoal *1/3'7' Subgoal *1/3'8' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3'4' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (EQUAL (ISORT (EVENS X)) (MSORT (EVENS X))) (EQUAL (ISORT (EVENS (CDR X))) (MSORT (EVENS (CDR X))))) (EQUAL (INSERT (CAR X) (ISORT (CDR X))) (MERGE2 (ISORT (EVENS X)) (ISORT (EVENS (CDR X)))))) *1.1 (Subgoal *1/3'8') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (CONSP X2) (EQUAL (INSERT X1 (ISORT X2)) (MERGE2 (MSORT (EVENS (CONS X1 X2))) (MSORT (EVENS X2))))). Subgoal *1.1/3 Subgoal *1.1/3' Subgoal *1.1/3.2 Subgoal *1.1/3.2' Subgoal *1.1/3.2'' Subgoal *1.1/3.2''' *1.1.1 (Subgoal *1.1/3.2''') is pushed for proof by induction. Subgoal *1.1/3.1 Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/2.2 Subgoal *1.1/2.2.4 Subgoal *1.1/2.2.4' Subgoal *1.1/2.2.3 Subgoal *1.1/2.2.2 Subgoal *1.1/2.2.2.3 Subgoal *1.1/2.2.2.2 Subgoal *1.1/2.2.2.1 Subgoal *1.1/2.2.1 Subgoal *1.1/2.1 Subgoal *1.1/1 So we now return to *1.1.1, which is (IMPLIES (AND (TRUE-LISTP ES) (EQUAL (INSERT X1 IT) (MERGE2 (MSORT (EVENS (CONS X1 X6))) (MSORT ES)))) (EQUAL (INSERT X1 (INSERT X3 (INSERT X5 IT))) (MERGE2 (MSORT (CONS X1 (EVENS (CONS X5 X6)))) (MSORT (CONS X3 ES))))). Subgoal *1.1.1/4 Subgoal *1.1.1/4' Subgoal *1.1.1/4.4 Subgoal *1.1.1/4.4.2 Subgoal *1.1.1/4.4.2' Subgoal *1.1.1/4.4.2'' Subgoal *1.1.1/4.4.2''' Subgoal *1.1.1/4.4.2'4' *1.1.1.1 (Subgoal *1.1.1/4.4.2'4') is pushed for proof by induction. Subgoal *1.1.1/4.4.1 Subgoal *1.1.1/4.4.1' Subgoal *1.1.1/4.4.1'' Subgoal *1.1.1/4.4.1''' Subgoal *1.1.1/4.4.1'4' *1.1.1.2 (Subgoal *1.1.1/4.4.1'4') is pushed for proof by induction. Subgoal *1.1.1/4.3 Subgoal *1.1.1/4.3' Subgoal *1.1.1/4.3'' Subgoal *1.1.1/4.3''' Subgoal *1.1.1/4.3'4' *1.1.1.3 (Subgoal *1.1.1/4.3'4') is pushed for proof by induction. Subgoal *1.1.1/4.2 Subgoal *1.1.1/4.2.2 Subgoal *1.1.1/4.2.1 Subgoal *1.1.1/4.2.1' Subgoal *1.1.1/4.2.1'' Subgoal *1.1.1/4.2.1''' *1.1.1.4 (Subgoal *1.1.1/4.2.1''') is pushed for proof by induction. Subgoal *1.1.1/4.1 Subgoal *1.1.1/4.1' Subgoal *1.1.1/4.1'' Subgoal *1.1.1/4.1''' *1.1.1.5 (Subgoal *1.1.1/4.1''') is pushed for proof by induction. Subgoal *1.1.1/3 Subgoal *1.1.1/3' Subgoal *1.1.1/3.4 Subgoal *1.1.1/3.4.2 Subgoal *1.1.1/3.4.2' Subgoal *1.1.1/3.4.2'' Subgoal *1.1.1/3.4.2''' *1.1.1.6 (Subgoal *1.1.1/3.4.2''') is pushed for proof by induction. Subgoal *1.1.1/3.4.1 Subgoal *1.1.1/3.4.1' Subgoal *1.1.1/3.4.1'' Subgoal *1.1.1/3.4.1''' *1.1.1.7 (Subgoal *1.1.1/3.4.1''') is pushed for proof by induction. Subgoal *1.1.1/3.3 Subgoal *1.1.1/3.3' Subgoal *1.1.1/3.3'' Subgoal *1.1.1/3.3''' *1.1.1.8 (Subgoal *1.1.1/3.3''') is pushed for proof by induction. Subgoal *1.1.1/3.2 Subgoal *1.1.1/3.2.2 Subgoal *1.1.1/3.2.1 Subgoal *1.1.1/3.2.1' Subgoal *1.1.1/3.2.1'' *1.1.1.9 (Subgoal *1.1.1/3.2.1'') is pushed for proof by induction. Subgoal *1.1.1/3.1 Subgoal *1.1.1/3.1' Subgoal *1.1.1/3.1'' Subgoal *1.1.1/3.1''' *1.1.1.10 (Subgoal *1.1.1/3.1''') is pushed for proof by induction. Subgoal *1.1.1/2 Subgoal *1.1.1/2' Subgoal *1.1.1/2.4 Subgoal *1.1.1/2.4.3 Subgoal *1.1.1/2.4.3' Subgoal *1.1.1/2.4.3'' Subgoal *1.1.1/2.4.3''' *1.1.1.11 (Subgoal *1.1.1/2.4.3''') is pushed for proof by induction. Subgoal *1.1.1/2.4.2 Subgoal *1.1.1/2.4.2' Subgoal *1.1.1/2.4.2'' Subgoal *1.1.1/2.4.2''' *1.1.1.12 (Subgoal *1.1.1/2.4.2''') is pushed for proof by induction. Subgoal *1.1.1/2.4.1 Subgoal *1.1.1/2.4.1' Subgoal *1.1.1/2.4.1'' Subgoal *1.1.1/2.4.1''' *1.1.1.13 (Subgoal *1.1.1/2.4.1''') is pushed for proof by induction. Subgoal *1.1.1/2.3 Subgoal *1.1.1/2.3.2 Subgoal *1.1.1/2.3.2' Subgoal *1.1.1/2.3.2'' Subgoal *1.1.1/2.3.2.2 Subgoal *1.1.1/2.3.2.2' *1.1.1.14 (Subgoal *1.1.1/2.3.2.2') is pushed for proof by induction. Subgoal *1.1.1/2.3.2.1 *1.1.1.15 (Subgoal *1.1.1/2.3.2.1) is pushed for proof by induction. Subgoal *1.1.1/2.3.1 Subgoal *1.1.1/2.3.1' Subgoal *1.1.1/2.3.1'' Subgoal *1.1.1/2.3.1.2 Subgoal *1.1.1/2.3.1.2.2 Subgoal *1.1.1/2.3.1.2.2' *1.1.1.16 (Subgoal *1.1.1/2.3.1.2.2') is pushed for proof by induction. Subgoal *1.1.1/2.3.1.2.1 Subgoal *1.1.1/2.3.1.2.1' *1.1.1.17 (Subgoal *1.1.1/2.3.1.2.1') is pushed for proof by induction. Subgoal *1.1.1/2.3.1.1 Subgoal *1.1.1/2.3.1.1' *1.1.1.18 (Subgoal *1.1.1/2.3.1.1') is pushed for proof by induction. Subgoal *1.1.1/2.2 Subgoal *1.1.1/2.2.3 Subgoal *1.1.1/2.2.2 Subgoal *1.1.1/2.2.2' Subgoal *1.1.1/2.2.2'' Subgoal *1.1.1/2.2.2''' *1.1.1.19 (Subgoal *1.1.1/2.2.2''') is pushed for proof by induction. Subgoal *1.1.1/2.2.1 Subgoal *1.1.1/2.1 Subgoal *1.1.1/2.1.4 Subgoal *1.1.1/2.1.3 Subgoal *1.1.1/2.1.3.2 Subgoal *1.1.1/2.1.3.1 Subgoal *1.1.1/2.1.3.1' Subgoal *1.1.1/2.1.3.1'' Subgoal *1.1.1/2.1.3.1''' *1.1.1.20 (Subgoal *1.1.1/2.1.3.1''') is pushed for proof by induction. Subgoal *1.1.1/2.1.2 Subgoal *1.1.1/2.1.1 Subgoal *1.1.1/2.1.1' Subgoal *1.1.1/2.1.1'' Subgoal *1.1.1/2.1.1''' *1.1.1.21 (Subgoal *1.1.1/2.1.1''') is pushed for proof by induction. Subgoal *1.1.1/1 Subgoal *1.1.1/1' Subgoal *1.1.1/1.2 Subgoal *1.1.1/1.2.3 *1.1.1.22 (Subgoal *1.1.1/1.2.3) is pushed for proof by induction. Subgoal *1.1.1/1.2.2 *1.1.1.23 (Subgoal *1.1.1/1.2.2) is pushed for proof by induction. Subgoal *1.1.1/1.2.1 Subgoal *1.1.1/1.2.1' *1.1.1.24 (Subgoal *1.1.1/1.2.1') is pushed for proof by induction. Subgoal *1.1.1/1.1 Subgoal *1.1.1/1.1.3 *1.1.1.25 (Subgoal *1.1.1/1.1.3) is pushed for proof by induction. Subgoal *1.1.1/1.1.2 *1.1.1.26 (Subgoal *1.1.1/1.1.2) is pushed for proof by induction. Subgoal *1.1.1/1.1.1 *1.1.1.27 (Subgoal *1.1.1/1.1.1) is pushed for proof by induction. So we now return to *1.1.1.27, which is (IMPLIES (AND (NOT (CONSP IT)) (TRUE-LISTP ES) (EQUAL (CONS X1 IT) (MERGE2 (MSORT (EVENS (CONS X1 X6))) (MSORT ES))) (NOT (LEXORDER X3 X5)) (NOT (LEXORDER X1 X5)) (LEXORDER X1 X3)) (EQUAL (LIST* X5 X1 X3 IT) (MERGE2 (MSORT (CONS X1 (EVENS (CONS X5 X6)))) (MSORT (CONS X3 ES))))). Subgoal *1.1.1.27/11 Subgoal *1.1.1.27/11' Subgoal *1.1.1.27/11'' Subgoal *1.1.1.27/11''' Subgoal *1.1.1.27/11'4' Subgoal *1.1.1.27/11'5' Subgoal *1.1.1.27/11'6' Subgoal *1.1.1.27/11'7' Subgoal *1.1.1.27/11'8' Subgoal *1.1.1.27/11'9' Subgoal *1.1.1.27/11'10' Subgoal *1.1.1.27/11'11' *1.1.1.27.1 (Subgoal *1.1.1.27/11'11') is pushed for proof by induction. Subgoal *1.1.1.27/10 Subgoal *1.1.1.27/10' Subgoal *1.1.1.27/10'' Subgoal *1.1.1.27/10''' Subgoal *1.1.1.27/10'4' Subgoal *1.1.1.27/10'5' Subgoal *1.1.1.27/10'6' Subgoal *1.1.1.27/10'7' Subgoal *1.1.1.27/10'8' Subgoal *1.1.1.27/10'9' Subgoal *1.1.1.27/10'10' *1.1.1.27.2 (Subgoal *1.1.1.27/10'10') is pushed for proof by induction. Subgoal *1.1.1.27/9 Subgoal *1.1.1.27/8 Subgoal *1.1.1.27/8' Subgoal *1.1.1.27/8'' Subgoal *1.1.1.27/8''' Subgoal *1.1.1.27/8'4' Subgoal *1.1.1.27/8'5' Subgoal *1.1.1.27/8'6' Subgoal *1.1.1.27/8'7' Subgoal *1.1.1.27/8'8' Subgoal *1.1.1.27/8'9' Subgoal *1.1.1.27/8'10' *1.1.1.27.3 (Subgoal *1.1.1.27/8'10') is pushed for proof by induction. Subgoal *1.1.1.27/7 Subgoal *1.1.1.27/7' Subgoal *1.1.1.27/7'' Subgoal *1.1.1.27/7''' Subgoal *1.1.1.27/7'4' Subgoal *1.1.1.27/7'5' Subgoal *1.1.1.27/7'6' Subgoal *1.1.1.27/7'7' Subgoal *1.1.1.27/7'8' *1.1.1.27.4 (Subgoal *1.1.1.27/7'8') is pushed for proof by induction. Subgoal *1.1.1.27/6 Subgoal *1.1.1.27/5 Subgoal *1.1.1.27/4 Subgoal *1.1.1.27/3 Subgoal *1.1.1.27/2 Subgoal *1.1.1.27/2' Subgoal *1.1.1.27/2'' Subgoal *1.1.1.27/2''' Subgoal *1.1.1.27/2'4' Subgoal *1.1.1.27/2.2 *1.1.1.27.5 (Subgoal *1.1.1.27/2.2) is pushed for proof by induction. Subgoal *1.1.1.27/2.1 *1.1.1.27.6 (Subgoal *1.1.1.27/2.1) is pushed for proof by induction. Subgoal *1.1.1.27/1 Subgoal *1.1.1.27/1' Subgoal *1.1.1.27/1'' Subgoal *1.1.1.27/1''' Subgoal *1.1.1.27/1'4' Subgoal *1.1.1.27/1'5' *1.1.1.27.7 (Subgoal *1.1.1.27/1'5') is pushed for proof by induction. So we now return to *1.1.1.27.7, which is (IMPLIES (AND (NOT (CONSP IT)) (NOT (LEXORDER X3 X5)) (NOT (LEXORDER X1 X5)) (LEXORDER X1 X3)) (EQUAL (LIST* X5 X1 X3 IT) (MERGE2 (MSORT (CONS X1 (EVENS (CONS X5 X6)))) (LIST X3)))). No induction schemes are suggested by *1.1.1.27.7. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ISORT-IS-MSORT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION EVENS) (:DEFINITION INSERT) (:DEFINITION ISORT) (:DEFINITION MERGE2) (:DEFINITION MSORT) (:DEFINITION NOT) (:DEFINITION ODDS) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EVENS) (:EXECUTABLE-COUNTERPART ISORT) (:EXECUTABLE-COUNTERPART MSORT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING LEXORDER-ANTI-SYMMETRIC) (:FORWARD-CHAINING LEXORDER-TOTAL) (:INDUCTION EVENS) (:INDUCTION INSERT) (:INDUCTION ISORT) (:INDUCTION MSORT) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-CDR) (:REWRITE LEXORDER-REFLEXIVE) (:REWRITE LEXORDER-TRANSITIVE) (:TYPE-PRESCRIPTION EVENS) (:TYPE-PRESCRIPTION LEXORDER) (:TYPE-PRESCRIPTION ODDS)) Warnings: Subsume Time: 0.57 seconds (prove: 0.54, print: 0.03, other: 0.00) --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint- summary-limit. --- *** Key checkpoint at the top level: *** Goal (EQUAL (ISORT X) (MSORT X)) *** Key checkpoint under a top-level induction: *** Subgoal *1/3'4' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (EQUAL (ISORT (EVENS X)) (MSORT (EVENS X))) (EQUAL (ISORT (EVENS (CDR X))) (MSORT (EVENS (CDR X))))) (EQUAL (INSERT (CAR X) (ISORT (CDR X))) (MERGE2 (ISORT (EVENS X)) (ISORT (EVENS (CDR X)))))) ACL2 Error in ( DEFTHM ISORT-IS-MSORT ...): See :DOC failure. ******** FAILED ******** ACL2 !>:u 3:x(DEFTHM TRUE-LISTP-ISORT ...) ACL2 !>:U 2:x(INCLUDE-BOOK "msort") ACL2 !>(defthm isort-is-msort (equal (isort x) (msort x)) :hints (("Goal" :in-theory (enable ordered-perms)))) ACL2 Warning [Subsume] in ( DEFTHM ISORT-IS-MSORT ...): A newly proposed :REWRITE rule generated from ISORT-IS-MSORT probably subsumes the previously added :REWRITE rule ISORT- PERM, in the sense that the new rule will now probably be applied whenever the old rule would have been. *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. Two induction schemes are suggested by this conjecture. By considering those suggested by the largest number of non-primitive recursive functions, we narrow the field to one. We will induct according to a scheme suggested by (MSORT X). This suggestion was produced using the :induction rule MSORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (EVENS X)) (:P (ODDS X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit MSORT. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' Subgoal *1/3'5' Subgoal *1/3'6' Subgoal *1/3'7' Subgoal *1/3'8' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3'4' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (EQUAL (ISORT (EVENS X)) (MSORT (EVENS X))) (EQUAL (ISORT (EVENS (CDR X))) (MSORT (EVENS (CDR X))))) (EQUAL (INSERT (CAR X) (ISORT (CDR X))) (MERGE2 (ISORT (EVENS X)) (ISORT (EVENS (CDR X)))))) *1.1 (Subgoal *1/3'8') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (CONSP X2) (EQUAL (INSERT X1 (ISORT X2)) (MERGE2 (MSORT (EVENS (CONS X1 X2))) (MSORT (EVENS X2))))). Subgoal *1.1/3 Subgoal *1.1/3' Subgoal *1.1/3.2 Subgoal *1.1/3.2' Subgoal *1.1/3.2'' Subgoal *1.1/3.2''' *1.1.1 (Subgoal *1.1/3.2''') is pushed for proof by induction. Subgoal *1.1/3.1 Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/2.2 Subgoal *1.1/2.2.4 Subgoal *1.1/2.2.4' Subgoal *1.1/2.2.3 Subgoal *1.1/2.2.2 Subgoal *1.1/2.2.2.3 Subgoal *1.1/2.2.2.2 Subgoal *1.1/2.2.2.1 Subgoal *1.1/2.2.1 Subgoal *1.1/2.1 Subgoal *1.1/1 So we now return to *1.1.1, which is (IMPLIES (AND (TRUE-LISTP ES) (EQUAL (INSERT X1 IT) (MERGE2 (MSORT (EVENS (CONS X1 X6))) (MSORT ES)))) (EQUAL (INSERT X1 (INSERT X3 (INSERT X5 IT))) (MERGE2 (MSORT (CONS X1 (EVENS (CONS X5 X6)))) (MSORT (CONS X3 ES))))). Subgoal *1.1.1/4 Subgoal *1.1.1/4' Subgoal *1.1.1/4.4 Subgoal *1.1.1/4.4.2 Subgoal *1.1.1/4.4.2' Subgoal *1.1.1/4.4.2'' Subgoal *1.1.1/4.4.2''' Subgoal *1.1.1/4.4.2'4' *1.1.1.1 (Subgoal *1.1.1/4.4.2'4') is pushed for proof by induction. Subgoal *1.1.1/4.4.1 Subgoal *1.1.1/4.4.1' Subgoal *1.1.1/4.4.1'' Subgoal *1.1.1/4.4.1''' Subgoal *1.1.1/4.4.1'4' *1.1.1.2 (Subgoal *1.1.1/4.4.1'4') is pushed for proof by induction. Subgoal *1.1.1/4.3 Subgoal *1.1.1/4.3' Subgoal *1.1.1/4.3'' Subgoal *1.1.1/4.3''' Subgoal *1.1.1/4.3'4' *1.1.1.3 (Subgoal *1.1.1/4.3'4') is pushed for proof by induction. Subgoal *1.1.1/4.2 Subgoal *1.1.1/4.2.2 Subgoal *1.1.1/4.2.1 Subgoal *1.1.1/4.2.1' Subgoal *1.1.1/4.2.1'' Subgoal *1.1.1/4.2.1''' *1.1.1.4 (Subgoal *1.1.1/4.2.1''') is pushed for proof by induction. Subgoal *1.1.1/4.1 Subgoal *1.1.1/4.1' Subgoal *1.1.1/4.1'' Subgoal *1.1.1/4.1''' *1.1.1.5 (Subgoal *1.1.1/4.1''') is pushed for proof by induction. Subgoal *1.1.1/3 Subgoal *1.1.1/3' Subgoal *1.1.1/3.4 Subgoal *1.1.1/3.4.2 Subgoal *1.1.1/3.4.2' Subgoal *1.1.1/3.4.2'' Subgoal *1.1.1/3.4.2''' *1.1.1.6 (Subgoal *1.1.1/3.4.2''') is pushed for proof by induction. Subgoal *1.1.1/3.4.1 Subgoal *1.1.1/3.4.1' Subgoal *1.1.1/3.4.1'' Subgoal *1.1.1/3.4.1''' *1.1.1.7 (Subgoal *1.1.1/3.4.1''') is pushed for proof by induction. Subgoal *1.1.1/3.3 Subgoal *1.1.1/3.3' Subgoal *1.1.1/3.3'' Subgoal *1.1.1/3.3''' *1.1.1.8 (Subgoal *1.1.1/3.3''') is pushed for proof by induction. Subgoal *1.1.1/3.2 Subgoal *1.1.1/3.2.2 Subgoal *1.1.1/3.2.1 Subgoal *1.1.1/3.2.1' Subgoal *1.1.1/3.2.1'' *1.1.1.9 (Subgoal *1.1.1/3.2.1'') is pushed for proof by induction. Subgoal *1.1.1/3.1 Subgoal *1.1.1/3.1' Subgoal *1.1.1/3.1'' Subgoal *1.1.1/3.1''' *1.1.1.10 (Subgoal *1.1.1/3.1''') is pushed for proof by induction. Subgoal *1.1.1/2 Subgoal *1.1.1/2' Subgoal *1.1.1/2.4 Subgoal *1.1.1/2.4.3 Subgoal *1.1.1/2.4.3' Subgoal *1.1.1/2.4.3'' Subgoal *1.1.1/2.4.3''' *1.1.1.11 (Subgoal *1.1.1/2.4.3''') is pushed for proof by induction. Subgoal *1.1.1/2.4.2 Subgoal *1.1.1/2.4.2' Subgoal *1.1.1/2.4.2'' Subgoal *1.1.1/2.4.2''' *1.1.1.12 (Subgoal *1.1.1/2.4.2''') is pushed for proof by induction. Subgoal *1.1.1/2.4.1 Subgoal *1.1.1/2.4.1' Subgoal *1.1.1/2.4.1'' Subgoal *1.1.1/2.4.1''' *1.1.1.13 (Subgoal *1.1.1/2.4.1''') is pushed for proof by induction. Subgoal *1.1.1/2.3 Subgoal *1.1.1/2.3.2 Subgoal *1.1.1/2.3.2' Subgoal *1.1.1/2.3.2'' Subgoal *1.1.1/2.3.2.2 Subgoal *1.1.1/2.3.2.2' *1.1.1.14 (Subgoal *1.1.1/2.3.2.2') is pushed for proof by induction. Subgoal *1.1.1/2.3.2.1 *1.1.1.15 (Subgoal *1.1.1/2.3.2.1) is pushed for proof by induction. Subgoal *1.1.1/2.3.1 Subgoal *1.1.1/2.3.1' Subgoal *1.1.1/2.3.1'' Subgoal *1.1.1/2.3.1.2 Subgoal *1.1.1/2.3.1.2.2 Subgoal *1.1.1/2.3.1.2.2' *1.1.1.16 (Subgoal *1.1.1/2.3.1.2.2') is pushed for proof by induction. Subgoal *1.1.1/2.3.1.2.1 Subgoal *1.1.1/2.3.1.2.1' *1.1.1.17 (Subgoal *1.1.1/2.3.1.2.1') is pushed for proof by induction. Subgoal *1.1.1/2.3.1.1 Subgoal *1.1.1/2.3.1.1' *1.1.1.18 (Subgoal *1.1.1/2.3.1.1') is pushed for proof by induction. Subgoal *1.1.1/2.2 Subgoal *1.1.1/2.2.3 Subgoal *1.1.1/2.2.2 Subgoal *1.1.1/2.2.2' Subgoal *1.1.1/2.2.2'' Subgoal *1.1.1/2.2.2''' *1.1.1.19 (Subgoal *1.1.1/2.2.2''') is pushed for proof by induction. Subgoal *1.1.1/2.2.1 Subgoal *1.1.1/2.1 Subgoal *1.1.1/2.1.4 Subgoal *1.1.1/2.1.3 Subgoal *1.1.1/2.1.3.2 Subgoal *1.1.1/2.1.3.1 Subgoal *1.1.1/2.1.3.1' Subgoal *1.1.1/2.1.3.1'' Subgoal *1.1.1/2.1.3.1''' *1.1.1.20 (Subgoal *1.1.1/2.1.3.1''') is pushed for proof by induction. Subgoal *1.1.1/2.1.2 Subgoal *1.1.1/2.1.1 Subgoal *1.1.1/2.1.1' Subgoal *1.1.1/2.1.1'' Subgoal *1.1.1/2.1.1''' *1.1.1.21 (Subgoal *1.1.1/2.1.1''') is pushed for proof by induction. Subgoal *1.1.1/1 Subgoal *1.1.1/1' Subgoal *1.1.1/1.2 Subgoal *1.1.1/1.2.3 *1.1.1.22 (Subgoal *1.1.1/1.2.3) is pushed for proof by induction. Subgoal *1.1.1/1.2.2 *1.1.1.23 (Subgoal *1.1.1/1.2.2) is pushed for proof by induction. Subgoal *1.1.1/1.2.1 Subgoal *1.1.1/1.2.1' *1.1.1.24 (Subgoal *1.1.1/1.2.1') is pushed for proof by induction. Subgoal *1.1.1/1.1 Subgoal *1.1.1/1.1.3 *1.1.1.25 (Subgoal *1.1.1/1.1.3) is pushed for proof by induction. Subgoal *1.1.1/1.1.2 *1.1.1.26 (Subgoal *1.1.1/1.1.2) is pushed for proof by induction. Subgoal *1.1.1/1.1.1 *1.1.1.27 (Subgoal *1.1.1/1.1.1) is pushed for proof by induction. So we now return to *1.1.1.27, which is (IMPLIES (AND (NOT (CONSP IT)) (TRUE-LISTP ES) (EQUAL (CONS X1 IT) (MERGE2 (MSORT (EVENS (CONS X1 X6))) (MSORT ES))) (NOT (LEXORDER X3 X5)) (NOT (LEXORDER X1 X5)) (LEXORDER X1 X3)) (EQUAL (LIST* X5 X1 X3 IT) (MERGE2 (MSORT (CONS X1 (EVENS (CONS X5 X6)))) (MSORT (CONS X3 ES))))). Subgoal *1.1.1.27/11 Subgoal *1.1.1.27/11' Subgoal *1.1.1.27/11'' Subgoal *1.1.1.27/11''' Subgoal *1.1.1.27/11'4' Subgoal *1.1.1.27/11'5' Subgoal *1.1.1.27/11'6' Subgoal *1.1.1.27/11'7' Subgoal *1.1.1.27/11'8' Subgoal *1.1.1.27/11'9' Subgoal *1.1.1.27/11'10' Subgoal *1.1.1.27/11'11' *1.1.1.27.1 (Subgoal *1.1.1.27/11'11') is pushed for proof by induction. Subgoal *1.1.1.27/10 Subgoal *1.1.1.27/10' Subgoal *1.1.1.27/10'' Subgoal *1.1.1.27/10''' Subgoal *1.1.1.27/10'4' Subgoal *1.1.1.27/10'5' Subgoal *1.1.1.27/10'6' Subgoal *1.1.1.27/10'7' Subgoal *1.1.1.27/10'8' Subgoal *1.1.1.27/10'9' Subgoal *1.1.1.27/10'10' *1.1.1.27.2 (Subgoal *1.1.1.27/10'10') is pushed for proof by induction. Subgoal *1.1.1.27/9 Subgoal *1.1.1.27/8 Subgoal *1.1.1.27/8' Subgoal *1.1.1.27/8'' Subgoal *1.1.1.27/8''' Subgoal *1.1.1.27/8'4' Subgoal *1.1.1.27/8'5' Subgoal *1.1.1.27/8'6' Subgoal *1.1.1.27/8'7' Subgoal *1.1.1.27/8'8' Subgoal *1.1.1.27/8'9' Subgoal *1.1.1.27/8'10' *1.1.1.27.3 (Subgoal *1.1.1.27/8'10') is pushed for proof by induction. Subgoal *1.1.1.27/7 Subgoal *1.1.1.27/7' Subgoal *1.1.1.27/7'' Subgoal *1.1.1.27/7''' Subgoal *1.1.1.27/7'4' Subgoal *1.1.1.27/7'5' Subgoal *1.1.1.27/7'6' Subgoal *1.1.1.27/7'7' Subgoal *1.1.1.27/7'8' *1.1.1.27.4 (Subgoal *1.1.1.27/7'8') is pushed for proof by induction. Subgoal *1.1.1.27/6 Subgoal *1.1.1.27/5 Subgoal *1.1.1.27/4 Subgoal *1.1.1.27/3 Subgoal *1.1.1.27/2 Subgoal *1.1.1.27/2' Subgoal *1.1.1.27/2'' Subgoal *1.1.1.27/2''' Subgoal *1.1.1.27/2'4' Subgoal *1.1.1.27/2.2 *1.1.1.27.5 (Subgoal *1.1.1.27/2.2) is pushed for proof by induction. Subgoal *1.1.1.27/2.1 *1.1.1.27.6 (Subgoal *1.1.1.27/2.1) is pushed for proof by induction. Subgoal *1.1.1.27/1 Subgoal *1.1.1.27/1' Subgoal *1.1.1.27/1'' Subgoal *1.1.1.27/1''' Subgoal *1.1.1.27/1'4' Subgoal *1.1.1.27/1'5' *1.1.1.27.7 (Subgoal *1.1.1.27/1'5') is pushed for proof by induction. So we now return to *1.1.1.27.7, which is (IMPLIES (AND (NOT (CONSP IT)) (NOT (LEXORDER X3 X5)) (NOT (LEXORDER X1 X5)) (LEXORDER X1 X3)) (EQUAL (LIST* X5 X1 X3 IT) (MERGE2 (MSORT (CONS X1 (EVENS (CONS X5 X6)))) (LIST X3)))). No induction schemes are suggested by *1.1.1.27.7. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ISORT-IS-MSORT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION EVENS) (:DEFINITION INSERT) (:DEFINITION ISORT) (:DEFINITION MERGE2) (:DEFINITION MSORT) (:DEFINITION NOT) (:DEFINITION ODDS) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART EVENS) (:EXECUTABLE-COUNTERPART ISORT) (:EXECUTABLE-COUNTERPART MSORT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:FORWARD-CHAINING LEXORDER-ANTI-SYMMETRIC) (:FORWARD-CHAINING LEXORDER-TOTAL) (:INDUCTION EVENS) (:INDUCTION INSERT) (:INDUCTION ISORT) (:INDUCTION MSORT) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-CDR) (:REWRITE LEXORDER-REFLEXIVE) (:REWRITE LEXORDER-TRANSITIVE) (:TYPE-PRESCRIPTION EVENS) (:TYPE-PRESCRIPTION LEXORDER) (:TYPE-PRESCRIPTION ODDS)) Warnings: Subsume Time: 0.93 seconds (prove: 0.89, print: 0.03, other: 0.00) --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint- summary-limit. --- *** Key checkpoint at the top level: *** Goal (EQUAL (ISORT X) (MSORT X)) *** Key checkpoint under a top-level induction: *** Subgoal *1/3'4' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (EQUAL (ISORT (EVENS X)) (MSORT (EVENS X))) (EQUAL (ISORT (EVENS (CDR X))) (MSORT (EVENS (CDR X))))) (EQUAL (INSERT (CAR X) (ISORT (CDR X))) (MERGE2 (ISORT (EVENS X)) (ISORT (EVENS (CDR X)))))) ACL2 Error in ( DEFTHM ISORT-IS-MSORT ...): See :DOC failure. ******** FAILED ******** ACL2 !>(verify (equal (isort x) (msort x))) ->: (in-theory (enable ordered-perms)) ->: comm 1. (:IN-THEORY (ENABLE ORDERED-PERMS)) << no event name specified at start >> ->: bash ***** Now entering the theorem prover ***** Goal is subsumed by a goal yet to be proved. Q.E.D. *** NO CHANGE *** -- Exactly one new goal was created by your PROVE command, and it has exactly the same hypotheses and conclusion as did the current goal. ->: th *** Top-level hypotheses: There are no top-level hypotheses. The current subterm is: (EQUAL (ISORT X) (MSORT X)) ->: sr ; show-rewrites 1. ORDERED-PERMS New term: (PERM (ISORT X) (MSORT X)) Hypotheses: ((TRUE-LISTP (ISORT X)) (TRUE-LISTP (MSORT X)) (ORDEREDP (ISORT X)) (ORDEREDP (MSORT X))) Equiv: EQUAL ->: r ; (r 1) ; (rewrite ordered-perms) Rewriting with ORDERED-PERMS. Creating four new goals: (MAIN . 1), (MAIN . 2), (MAIN . 3) and (MAIN . 4). ->: p (PERM (ISORT X) (MSORT X)) ->: prove ***** Now entering the theorem prover ***** Goal' Q.E.D. The proof of the current goal, MAIN, has been completed. However, the following subgoals remain to be proved: (MAIN . 1), (MAIN . 2), (MAIN . 3) and (MAIN . 4). Now proving (MAIN . 1). ->: prove ***** Now entering the theorem prover ***** *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (ISORT X). This suggestion was produced using the :induction rule ISORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit ISORT. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' Subgoal *1/2'4' Subgoal *1/2'5' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2'' (IMPLIES (AND (CONSP X) (TRUE-LISTP (ISORT (CDR X)))) (TRUE-LISTP (INSERT (CAR X) (ISORT (CDR X))))) *1.1 (Subgoal *1/2'5') is pushed for proof by induction. ]) Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (TRUE-LISTP IT) (TRUE-LISTP (INSERT X1 IT))). Subgoal *1.1/4 Subgoal *1.1/4' Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/2'' Subgoal *1.1/1 Subgoal *1.1/1' *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/2'' and Goal are COMPLETED! Q.E.D. The proof of the current goal, (MAIN . 1), has been completed, as have all of its subgoals. Now proving (MAIN . 2). ->: undo Undoing: :PROVE ->: bash ***** Now entering the theorem prover ***** Goal is subsumed by a goal yet to be proved. Q.E.D. *** NO CHANGE *** -- Exactly one new goal was created by your PROVE command, and it has exactly the same hypotheses and conclusion as did the current goal. ->: th *** Top-level hypotheses: There are no top-level hypotheses. The current subterm is: (TRUE-LISTP (ISORT X)) ->: exit Exiting.... NIL ACL2 !>(defthm true-listp-isort (true-listp (isort x))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (ISORT X). This suggestion was produced using the :induction rule ISORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit ISORT. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' Subgoal *1/2'4' Subgoal *1/2'5' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/2'' (IMPLIES (AND (CONSP X) (TRUE-LISTP (ISORT (CDR X)))) (TRUE-LISTP (INSERT (CAR X) (ISORT (CDR X))))) *1.1 (Subgoal *1/2'5') is pushed for proof by induction. ]) Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (TRUE-LISTP IT) (TRUE-LISTP (INSERT X1 IT))). Subgoal *1.1/4 Subgoal *1.1/4' Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/2'' Subgoal *1.1/1 Subgoal *1.1/1' *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/2'' and Goal are COMPLETED! Q.E.D. The storage of TRUE-LISTP-ISORT depends upon the :type- prescription rule TRUE-LISTP. Summary Form: ( DEFTHM TRUE-LISTP-ISORT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION INSERT) (:DEFINITION ISORT) (:DEFINITION NOT) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION INSERT) (:INDUCTION ISORT) (:INDUCTION TRUE-LISTP) (:REWRITE LEXORDER-REFLEXIVE) (:REWRITE LEXORDER-TRANSITIVE) (:TYPE-PRESCRIPTION INSERT) (:TYPE-PRESCRIPTION LEXORDER) (:TYPE-PRESCRIPTION TRUE-LISTP)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.01, other: 0.00) TRUE-LISTP-ISORT ACL2 !>(defthm true-listp-msort (true-listp (msort x))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Perhaps we can prove *1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (MSORT X). This suggestion was produced using the :induction rule MSORT. If we let (:P X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (NOT (ENDP (CDR X))) (:P (EVENS X)) (:P (ODDS X))) (:P X)) (IMPLIES (AND (NOT (ENDP X)) (ENDP (CDR X))) (:P X)) (IMPLIES (ENDP X) (:P X))). This induction is justified by the same argument used to admit MSORT. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 Subgoal *1/3' Subgoal *1/3'' Subgoal *1/3''' Subgoal *1/3'4' Subgoal *1/3'5' Subgoal *1/3'6' Subgoal *1/3'7' Subgoal *1/3'8' ([ A key checkpoint while proving *1 (descended from Goal): Subgoal *1/3''' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (TRUE-LISTP (MSORT (EVENS X))) (TRUE-LISTP (MSORT (EVENS (CDR X))))) (TRUE-LISTP (MERGE2 (MSORT (EVENS X)) (MSORT (EVENS (CDR X)))))) *1.1 (Subgoal *1/3'8') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 Subgoal *1/1' So we now return to *1.1, which is (IMPLIES (AND (TRUE-LISTP MT0) (TRUE-LISTP MT)) (TRUE-LISTP (MERGE2 MT0 MT))). Subgoal *1.1/6 Subgoal *1.1/6' Subgoal *1.1/5 Subgoal *1.1/4 Subgoal *1.1/4' Subgoal *1.1/3 Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/1 Subgoal *1.1/1' *1.1 and *1 are COMPLETED! Thus key checkpoints Subgoal *1/3''' and Goal are COMPLETED! Q.E.D. The storage of TRUE-LISTP-MSORT depends upon the :type- prescription rule TRUE-LISTP. Summary Form: ( DEFTHM TRUE-LISTP-MSORT ...) Rules: ((:DEFINITION ENDP) (:DEFINITION MERGE2) (:DEFINITION MSORT) (:DEFINITION NOT) (:DEFINITION ODDS) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION MERGE2) (:INDUCTION MSORT) (:INDUCTION TRUE-LISTP) (:REWRITE LEXORDER-REFLEXIVE) (:REWRITE LEXORDER-TRANSITIVE) (:TYPE-PRESCRIPTION EVENS) (:TYPE-PRESCRIPTION LEXORDER) (:TYPE-PRESCRIPTION MERGE2) (:TYPE-PRESCRIPTION TRUE-LISTP)) Warnings: None Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00) TRUE-LISTP-MSORT ACL2 !>(defthm isort-is-msort (equal (isort x) (msort x)) :hints (("Goal" :in-theory (enable ordered-perms)))) ACL2 Warning [Subsume] in ( DEFTHM ISORT-IS-MSORT ...): A newly proposed :REWRITE rule generated from ISORT-IS-MSORT probably subsumes the previously added :REWRITE rule ISORT- PERM, in the sense that the new rule will now probably be applied whenever the old rule would have been. Q.E.D. Summary Form: ( DEFTHM ISORT-IS-MSORT ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CONVERT-PERM-TO-HOW-MANY) (:REWRITE HOW-MANY-ISORT) (:REWRITE HOW-MANY-MSORT) (:REWRITE ORDERED-PERMS) (:REWRITE ORDEREDP-ISORT) (:REWRITE ORDEREDP-MSORT) (:REWRITE TRUE-LISTP-ISORT) (:REWRITE TRUE-LISTP-MSORT)) Warnings: Subsume Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) ISORT-IS-MSORT ACL2 !>