~/class$ acl2-4.3 Welcome to Clozure Common Lisp Version 1.8-dev-r14970M-trunk (DarwinX8664)! ACL2 Version 4.3 built September 5, 2011 13:09:21. Copyright (C) 2011 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-4-3 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/class/acl2-customization.lisp". ACL2 Version 4.3. Level 1. Cbd "/Users/kaufmann/class/". Distributed books directory "/Users/kaufmann/acl2/v4-3/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> ACL2 !> ACL2 !>Bye. ACL2 Version 4.3. Level 1. Cbd "/Users/kaufmann/class/". Distributed books directory "/Users/kaufmann/acl2/v4-3/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. 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)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) APP ACL2 !>(defun rev (x) (if (consp x) (app (rev (cdr x)) (list (car x))) 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)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) REV ACL2 !>(let ((x '(a b c)) (y '(d e f))) (rev (app x y))) (F E D C B A) ACL2 !>(let ((x '(a b c)) (y '(d e f))) (app (rev x) (rev y))) (C B A F E D) ACL2 !>(let ((x '(a b c)) (y '(d e f))) (app (rev y) (rev x))) (F E D C B A) ACL2 !>(let ((x '(a b c)) (y '(d e f))) (equal (rev (app x y)) (app (rev y) (rev x)))) T ACL2 !>(defthm rev-app (equal (rev (app x y)) (app (rev y) (rev x)))) Name the formula above *1. 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 X Y). This suggestion was produced using the :induction rules APP and REV. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y)) (IMPLIES (AND (CONSP X) (:P (CDR X) Y)) (:P X 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 (IMPLIES (NOT (CONSP X)) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, to Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (EQUAL (REV Y) (APP (REV Y) NIL))). We generalize this conjecture, replacing (REV Y) by RV. This produces Subgoal *1/2'' (IMPLIES (NOT (CONSP X)) (EQUAL RV (APP RV NIL))). We suspect that the term (NOT (CONSP X)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/2''' (EQUAL RV (APP RV NIL)). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Subgoal *1/1' (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (APP (REV (APP (CDR X) Y)) (LIST (CAR X))) (APP (REV Y) (APP (REV (CDR X)) (LIST (CAR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2)))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1/1''' (IMPLIES (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). We now use the hypothesis by substituting (APP (REV Y) (REV X2)) for (REV (APP X2 Y)) and throwing away the hypothesis. This produces Subgoal *1/1'4' (EQUAL (APP (APP (REV Y) (REV X2)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1)))). We generalize this conjecture, replacing (REV X2) by RV and (REV Y) by RV0. This produces Subgoal *1/1'5' (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1)))). Name the formula above *1.2. Perhaps we can prove *1.2 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 RV0 RV). This suggestion was produced using the :induction rule APP. If we let (:P RV RV0 X1) denote *1.2 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV0)) (:P RV RV0 X1)) (IMPLIES (AND (CONSP RV0) (:P RV (CDR RV0) X1)) (:P RV RV0 X1))). 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/2 (IMPLIES (NOT (CONSP RV0)) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP and primitive type reasoning. Subgoal *1.2/1 (IMPLIES (AND (CONSP RV0) (EQUAL (APP (APP (CDR RV0) RV) (LIST X1)) (APP (CDR RV0) (APP RV (LIST X1))))) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proof of *1.2. We therefore turn our attention to *1.1, which is (EQUAL RV (APP RV NIL)). Perhaps we can prove *1.1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (APP RV 'NIL). This suggestion was produced using the :induction rule APP. If we let (:P RV) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV)) (:P RV)) (IMPLIES (AND (CONSP RV) (:P (CDR RV))) (:P RV))). 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.1/2 (IMPLIES (NOT (CONSP RV)) (EQUAL RV (APP RV NIL))). This simplifies, using the :definition APP and primitive type reasoning, to Subgoal *1.1/2' (IMPLIES (NOT (CONSP RV)) (NOT RV)). Name the formula above *1.1.1. Subgoal *1.1/1 (IMPLIES (AND (CONSP RV) (EQUAL (CDR RV) (APP (CDR RV) NIL))) (EQUAL RV (APP RV NIL))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. So we now return to *1.1.1, which is (IMPLIES (NOT (CONSP RV)) (NOT RV)). No induction schemes are suggested by *1.1.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM REV-APP ...) Rules: ((:DEFINITION APP) (:DEFINITION REV) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION REV) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR)) Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00) Prover steps counted: 2443 --- 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 (REV (APP X Y)) (APP (REV Y) (REV X))) *** Key checkpoint under a top-level induction: *** Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (EQUAL (REV Y) (APP (REV Y) NIL))) ACL2 Error in ( DEFTHM REV-APP ...): See :DOC failure. ******** FAILED ******** ACL2 !>(let ((x 1)) (app x nil)) NIL ACL2 !>(defthm app-nil (implies (true-listp x) (equal x (app x nil)))) ACL2 Error in ( DEFTHM APP-NIL ...): A :REWRITE rule generated from APP-NIL is illegal because it rewrites the variable symbol X. See :DOC rewrite. Summary Form: ( DEFTHM APP-NIL ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( DEFTHM APP-NIL ...): See :DOC failure. ******** FAILED ******** ACL2 !>(defthm app-nil (implies (true-listp x) (equal (app x nil) x))) Name the formula above *1. 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 X 'NIL). This suggestion was produced using the :induction rules APP 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 APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But simplification reduces this to T, using the :definition TRUE-LISTP, the :executable-counterparts of APP, CONSP and EQUAL and primitive type reasoning. Subgoal *1/2 (IMPLIES (AND (CONSP X) (EQUAL (APP (CDR X) NIL) (CDR X)) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. Subgoal *1/1 (IMPLIES (AND (CONSP X) (NOT (TRUE-LISTP (CDR X))) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But we reduce the conjecture to T, by primitive type reasoning. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM APP-NIL ...) Rules: ((:DEFINITION APP) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION TRUE-LISTP) (:REWRITE CONS-CAR-CDR)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 171 APP-NIL ACL2 !>(defthm rev-app (equal (rev (app x y)) (app (rev y) (rev x)))) Name the formula above *1. 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 X Y). This suggestion was produced using the :induction rules APP and REV. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y)) (IMPLIES (AND (CONSP X) (:P (CDR X) Y)) (:P X 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 (IMPLIES (NOT (CONSP X)) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, to Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (EQUAL (REV Y) (APP (REV Y) NIL))). We generalize this conjecture, replacing (REV Y) by RV. This produces Subgoal *1/2'' (IMPLIES (NOT (CONSP X)) (EQUAL RV (APP RV NIL))). We suspect that the term (NOT (CONSP X)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/2''' (EQUAL RV (APP RV NIL)). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Subgoal *1/1' (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (APP (REV (APP (CDR X) Y)) (LIST (CAR X))) (APP (REV Y) (APP (REV (CDR X)) (LIST (CAR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2)))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1/1''' (IMPLIES (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). We now use the hypothesis by substituting (APP (REV Y) (REV X2)) for (REV (APP X2 Y)) and throwing away the hypothesis. This produces Subgoal *1/1'4' (EQUAL (APP (APP (REV Y) (REV X2)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1)))). We generalize this conjecture, replacing (REV X2) by RV and (REV Y) by RV0. This produces Subgoal *1/1'5' (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1)))). Name the formula above *1.2. Perhaps we can prove *1.2 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 RV0 RV). This suggestion was produced using the :induction rule APP. If we let (:P RV RV0 X1) denote *1.2 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV0)) (:P RV RV0 X1)) (IMPLIES (AND (CONSP RV0) (:P RV (CDR RV0) X1)) (:P RV RV0 X1))). 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/2 (IMPLIES (NOT (CONSP RV0)) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP and primitive type reasoning. Subgoal *1.2/1 (IMPLIES (AND (CONSP RV0) (EQUAL (APP (APP (CDR RV0) RV) (LIST X1)) (APP (CDR RV0) (APP RV (LIST X1))))) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proof of *1.2. We therefore turn our attention to *1.1, which is (EQUAL RV (APP RV NIL)). Perhaps we can prove *1.1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (APP RV 'NIL). This suggestion was produced using the :induction rule APP. If we let (:P RV) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV)) (:P RV)) (IMPLIES (AND (CONSP RV) (:P (CDR RV))) (:P RV))). 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.1/2 (IMPLIES (NOT (CONSP RV)) (EQUAL RV (APP RV NIL))). This simplifies, using the :definition APP and primitive type reasoning, to Subgoal *1.1/2' (IMPLIES (NOT (CONSP RV)) (NOT RV)). Name the formula above *1.1.1. Subgoal *1.1/1 (IMPLIES (AND (CONSP RV) (EQUAL (CDR RV) (APP (CDR RV) NIL))) (EQUAL RV (APP RV NIL))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. So we now return to *1.1.1, which is (IMPLIES (NOT (CONSP RV)) (NOT RV)). No induction schemes are suggested by *1.1.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM REV-APP ...) Rules: ((:DEFINITION APP) (:DEFINITION REV) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION REV) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR)) Time: 0.03 seconds (prove: 0.01, print: 0.01, other: 0.00) Prover steps counted: 2559 --- 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 (REV (APP X Y)) (APP (REV Y) (REV X))) *** Key checkpoint under a top-level induction: *** Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (EQUAL (REV Y) (APP (REV Y) NIL))) ACL2 Error in ( DEFTHM REV-APP ...): See :DOC failure. ******** FAILED ******** ACL2 !>(rev 3) NIL ACL2 !>(defthm true-listp-rev (true-listp (rev x))) Name the formula above *1. 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 (IMPLIES (NOT (CONSP X)) (TRUE-LISTP (REV X))). But simplification reduces this to T, using the :definition REV and the :executable-counterpart of TRUE-LISTP. Subgoal *1/1 (IMPLIES (AND (CONSP X) (TRUE-LISTP (REV (CDR X)))) (TRUE-LISTP (REV X))). This simplifies, using the :definition REV, to Subgoal *1/1' (IMPLIES (AND (CONSP X) (TRUE-LISTP (REV (CDR X)))) (TRUE-LISTP (APP (REV (CDR X)) (LIST (CAR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (TRUE-LISTP (REV X2))) (TRUE-LISTP (APP (REV X2) (LIST X1)))). This simplifies, using primitive type reasoning, to Subgoal *1/1''' (IMPLIES (TRUE-LISTP (REV X2)) (TRUE-LISTP (APP (REV X2) (LIST X1)))). We generalize this conjecture, replacing (REV X2) by RV. This produces Subgoal *1/1'4' (IMPLIES (TRUE-LISTP RV) (TRUE-LISTP (APP RV (LIST X1)))). Name the formula above *1.1. Perhaps we can prove *1.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 RV (CONS X1 'NIL)). This suggestion was produced using the :induction rules APP and TRUE-LISTP. If we let (:P RV X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV)) (:P RV X1)) (IMPLIES (AND (CONSP RV) (:P (CDR RV) X1)) (:P RV X1))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.1/3 (IMPLIES (AND (NOT (CONSP RV)) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST X1)))). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, the :executable-counterpart of CONSP and primitive type reasoning. Subgoal *1.1/2 (IMPLIES (AND (CONSP RV) (TRUE-LISTP (APP (CDR RV) (LIST X1))) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST X1)))). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, primitive type reasoning and the :type- prescription rule APP. Subgoal *1.1/1 (IMPLIES (AND (CONSP RV) (NOT (TRUE-LISTP (CDR RV))) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST X1)))). But we reduce the conjecture to T, by primitive type reasoning. That completes the proofs of *1.1 and *1. 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)) Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00) Prover steps counted: 751 TRUE-LISTP-REV ACL2 !>(defthm rev-app (equal (rev (app x y)) (app (rev y) (rev x)))) Name the formula above *1. 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 X Y). This suggestion was produced using the :induction rules APP and REV. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y)) (IMPLIES (AND (CONSP X) (:P (CDR X) Y)) (:P X 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 (IMPLIES (NOT (CONSP X)) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). But simplification reduces this to T, using the :definitions APP and REV, primitive type reasoning and the :rewrite rules APP-NIL and TRUE-LISTP-REV. Subgoal *1/1 (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Subgoal *1/1' (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (APP (REV (APP (CDR X) Y)) (LIST (CAR X))) (APP (REV Y) (APP (REV (CDR X)) (LIST (CAR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2)))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1/1''' (IMPLIES (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). We now use the hypothesis by substituting (APP (REV Y) (REV X2)) for (REV (APP X2 Y)) and throwing away the hypothesis. This produces Subgoal *1/1'4' (EQUAL (APP (APP (REV Y) (REV X2)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1)))). We generalize this conjecture, replacing (REV X2) by RV and (REV Y) by RV0. This produces Subgoal *1/1'5' (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1)))). Name the formula above *1.1. Perhaps we can prove *1.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 RV0 RV). This suggestion was produced using the :induction rule APP. If we let (:P RV RV0 X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV0)) (:P RV RV0 X1)) (IMPLIES (AND (CONSP RV0) (:P RV (CDR RV0) X1)) (:P RV RV0 X1))). 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.1/2 (IMPLIES (NOT (CONSP RV0)) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP and primitive type reasoning. Subgoal *1.1/1 (IMPLIES (AND (CONSP RV0) (EQUAL (APP (APP (CDR RV0) RV) (LIST X1)) (APP (CDR RV0) (APP RV (LIST X1))))) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proofs of *1.1 and *1. Q.E.D. Summary Form: ( DEFTHM REV-APP ...) Rules: ((:DEFINITION APP) (:DEFINITION REV) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION REV) (:REWRITE APP-NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE TRUE-LISTP-REV)) Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00) Prover steps counted: 2200 REV-APP ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN APP (X Y) ...) L 2 (DEFUN REV (X) ...) 3 (DEFTHM APP-NIL ...) 4 (DEFTHM TRUE-LISTP-REV ...) 5:x(DEFTHM REV-APP ...) ACL2 !>:u 4:x(DEFTHM TRUE-LISTP-REV ...) ACL2 !>:u 3:x(DEFTHM APP-NIL ...) ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN APP (X Y) ...) L 2 (DEFUN REV (X) ...) 3:x(DEFTHM APP-NIL ...) ACL2 !>(defthm true-listp-rev (true-listp (rev x))) Name the formula above *1. 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 (IMPLIES (NOT (CONSP X)) (TRUE-LISTP (REV X))). But simplification reduces this to T, using the :definition REV and the :executable-counterpart of TRUE-LISTP. Subgoal *1/1 (IMPLIES (AND (CONSP X) (TRUE-LISTP (REV (CDR X)))) (TRUE-LISTP (REV X))). This simplifies, using the :definition REV, to Subgoal *1/1' (IMPLIES (AND (CONSP X) (TRUE-LISTP (REV (CDR X)))) (TRUE-LISTP (APP (REV (CDR X)) (LIST (CAR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (TRUE-LISTP (REV X2))) (TRUE-LISTP (APP (REV X2) (LIST X1)))). This simplifies, using primitive type reasoning, to Subgoal *1/1''' (IMPLIES (TRUE-LISTP (REV X2)) (TRUE-LISTP (APP (REV X2) (LIST X1)))). We generalize this conjecture, replacing (REV X2) by RV. This produces Subgoal *1/1'4' (IMPLIES (TRUE-LISTP RV) (TRUE-LISTP (APP RV (LIST X1)))). Name the formula above *1.1. Perhaps we can prove *1.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 RV (CONS X1 'NIL)). This suggestion was produced using the :induction rules APP and TRUE-LISTP. If we let (:P RV X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV)) (:P RV X1)) (IMPLIES (AND (CONSP RV) (:P (CDR RV) X1)) (:P RV X1))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.1/3 (IMPLIES (AND (NOT (CONSP RV)) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST X1)))). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, the :executable-counterpart of CONSP and primitive type reasoning. Subgoal *1.1/2 (IMPLIES (AND (CONSP RV) (TRUE-LISTP (APP (CDR RV) (LIST X1))) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST X1)))). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, primitive type reasoning and the :type- prescription rule APP. Subgoal *1.1/1 (IMPLIES (AND (CONSP RV) (NOT (TRUE-LISTP (CDR RV))) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST X1)))). But we reduce the conjecture to T, by primitive type reasoning. That completes the proofs of *1.1 and *1. 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)) Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) Prover steps counted: 751 TRUE-LISTP-REV ACL2 !>:u 3:x(DEFTHM APP-NIL ...) ACL2 !>(defthm rev-app (equal (rev (app x y)) (app (rev y) (rev x)))) Name the formula above *1. 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 X Y). This suggestion was produced using the :induction rules APP and REV. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y)) (IMPLIES (AND (CONSP X) (:P (CDR X) Y)) (:P X 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 (IMPLIES (NOT (CONSP X)) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, to Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (EQUAL (REV Y) (APP (REV Y) NIL))). We generalize this conjecture, replacing (REV Y) by RV. This produces Subgoal *1/2'' (IMPLIES (NOT (CONSP X)) (EQUAL RV (APP RV NIL))). We suspect that the term (NOT (CONSP X)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/2''' (EQUAL RV (APP RV NIL)). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Subgoal *1/1' (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (APP (REV (APP (CDR X) Y)) (LIST (CAR X))) (APP (REV Y) (APP (REV (CDR X)) (LIST (CAR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2)))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1/1''' (IMPLIES (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). We now use the hypothesis by substituting (APP (REV Y) (REV X2)) for (REV (APP X2 Y)) and throwing away the hypothesis. This produces Subgoal *1/1'4' (EQUAL (APP (APP (REV Y) (REV X2)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1)))). We generalize this conjecture, replacing (REV X2) by RV and (REV Y) by RV0. This produces Subgoal *1/1'5' (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1)))). Name the formula above *1.2. Perhaps we can prove *1.2 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 RV0 RV). This suggestion was produced using the :induction rule APP. If we let (:P RV RV0 X1) denote *1.2 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV0)) (:P RV RV0 X1)) (IMPLIES (AND (CONSP RV0) (:P RV (CDR RV0) X1)) (:P RV RV0 X1))). 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/2 (IMPLIES (NOT (CONSP RV0)) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP and primitive type reasoning. Subgoal *1.2/1 (IMPLIES (AND (CONSP RV0) (EQUAL (APP (APP (CDR RV0) RV) (LIST X1)) (APP (CDR RV0) (APP RV (LIST X1))))) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proof of *1.2. We therefore turn our attention to *1.1, which is (EQUAL RV (APP RV NIL)). Perhaps we can prove *1.1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (APP RV 'NIL). This suggestion was produced using the :induction rule APP. If we let (:P RV) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV)) (:P RV)) (IMPLIES (AND (CONSP RV) (:P (CDR RV))) (:P RV))). 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.1/2 (IMPLIES (NOT (CONSP RV)) (EQUAL RV (APP RV NIL))). This simplifies, using the :definition APP and primitive type reasoning, to Subgoal *1.1/2' (IMPLIES (NOT (CONSP RV)) (NOT RV)). Name the formula above *1.1.1. Subgoal *1.1/1 (IMPLIES (AND (CONSP RV) (EQUAL (CDR RV) (APP (CDR RV) NIL))) (EQUAL RV (APP RV NIL))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. So we now return to *1.1.1, which is (IMPLIES (NOT (CONSP RV)) (NOT RV)). No induction schemes are suggested by *1.1.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM REV-APP ...) Rules: ((:DEFINITION APP) (:DEFINITION REV) (:ELIM CAR-CDR-ELIM) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION REV) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR)) Time: 0.03 seconds (prove: 0.02, print: 0.01, other: 0.00) Prover steps counted: 2559 --- 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 (REV (APP X Y)) (APP (REV Y) (REV X))) *** Key checkpoint under a top-level induction: *** Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (EQUAL (REV Y) (APP (REV Y) NIL))) ACL2 Error in ( DEFTHM REV-APP ...): See :DOC failure. ******** FAILED ******** ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN APP (X Y) ...) L 2 (DEFUN REV (X) ...) 3:x(DEFTHM APP-NIL ...) ACL2 !>(defthm app-nil (implies (force (true-listp x)) (equal (app x nil) x))) ACL2 Error in ( DEFTHM APP-NIL ...): The name APP-NIL is in use as a theorem. The redefinition feature is currently off. See :DOC ld-redefinition-action. Note: APP-NIL was previously defined at the top level. Summary Form: ( DEFTHM APP-NIL ...) Rules: NIL Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) ACL2 Error in ( DEFTHM APP-NIL ...): See :DOC failure. ******** FAILED ******** ACL2 !>:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN APP (X Y) ...) L 2 (DEFUN REV (X) ...) 3:x(DEFTHM APP-NIL ...) ACL2 !>:u L 2:x(DEFUN REV (X) ...) ACL2 !>(defthm app-nil (implies (force (true-listp x)) (equal (app x nil) x))) By the simple :definition FORCE we reduce the conjecture to Goal' (IMPLIES (TRUE-LISTP X) (EQUAL (APP X NIL) X)). Name the formula above *1. 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 X 'NIL). This suggestion was produced using the :induction rules APP 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 APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But simplification reduces this to T, using the :definition TRUE-LISTP, the :executable-counterparts of APP, CONSP and EQUAL and primitive type reasoning. Subgoal *1/2 (IMPLIES (AND (CONSP X) (EQUAL (APP (CDR X) NIL) (CDR X)) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. Subgoal *1/1 (IMPLIES (AND (CONSP X) (NOT (TRUE-LISTP (CDR X))) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But we reduce the conjecture to T, by primitive type reasoning. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM APP-NIL ...) Rules: ((:DEFINITION APP) (:DEFINITION FORCE) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION TRUE-LISTP) (:REWRITE CONS-CAR-CDR)) Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) Prover steps counted: 173 APP-NIL ACL2 !>(defthm rev-app (equal (rev (app x y)) (app (rev y) (rev x)))) Name the formula above *1. 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 X Y). This suggestion was produced using the :induction rules APP and REV. If we let (:P X Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X)) (:P X Y)) (IMPLIES (AND (CONSP X) (:P (CDR X) Y)) (:P X 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 (IMPLIES (NOT (CONSP X)) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). But forced simplification reduces this to T, using the :definitions APP and REV, primitive type reasoning and the :rewrite rule APP-NIL (forced). Subgoal *1/1 (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (REV (APP X Y)) (APP (REV Y) (REV X)))). This simplifies, using the :definitions APP and REV, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Subgoal *1/1' (IMPLIES (AND (CONSP X) (EQUAL (REV (APP (CDR X) Y)) (APP (REV Y) (REV (CDR X))))) (EQUAL (APP (REV (APP (CDR X) Y)) (LIST (CAR X))) (APP (REV Y) (APP (REV (CDR X)) (LIST (CAR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2)))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1/1''' (IMPLIES (EQUAL (REV (APP X2 Y)) (APP (REV Y) (REV X2))) (EQUAL (APP (REV (APP X2 Y)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1))))). We now use the hypothesis by substituting (APP (REV Y) (REV X2)) for (REV (APP X2 Y)) and throwing away the hypothesis. This produces Subgoal *1/1'4' (EQUAL (APP (APP (REV Y) (REV X2)) (LIST X1)) (APP (REV Y) (APP (REV X2) (LIST X1)))). We generalize this conjecture, replacing (REV X2) by RV and (REV Y) by RV0. This produces Subgoal *1/1'5' (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1)))). Name the formula above *1.1. Perhaps we can prove *1.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 RV0 RV). This suggestion was produced using the :induction rule APP. If we let (:P RV RV0 X1) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV0)) (:P RV RV0 X1)) (IMPLIES (AND (CONSP RV0) (:P RV (CDR RV0) X1)) (:P RV RV0 X1))). 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.1/2 (IMPLIES (NOT (CONSP RV0)) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP and primitive type reasoning. Subgoal *1.1/1 (IMPLIES (AND (CONSP RV0) (EQUAL (APP (APP (CDR RV0) RV) (LIST X1)) (APP (CDR RV0) (APP RV (LIST X1))))) (EQUAL (APP (APP RV0 RV) (LIST X1)) (APP RV0 (APP RV (LIST X1))))). But simplification reduces this to T, using the :definition APP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. That completes the proofs of *1.1 and *1. q.e.d. (given one forced hypothesis) Modulo the following forced goal, that completes the proof of the input Goal. See :DOC forcing-round. [1]Goal, below, will focus on (TRUE-LISTP (REV Y)), which was forced in Subgoal *1/2 by applying (:REWRITE APP-NIL) to (APP (REV Y) NIL). We now undertake Forcing Round 1. [1]Goal (IMPLIES (NOT (CONSP X)) (TRUE-LISTP (REV Y))). Name the formula above [1]*1. Perhaps we can prove [1]*1 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (REV Y). This suggestion was produced using the :induction rule REV. If we let (:P X Y) denote [1]*1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP Y)) (:P X Y)) (IMPLIES (AND (CONSP Y) (:P X (CDR Y))) (:P X Y))). 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. [1]Subgoal *1/2 (IMPLIES (AND (NOT (CONSP Y)) (NOT (CONSP X))) (TRUE-LISTP (REV Y))). But simplification reduces this to T, using the :definition REV and the :executable-counterpart of TRUE-LISTP. [1]Subgoal *1/1 (IMPLIES (AND (CONSP Y) (TRUE-LISTP (REV (CDR Y))) (NOT (CONSP X))) (TRUE-LISTP (REV Y))). This simplifies, using the :definition REV, to [1]Subgoal *1/1' (IMPLIES (AND (CONSP Y) (TRUE-LISTP (REV (CDR Y))) (NOT (CONSP X))) (TRUE-LISTP (APP (REV (CDR Y)) (LIST (CAR Y))))). The destructor terms (CAR Y) and (CDR Y) can be eliminated by using CAR-CDR-ELIM to replace Y by (CONS Y1 Y2), (CAR Y) by Y1 and (CDR Y) by Y2. This produces the following goal. [1]Subgoal *1/1'' (IMPLIES (AND (CONSP (CONS Y1 Y2)) (TRUE-LISTP (REV Y2)) (NOT (CONSP X))) (TRUE-LISTP (APP (REV Y2) (LIST Y1)))). This simplifies, using primitive type reasoning, to [1]Subgoal *1/1''' (IMPLIES (AND (TRUE-LISTP (REV Y2)) (NOT (CONSP X))) (TRUE-LISTP (APP (REV Y2) (LIST Y1)))). We generalize this conjecture, replacing (REV Y2) by RV. This produces [1]Subgoal *1/1'4' (IMPLIES (AND (TRUE-LISTP RV) (NOT (CONSP X))) (TRUE-LISTP (APP RV (LIST Y1)))). We suspect that the term (NOT (CONSP X)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove [1]Subgoal *1/1'5' (IMPLIES (TRUE-LISTP RV) (TRUE-LISTP (APP RV (LIST Y1)))). Name the formula above [1]*1.1. Perhaps we can prove [1]*1.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 RV (CONS Y1 'NIL)). This suggestion was produced using the :induction rules APP and TRUE-LISTP. If we let (:P RV Y1) denote [1]*1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP RV)) (:P RV Y1)) (IMPLIES (AND (CONSP RV) (:P (CDR RV) Y1)) (:P RV Y1))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. [1]Subgoal *1.1/3 (IMPLIES (AND (NOT (CONSP RV)) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST Y1)))). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, the :executable-counterpart of CONSP and primitive type reasoning. [1]Subgoal *1.1/2 (IMPLIES (AND (CONSP RV) (TRUE-LISTP (APP (CDR RV) (LIST Y1))) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST Y1)))). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, primitive type reasoning and the :type- prescription rule APP. [1]Subgoal *1.1/1 (IMPLIES (AND (CONSP RV) (NOT (TRUE-LISTP (CDR RV))) (TRUE-LISTP RV)) (TRUE-LISTP (APP RV (LIST Y1)))). But we reduce the conjecture to T, by primitive type reasoning. That completes the proofs of [1]*1.1 and [1]*1. Q.E.D. Summary Form: ( DEFTHM REV-APP ...) 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) (:REWRITE APP-NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION APP)) Time: 0.03 seconds (prove: 0.02, print: 0.02, other: 0.00) Prover steps counted: 3061 REV-APP ACL2 !>:ubt! 1 0:x(EXIT-BOOT-STRAP-MODE) ACL2 !>(defun app (x y) (cond ((endp x) y) (t (cons (car x) (app (cdr x) 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)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) APP ACL2 !>(defun rotate (n x) (cond ((zp n) x) (t (rotate (1- n) (app (cdr x) (list (car x))))))) The admission of ROTATE 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 N). We observe that the type of ROTATE is described by the theorem (OR (CONSP (ROTATE N X)) (EQUAL (ROTATE N X) X)). We used primitive type reasoning and the :type-prescription rule APP. Summary Form: ( DEFUN ROTATE ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION APP)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ROTATE ACL2 !>(rotate 3 '(a b c d e f g)) (D E F G A B C) ACL2 !>(rotate 7 '(a b c d e f g)) (A B C D E F G) ACL2 !>:pe len V -6885 (DEFUN LEN (X) "Documentation available via :doc" (DECLARE (XARGS :GUARD T :MODE :LOGIC)) (IF (CONSP X) (+ 1 (LEN (CDR X))) 0)) ACL2 !>(let ((x (cons 1 2))) (equal (rotate (len x) x) x)) ACL2 Error in TOP-LEVEL: The guard for the function call (ENDP X), which is (OR (CONSP X) (EQUAL X NIL)), is violated by the arguments in the call (ENDP 2). The guard is being checked because this function is a primitive and a "safe" mode is being used for defconst, defpkg, macroexpansion, or another operation where safe mode is required. To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>:set-guard-checking :none Turning off guard checking entirely. To allow execution in raw Lisp for functions with guards other than T, while continuing to mask guard violations, :SET-GUARD-CHECKING NIL. See :DOC set-guard-checking. ACL2 >(let ((x (cons 1 2))) (equal (rotate (len x) x) x)) NIL ACL2 >(let ((x (cons 1 2))) (rotate (len x) x)) (1) ACL2 >(trace$ rotate) ((ROTATE)) ACL2 >(let ((x (cons 1 2))) (rotate (len x) x)) 1> (ACL2_*1*_ACL2::ROTATE 1 (1 . 2)) 2> (ACL2_*1*_ACL2::ROTATE 0 (1)) <2 (ACL2_*1*_ACL2::ROTATE (1)) <1 (ACL2_*1*_ACL2::ROTATE (1)) (1) ACL2 >(trace$ app) ((APP)) ACL2 >(let ((x (cons 1 2))) (rotate (len x) x)) 1> (ACL2_*1*_ACL2::ROTATE 1 (1 . 2)) 2> (ACL2_*1*_ACL2::APP 2 (1)) <2 (ACL2_*1*_ACL2::APP (1)) 2> (ACL2_*1*_ACL2::ROTATE 0 (1)) <2 (ACL2_*1*_ACL2::ROTATE (1)) <1 (ACL2_*1*_ACL2::ROTATE (1)) (1) ACL2 >(untrace$) (APP ROTATE) ACL2 >(defthm rotate-len (implies (true-listp x) (equal (rotate (len x) x) x))) Name the formula above *1. 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 (LEN X). This suggestion was produced using the :induction rules LEN 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 LEN. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X)) (EQUAL (ROTATE (LEN X) X) X)). But simplification reduces this to T, using the :definition TRUE-LISTP, the :executable-counterparts of CONSP, EQUAL, LEN and ROTATE and primitive type reasoning. Subgoal *1/2 (IMPLIES (AND (CONSP X) (EQUAL (ROTATE (LEN (CDR X)) (CDR X)) (CDR X)) (TRUE-LISTP X)) (EQUAL (ROTATE (LEN X) X) X)). This simplifies, using the :definitions LEN and TRUE-LISTP, to Subgoal *1/2' (IMPLIES (AND (CONSP X) (EQUAL (ROTATE (LEN (CDR X)) (CDR X)) (CDR X)) (TRUE-LISTP (CDR X))) (EQUAL (ROTATE (+ 1 (LEN (CDR X))) X) X)). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2'' (IMPLIES (AND (CONSP (CONS X1 X2)) (EQUAL (ROTATE (LEN X2) X2) X2) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 (LEN X2)) (CONS X1 X2)) (CONS X1 X2))). This simplifies, using primitive type reasoning, to Subgoal *1/2''' (IMPLIES (AND (EQUAL (ROTATE (LEN X2) X2) X2) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 (LEN X2)) (CONS X1 X2)) (CONS X1 X2))). We now use the first hypothesis by cross-fertilizing (ROTATE (LEN X2) X2) for X2 and throwing away the hypothesis. This produces Subgoal *1/2'4' (IMPLIES (TRUE-LISTP X2) (EQUAL (ROTATE (+ 1 (LEN X2)) (CONS X1 X2)) (CONS X1 (ROTATE (LEN X2) X2)))). We generalize this conjecture, replacing (LEN X2) by I and restricting the type of the new variable I to be that of the term it replaces, as established by LEN. This produces Subgoal *1/2'5' (IMPLIES (AND (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). By case analysis we reduce the conjecture to Subgoal *1/2'6' (IMPLIES (AND (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (AND (CONSP X) (NOT (TRUE-LISTP (CDR X))) (TRUE-LISTP X)) (EQUAL (ROTATE (LEN X) X) X)). But we reduce the conjecture to T, by primitive type reasoning. So we now return to *1.1, which is (IMPLIES (AND (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). Perhaps we can prove *1.1 by induction. Two induction schemes are suggested by this conjecture. However, one of these is flawed and so we are left with one viable candidate. We will induct according to a scheme suggested by (ROTATE I X2). This suggestion was produced using the :induction rule ROTATE. If we let (:P I X1 X2) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP I)) (:P (+ -1 I) X1 (APP (CDR X2) (LIST (CAR X2))))) (:P I X1 X2)) (IMPLIES (ZP I) (:P I X1 X2))). This induction is justified by the same argument used to admit ROTATE. Note, however, that the unmeasured variable X2 is being instantiated. When applied to the goal at hand the above induction scheme produces five nontautological subgoals. Subgoal *1.1/5 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ 1 -1 I) (CONS X1 (APP (CDR X2) (LIST (CAR X2))))) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2)))))) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions ROTATE and TRUE-LISTP, the :executable-counterparts of APP, CAR, CDR, CONS and CONSP and primitive type reasoning, to the following two conjectures. Subgoal *1.1/5.2 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ 1 -1 I) (CONS X1 (APP (CDR X2) (LIST (CAR X2))))) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2)))))) (<= 0 I) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2))))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.1/5.2' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (EQUAL (ROTATE (+ 1 -1 I) (CONS X1 (APP X4 (LIST X3)))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3))))) (<= 0 I) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ 1 I) (LIST* X1 X3 X4)) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). This simplifies, using primitive type reasoning, to Subgoal *1.1/5.2'' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ 1 -1 I) (CONS X1 (APP X4 (LIST X3)))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3))))) (<= 0 I) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ 1 I) (LIST* X1 X3 X4)) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). We now use the second hypothesis by substituting (ROTATE (+ 1 -1 I) (CONS X1 (APP X4 (LIST X3)))) for (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))) and throwing away the hypothesis. This produces Subgoal *1.1/5.2''' (IMPLIES (AND (NOT (ZP I)) (<= 0 I) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ 1 I) (LIST* X1 X3 X4)) (ROTATE (+ 1 -1 I) (CONS X1 (APP X4 (LIST X3)))))). Name the formula above *1.1.1. Subgoal *1.1/5.1 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ 1 -1 I) (CONS X1 '(NIL))) (CONS X1 (ROTATE (+ -1 I) '(NIL)))) (<= 0 I) (NOT X2)) (EQUAL (ROTATE (+ 1 I) (LIST X1)) (CONS X1 (ROTATE I NIL)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition ROTATE and the :executable- counterparts of APP, CAR, CDR and CONS, to Subgoal *1.1/5.1' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ 1 -1 I) (CONS X1 '(NIL))) (CONS X1 (ROTATE (+ -1 I) '(NIL)))) (<= 0 I)) (EQUAL (ROTATE (+ 1 I) (LIST X1)) (CONS X1 (ROTATE (+ -1 I) '(NIL))))). We now use the second hypothesis by substituting (ROTATE (+ 1 -1 I) (CONS X1 '(NIL))) for (CONS X1 (ROTATE (+ -1 I) '(NIL))) and throwing away the hypothesis. This produces Subgoal *1.1/5.1'' (IMPLIES (AND (NOT (ZP I)) (<= 0 I)) (EQUAL (ROTATE (+ 1 I) (LIST X1)) (ROTATE (+ 1 -1 I) (CONS X1 '(NIL))))). Name the formula above *1.1.2. Subgoal *1.1/4 (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (APP (CDR X2) (LIST (CAR X2))))) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions ROTATE and TRUE-LISTP, the :executable-counterparts of APP, CAR, CDR, CONS, CONSP and TRUE-LISTP and primitive type reasoning, to Subgoal *1.1/4' (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (APP (CDR X2) (LIST (CAR X2))))) (<= 0 I) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2))))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.1/4'' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (NOT (TRUE-LISTP (APP X4 (LIST X3)))) (<= 0 I) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ 1 I) (LIST* X1 X3 X4)) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). This simplifies, using primitive type reasoning, to Subgoal *1.1/4''' (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (APP X4 (LIST X3)))) (<= 0 I) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ 1 I) (LIST* X1 X3 X4)) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). We generalize this conjecture, replacing (APP X4 (LIST X3)) by L and restricting the type of the new variable L to be that of the term it replaces, as established by primitive type reasoning and APP. This produces Subgoal *1.1/4'4' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP I)) (NOT (TRUE-LISTP L)) (<= 0 I) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ 1 I) (LIST* X1 X3 X4)) (CONS X1 (ROTATE (+ -1 I) L)))). By case analysis we reduce the conjecture to Subgoal *1.1/4'5' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP I)) (<= 0 I) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ 1 I) (LIST* X1 X3 X4)) (CONS X1 (ROTATE (+ -1 I) L)))). Name the formula above *1.1.3. Subgoal *1.1/3 (IMPLIES (AND (NOT (ZP I)) (< (+ -1 I) 0) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.1/2 (IMPLIES (AND (NOT (ZP I)) (NOT (INTEGERP (+ -1 I))) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.1/1 (IMPLIES (AND (ZP I) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE (+ 1 I) (CONS X1 X2)) (CONS X1 (ROTATE I X2)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of <, BINARY-+, INTEGERP, NOT and ZP and linear arithmetic, to Subgoal *1.1/1' (IMPLIES (TRUE-LISTP X2) (EQUAL (ROTATE 1 (CONS X1 X2)) (CONS X1 (ROTATE 0 X2)))). This simplifies, using the :definition ROTATE and the :executable- counterpart of ZP, to Subgoal *1.1/1'' (IMPLIES (TRUE-LISTP X2) (EQUAL (ROTATE 1 (CONS X1 X2)) (CONS X1 X2))). Name the formula above *1.1.4. Perhaps we can prove *1.1.4 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (TRUE-LISTP X2). This suggestion was produced using the :induction rule TRUE-LISTP. If we let (:P X1 X2) denote *1.1.4 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X2)) (:P X1 X2)) (IMPLIES (AND (CONSP X2) (:P X1 (CDR X2))) (:P X1 X2))). This induction is justified by the same argument used to admit TRUE-LISTP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.1.4/3 (IMPLIES (AND (NOT (CONSP X2)) (TRUE-LISTP X2)) (EQUAL (ROTATE 1 (CONS X1 X2)) (CONS X1 X2))). This simplifies, using the :definition TRUE-LISTP, the :executable- counterpart of CONSP and primitive type reasoning, to Subgoal *1.1.4/3' (IMPLIES (NOT X2) (EQUAL (ROTATE 1 (LIST X1)) (LIST X1))). This simplifies, using trivial observations, to Subgoal *1.1.4/3'' (EQUAL (ROTATE 1 (LIST X1)) (LIST X1)). Name the formula above *1.1.4.1. Subgoal *1.1.4/2 (IMPLIES (AND (CONSP X2) (EQUAL (ROTATE 1 (CONS X1 (CDR X2))) (CONS X1 (CDR X2))) (TRUE-LISTP X2)) (EQUAL (ROTATE 1 (CONS X1 X2)) (CONS X1 X2))). This simplifies, using the :definition TRUE-LISTP, to Subgoal *1.1.4/2' (IMPLIES (AND (CONSP X2) (EQUAL (ROTATE 1 (CONS X1 (CDR X2))) (CONS X1 (CDR X2))) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE 1 (CONS X1 X2)) (CONS X1 X2))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.1.4/2'' (IMPLIES (AND (CONSP (CONS X3 X4)) (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). This simplifies, using primitive type reasoning, to Subgoal *1.1.4/2''' (IMPLIES (AND (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). Name the formula above *1.1.4.2. Subgoal *1.1.4/1 (IMPLIES (AND (CONSP X2) (NOT (TRUE-LISTP (CDR X2))) (TRUE-LISTP X2)) (EQUAL (ROTATE 1 (CONS X1 X2)) (CONS X1 X2))). But we reduce the conjecture to T, by primitive type reasoning. So we now return to *1.1.4.2, which is (IMPLIES (AND (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). Perhaps we can prove *1.1.4.2 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (TRUE-LISTP X4). This suggestion was produced using the :induction rule TRUE-LISTP. If we let (:P X1 X3 X4) denote *1.1.4.2 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X4)) (:P X1 X3 X4)) (IMPLIES (AND (CONSP X4) (:P X1 X3 (CDR X4))) (:P X1 X3 X4))). This induction is justified by the same argument used to admit TRUE-LISTP. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1.1.4.2/4 (IMPLIES (AND (NOT (CONSP X4)) (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). This simplifies, using the :definition TRUE-LISTP, the :executable- counterpart of CONSP and primitive type reasoning, to Subgoal *1.1.4.2/4' (IMPLIES (AND (EQUAL (ROTATE 1 (LIST X1)) (LIST X1)) (NOT X4)) (EQUAL (ROTATE 1 (LIST X1 X3)) (LIST X1 X3))). This simplifies, using trivial observations, to Subgoal *1.1.4.2/4'' (IMPLIES (EQUAL (ROTATE 1 (LIST X1)) (LIST X1)) (EQUAL (ROTATE 1 (LIST X1 X3)) (LIST X1 X3))). Name the formula above *1.1.4.2.1. Subgoal *1.1.4.2/3 (IMPLIES (AND (CONSP X4) (EQUAL (ROTATE 1 (LIST* X1 X3 (CDR X4))) (LIST* X1 X3 (CDR X4))) (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). This simplifies, using the :definition TRUE-LISTP, to Subgoal *1.1.4.2/3' (IMPLIES (AND (CONSP X4) (EQUAL (ROTATE 1 (LIST* X1 X3 (CDR X4))) (LIST* X1 X3 (CDR X4))) (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP (CDR X4))) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). The destructor terms (CAR X4) and (CDR X4) can be eliminated by using CAR-CDR-ELIM to replace X4 by (CONS X5 X6), (CAR X4) by X5 and (CDR X4) by X6. This produces the following goal. Subgoal *1.1.4.2/3'' (IMPLIES (AND (CONSP (CONS X5 X6)) (EQUAL (ROTATE 1 (LIST* X1 X3 X6)) (LIST* X1 X3 X6)) (EQUAL (ROTATE 1 (LIST* X1 X5 X6)) (LIST* X1 X5 X6)) (TRUE-LISTP X6)) (EQUAL (ROTATE 1 (LIST* X1 X3 X5 X6)) (LIST* X1 X3 X5 X6))). This simplifies, using primitive type reasoning, to Subgoal *1.1.4.2/3''' (IMPLIES (AND (EQUAL (ROTATE 1 (LIST* X1 X3 X6)) (LIST* X1 X3 X6)) (EQUAL (ROTATE 1 (LIST* X1 X5 X6)) (LIST* X1 X5 X6)) (TRUE-LISTP X6)) (EQUAL (ROTATE 1 (LIST* X1 X3 X5 X6)) (LIST* X1 X3 X5 X6))). Name the formula above *1.1.4.2.2. Subgoal *1.1.4.2/2 (IMPLIES (AND (CONSP X4) (NOT (TRUE-LISTP (CDR X4))) (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.1.4.2/1 (IMPLIES (AND (CONSP X4) (NOT (EQUAL (ROTATE 1 (CONS X1 (CDR X4))) (CONS X1 (CDR X4)))) (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). This simplifies, using the :definition TRUE-LISTP, to Subgoal *1.1.4.2/1' (IMPLIES (AND (CONSP X4) (NOT (EQUAL (ROTATE 1 (CONS X1 (CDR X4))) (CONS X1 (CDR X4)))) (EQUAL (ROTATE 1 (CONS X1 X4)) (CONS X1 X4)) (TRUE-LISTP (CDR X4))) (EQUAL (ROTATE 1 (LIST* X1 X3 X4)) (LIST* X1 X3 X4))). The destructor terms (CAR X4) and (CDR X4) can be eliminated by using CAR-CDR-ELIM to replace X4 by (CONS X5 X6), (CAR X4) by X5 and (CDR X4) by X6. This produces the following goal. Subgoal *1.1.4.2/1'' (IMPLIES (AND (CONSP (CONS X5 X6)) (NOT (EQUAL (ROTATE 1 (CONS X1 X6)) (CONS X1 X6))) (EQUAL (ROTATE 1 (LIST* X1 X5 X6)) (LIST* X1 X5 X6)) (TRUE-LISTP X6)) (EQUAL (ROTATE 1 (LIST* X1 X3 X5 X6)) (LIST* X1 X3 X5 X6))). This simplifies, using primitive type reasoning, to Subgoal *1.1.4.2/1''' (IMPLIES (AND (NOT (EQUAL (ROTATE 1 (CONS X1 X6)) (CONS X1 X6))) (EQUAL (ROTATE 1 (LIST* X1 X5 X6)) (LIST* X1 X5 X6)) (TRUE-LISTP X6)) (EQUAL (ROTATE 1 (LIST* X1 X3 X5 X6)) (LIST* X1 X3 X5 X6))). Name the formula above *1.1.4.2.3. The formula above is subsumed by one of its parents, *1.1.4, which we're in the process of trying to prove by induction. When an inductive proof pushes a subgoal for induction that is less general than the original goal, it may be a sign that either an inappropriate induction was chosen or that the original goal is insufficiently general. In any case, our proof attempt has failed. Summary Form: ( DEFTHM ROTATE-LEN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ROTATE) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION LEN)) Time: 0.09 seconds (prove: 0.06, print: 0.04, other: 0.00) Prover steps counted: 9865 --- 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 (IMPLIES (TRUE-LISTP X) (EQUAL (ROTATE (LEN X) X) X)) *** Key checkpoint under a top-level induction: *** Subgoal *1/2' (IMPLIES (AND (CONSP X) (EQUAL (ROTATE (LEN (CDR X)) (CDR X)) (CDR X)) (TRUE-LISTP (CDR X))) (EQUAL (ROTATE (+ 1 (LEN (CDR X))) X) X)) ACL2 Error in ( DEFTHM ROTATE-LEN ...): See :DOC failure. ******** FAILED ******** ACL2 >(include-book "arithmetic-5/top" :dir :system) ACL2 Observation in NON-LINEAR-ARITHMETIC: To turn on non- linear arithmetic, execute : (SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))) or : (SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT++ ID STABLE-UNDER-SIMPLIFICATIONP HIST NIL))) See the README for more about non-linear arithmetic and general information about using this library. Summary Form: ( INCLUDE-BOOK "arithmetic-5/top" ...) Rules: NIL Time: 0.28 seconds (prove: 0.00, print: 0.00, other: 0.27) "/Users/kaufmann/acl2/v4-3/acl2-sources/books/arithmetic-5/top.lisp" ACL2 >(defthm rotate-len (implies (true-listp x) (equal (rotate (len x) x) x))) Name the formula above *1. 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 (LEN X). This suggestion was produced using the :induction rules LEN 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 LEN. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X)) (EQUAL (ROTATE (LEN X) X) X)). But simplification reduces this to T, using the :definition TRUE-LISTP, the :executable-counterparts of CONSP, EQUAL, LEN and ROTATE and primitive type reasoning. Subgoal *1/2 (IMPLIES (AND (CONSP X) (EQUAL (ROTATE (LEN (CDR X)) (CDR X)) (CDR X)) (TRUE-LISTP X)) (EQUAL (ROTATE (LEN X) X) X)). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterpart of BINARY-+, primitive type reasoning, the :rewrite rules |(+ 0 x)|, |(+ c (+ d x))| and |(+ y (+ x z))| and the :type-prescription rule LEN, to Subgoal *1/2' (IMPLIES (AND (CONSP X) (EQUAL (ROTATE (LEN (CDR X)) (CDR X)) (CDR X)) (TRUE-LISTP (CDR X))) (EQUAL (ROTATE (LEN (CDR X)) (APP (CDR X) (LIST (CAR X)))) X)). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2'' (IMPLIES (AND (CONSP (CONS X1 X2)) (EQUAL (ROTATE (LEN X2) X2) X2) (TRUE-LISTP X2)) (EQUAL (ROTATE (LEN X2) (APP X2 (LIST X1))) (CONS X1 X2))). This simplifies, using primitive type reasoning, to Subgoal *1/2''' (IMPLIES (AND (EQUAL (ROTATE (LEN X2) X2) X2) (TRUE-LISTP X2)) (EQUAL (ROTATE (LEN X2) (APP X2 (LIST X1))) (CONS X1 X2))). We now use the first hypothesis by cross-fertilizing (ROTATE (LEN X2) X2) for X2 and throwing away the hypothesis. This produces Subgoal *1/2'4' (IMPLIES (TRUE-LISTP X2) (EQUAL (ROTATE (LEN X2) (APP X2 (LIST X1))) (CONS X1 (ROTATE (LEN X2) X2)))). We generalize this conjecture, replacing (LEN X2) by I and restricting the type of the new variable I to be that of the term it replaces, as established by LEN. This produces Subgoal *1/2'5' (IMPLIES (AND (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). By case analysis we reduce the conjecture to Subgoal *1/2'6' (IMPLIES (AND (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). Name the formula above *1.1. Subgoal *1/1 (IMPLIES (AND (CONSP X) (NOT (TRUE-LISTP (CDR X))) (TRUE-LISTP X)) (EQUAL (ROTATE (LEN X) X) X)). But we reduce the conjecture to T, by primitive type reasoning. So we now return to *1.1, which is (IMPLIES (AND (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). Perhaps we can prove *1.1 by induction. Four induction schemes are suggested by this conjecture. Subsumption reduces that number to three. 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 (ROTATE I X2). This suggestion was produced using the :induction rule ROTATE. If we let (:P I X1 X2) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP I)) (:P (+ -1 I) X1 (APP (CDR X2) (LIST (CAR X2))))) (:P I X1 X2)) (IMPLIES (ZP I) (:P I X1 X2))). This induction is justified by the same argument used to admit ROTATE. Note, however, that the unmeasured variable X2 is being instantiated. When applied to the goal at hand the above induction scheme produces five nontautological subgoals. Subgoal *1.1/5 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (APP (CDR X2) (LIST (CAR X2))) (LIST X1))) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2)))))) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions APP, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of APP, CAR, CDR, CONS and CONSP, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS and REMOVE-WEAK-INEQUALITIES, to the following two conjectures. Subgoal *1.1/5.2 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (APP (CDR X2) (LIST (CAR X2))) (LIST X1))) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2)))))) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE I (CONS (CAR X2) (APP (CDR X2) (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2))))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.1/5.2' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (APP X4 (LIST X3)) (LIST X1))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3))))) (TRUE-LISTP X4)) (EQUAL (ROTATE I (CONS X3 (APP X4 (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). This simplifies, using primitive type reasoning, to Subgoal *1.1/5.2'' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (APP X4 (LIST X3)) (LIST X1))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3))))) (TRUE-LISTP X4)) (EQUAL (ROTATE I (CONS X3 (APP X4 (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). We now use the second hypothesis by substituting (ROTATE (+ -1 I) (APP (APP X4 (LIST X3)) (LIST X1))) for (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))) and throwing away the hypothesis. This produces Subgoal *1.1/5.2''' (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP X4)) (EQUAL (ROTATE I (CONS X3 (APP X4 (LIST X1)))) (ROTATE (+ -1 I) (APP (APP X4 (LIST X3)) (LIST X1))))). Name the formula above *1.1.1. Subgoal *1.1/5.1 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP '(NIL) (LIST X1))) (CONS X1 (ROTATE (+ -1 I) '(NIL)))) (NOT X2)) (EQUAL (ROTATE (+ -1 I) (LIST X1)) (CONS X1 (ROTATE I NIL)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions APP and ROTATE and the :executable-counterparts of APP, CAR, CDR, CONS and CONSP, to Subgoal *1.1/5.1' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (LIST NIL X1)) (CONS X1 (ROTATE (+ -1 I) '(NIL))))) (EQUAL (ROTATE (+ -1 I) (LIST X1)) (CONS X1 (ROTATE (+ -1 I) '(NIL))))). We now use the second hypothesis by substituting (ROTATE (+ -1 I) (LIST NIL X1)) for (CONS X1 (ROTATE (+ -1 I) '(NIL))) and throwing away the hypothesis. This produces Subgoal *1.1/5.1'' (IMPLIES (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (LIST X1)) (ROTATE (+ -1 I) (LIST NIL X1)))). We generalize this conjecture, replacing (+ -1 I) by J and restricting the type of the new variable J to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.1/5.1''' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I))) (EQUAL (ROTATE J (LIST X1)) (ROTATE J (LIST NIL X1)))). By case analysis we reduce the conjecture to Subgoal *1.1/5.1'4' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I))) (EQUAL (ROTATE J (LIST X1)) (ROTATE J (LIST NIL X1)))). We suspect that the term (NOT (ZP I)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1.1/5.1'5' (IMPLIES (AND (INTEGERP J) (<= 0 J)) (EQUAL (ROTATE J (LIST X1)) (ROTATE J (LIST NIL X1)))). Name the formula above *1.1.2. Subgoal *1.1/4 (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (APP (CDR X2) (LIST (CAR X2))))) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions APP, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of APP, CAR, CDR, CONS, CONSP and TRUE-LISTP, primitive type reasoning and the :rewrite rule REMOVE-WEAK-INEQUALITIES, to Subgoal *1.1/4' (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (APP (CDR X2) (LIST (CAR X2))))) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE I (CONS (CAR X2) (APP (CDR X2) (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) (APP (CDR X2) (LIST (CAR X2))))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.1/4'' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (NOT (TRUE-LISTP (APP X4 (LIST X3)))) (TRUE-LISTP X4)) (EQUAL (ROTATE I (CONS X3 (APP X4 (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). This simplifies, using primitive type reasoning, to Subgoal *1.1/4''' (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (APP X4 (LIST X3)))) (TRUE-LISTP X4)) (EQUAL (ROTATE I (CONS X3 (APP X4 (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) (APP X4 (LIST X3)))))). We generalize this conjecture, replacing (APP X4 (LIST X3)) by L and restricting the type of the new variable L to be that of the term it replaces, as established by primitive type reasoning and APP. This produces Subgoal *1.1/4'4' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP I)) (NOT (TRUE-LISTP L)) (TRUE-LISTP X4)) (EQUAL (ROTATE I (CONS X3 (APP X4 (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) L)))). By case analysis we reduce the conjecture to Subgoal *1.1/4'5' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP I)) (TRUE-LISTP X4)) (EQUAL (ROTATE I (CONS X3 (APP X4 (LIST X1)))) (CONS X1 (ROTATE (+ -1 I) L)))). Name the formula above *1.1.3. Subgoal *1.1/3 (IMPLIES (AND (NOT (ZP I)) (< (+ -1 I) 0) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.1/2 (IMPLIES (AND (NOT (ZP I)) (NOT (INTEGERP (+ -1 I))) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.1/1 (IMPLIES (AND (ZP I) (INTEGERP I) (<= 0 I) (TRUE-LISTP X2)) (EQUAL (ROTATE I (APP X2 (LIST X1))) (CONS X1 (ROTATE I X2)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of <, INTEGERP, NOT and ZP and linear arithmetic, to Subgoal *1.1/1' (IMPLIES (TRUE-LISTP X2) (EQUAL (ROTATE 0 (APP X2 (LIST X1))) (CONS X1 (ROTATE 0 X2)))). This simplifies, using the :definition ROTATE and the :executable- counterpart of ZP, to Subgoal *1.1/1'' (IMPLIES (TRUE-LISTP X2) (EQUAL (APP X2 (LIST X1)) (CONS X1 X2))). Name the formula above *1.1.4. Perhaps we can prove *1.1.4 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 X2 (CONS X1 'NIL)). This suggestion was produced using the :induction rules APP and TRUE-LISTP. If we let (:P X1 X2) denote *1.1.4 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X2)) (:P X1 (CDR X2))) (:P X1 X2)) (IMPLIES (ENDP X2) (:P X1 X2))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.1.4/3 (IMPLIES (AND (NOT (ENDP X2)) (EQUAL (APP (CDR X2) (LIST X1)) (CONS X1 (CDR X2))) (TRUE-LISTP X2)) (EQUAL (APP X2 (LIST X1)) (CONS X1 X2))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1.4/3' (IMPLIES (AND (CONSP X2) (EQUAL (APP (CDR X2) (LIST X1)) (CONS X1 (CDR X2))) (TRUE-LISTP X2)) (EQUAL (APP X2 (LIST X1)) (CONS X1 X2))). This simplifies, using the :definitions APP and TRUE-LISTP, primitive type reasoning and the :rewrite rules CAR-CONS, CDR-CONS and CONS-EQUAL, to Subgoal *1.1.4/3'' (IMPLIES (AND (CONSP X2) (EQUAL (APP (CDR X2) (LIST X1)) (CONS X1 (CDR X2))) (TRUE-LISTP (CDR X2))) (EQUAL (CAR X2) X1)). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.1.4/3''' (IMPLIES (AND (CONSP (CONS X3 X4)) (EQUAL (APP X4 (LIST X1)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL X3 X1)). This simplifies, using primitive type reasoning, to Subgoal *1.1.4/3'4' (IMPLIES (AND (EQUAL (APP X4 (LIST X1)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL X3 X1)). Name the formula above *1.1.4.1. Subgoal *1.1.4/2 (IMPLIES (AND (NOT (ENDP X2)) (NOT (TRUE-LISTP (CDR X2))) (TRUE-LISTP X2)) (EQUAL (APP X2 (LIST X1)) (CONS X1 X2))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.1.4/1 (IMPLIES (AND (ENDP X2) (TRUE-LISTP X2)) (EQUAL (APP X2 (LIST X1)) (CONS X1 X2))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.1.4/1' (IMPLIES (AND (NOT (CONSP X2)) (TRUE-LISTP X2)) (EQUAL (APP X2 (LIST X1)) (CONS X1 X2))). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, the :executable-counterpart of CONSP and primitive type reasoning. So we now return to *1.1.4.1, which is (IMPLIES (AND (EQUAL (APP X4 (LIST X1)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL X3 X1)). Perhaps we can prove *1.1.4.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 (TRUE-LISTP X4). This suggestion was produced using the :induction rules APP and TRUE-LISTP. If we let (:P X1 X3 X4) denote *1.1.4.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP X4)) (:P X1 X3 X4)) (IMPLIES (AND (CONSP X4) (:P X1 X3 (CDR X4))) (:P X1 X3 X4))). This induction is justified by the same argument used to admit TRUE-LISTP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.1.4.1/3 (IMPLIES (AND (NOT (CONSP X4)) (EQUAL (APP X4 (LIST X1)) (CONS X1 X4)) (TRUE-LISTP X4)) (EQUAL X3 X1)). This simplifies, using the :definitions APP and TRUE-LISTP, the :executable-counterpart of CONSP and primitive type reasoning, to Subgoal *1.1.4.1/3' (IMPLIES (NOT X4) (EQUAL X3 X1)). This simplifies, using trivial observations, to Subgoal *1.1.4.1/3'' (EQUAL X3 X1). We suspect that this conjecture is not a theorem. We might as well be trying to prove Subgoal *1.1.4.1/3''' NIL. Summary Form: ( DEFTHM ROTATE-LEN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION ENDP) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART ROTATE) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-EQUAL) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION LEN)) Time: 0.12 seconds (prove: 0.09, print: 0.03, other: 0.00) Prover steps counted: 7003 --- 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 (IMPLIES (TRUE-LISTP X) (EQUAL (ROTATE (LEN X) X) X)) *** Key checkpoint under a top-level induction: *** Subgoal *1/2' (IMPLIES (AND (CONSP X) (EQUAL (ROTATE (LEN (CDR X)) (CDR X)) (CDR X)) (TRUE-LISTP (CDR X))) (EQUAL (ROTATE (LEN (CDR X)) (APP (CDR X) (LIST (CAR X)))) X)) ACL2 Error in ( DEFTHM ROTATE-LEN ...): See :DOC failure. ******** FAILED ******** ACL2 >(rotate 3 '(a b c d e f g)) (D E F G A B C) ACL2 >:pe firstn ACL2 Error in :PE: The object FIRSTN is not a logical name. See :DOC logical-name. ACL2 >:pe take V -719 (DEFUN TAKE (N L) "Documentation available via :doc" (DECLARE (XARGS :GUARD (AND (INTEGERP N) (NOT (< N 0)) (TRUE-LISTP L)))) (FIRST-N-AC N L NIL)) Additional events for the logical name TAKE: PV -6647 (DEFUN TAKE (N L) "Documentation available via :doc" (DECLARE (XARGS :GUARD (AND (INTEGERP N) (NOT (< N 0)) (TRUE-LISTP L)))) (FIRST-N-AC N L NIL)) ACL2 >:pe first-n ACL2 Error in :PE: The object FIRST-N is not a logical name. See :DOC logical-name. ACL2 >:pe firstn-ac ACL2 Error in :PE: The object FIRSTN-AC is not a logical name. See :DOC logical-name. ACL2 >(defun firstn (n x) (if (zp n) nil (cons (car x) (firstn (1- n) (cdr x))))) The admission of FIRSTN 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 N). We observe that the type of FIRSTN is described by the theorem (TRUE-LISTP (FIRSTN N X)). We used primitive type reasoning. Summary Form: ( DEFUN FIRSTN ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) FIRSTN ACL2 >(defun dropn (n x) (if (zp n) x (dropn (1- n) (cdr x)))) The admission of DROPN 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 N). We could deduce no constraints on the type of DROPN. Summary Form: ( DEFUN DROPN ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) DROPN ACL2 >(defthm rotate-len-generalization (implies (and (true-listp x) (<= n (len x))) (equal (rotate n x) (app (dropn n x) (firstn n x))))) This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, ROTATE and SYNP and the :rewrite rule DEFAULT-LESS-THAN-2, to the following two conjectures. Subgoal 2 (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). Name the formula above *1. Subgoal 1 (IMPLIES (AND (TRUE-LISTP X) (NOT (ACL2-NUMBERP N)) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). Normally we would attempt to prove Subgoal 1 by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) Perhaps we can prove *1 by induction. Five 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 (ROTATE N X). This suggestion was produced using the :induction rules DROPN, FIRSTN and ROTATE. If we let (:P N X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP N)) (:P (+ -1 N) (APP (CDR X) (LIST (CAR X))))) (:P N X)) (IMPLIES (ZP N) (:P N X))). This induction is justified by the same argument used to admit ROTATE. Note, however, that the unmeasured variable X is being instantiated. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1/2 (IMPLIES (AND (NOT (ZP N)) (IMPLIES (AND (TRUE-LISTP (APP (CDR X) (LIST (CAR X)))) (<= (+ -1 N) (LEN (APP (CDR X) (LIST (CAR X)))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))))) (IMPLIES (AND (TRUE-LISTP X) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X))))). By case analysis we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (IMPLIES (AND (TRUE-LISTP (APP (CDR X) (LIST (CAR X)))) (<= (+ -1 N) (LEN (APP (CDR X) (LIST (CAR X)))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X))))))) (TRUE-LISTP X) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, NOT, ROTATE and TRUE-LISTP, the :executable-counterparts of APP, CAR, CDR, CONS, CONSP, LEN and TRUE-LISTP and primitive type reasoning, to the following three conjectures. Subgoal *1/2.3 (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2.3' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (ZP N)) (NOT (TRUE-LISTP (APP X2 (LIST X1)))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/2.3'' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP X2 (LIST X1)))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We generalize this conjecture, replacing (APP X2 (LIST X1)) by L and (+ -1 N) by I and restricting the types of the new variables L and I to be those of the terms they replace, as established by primitive type reasoning and APP and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1/2.3''' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (NOT (TRUE-LISTP L)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). By case analysis we reduce the conjecture to Subgoal *1/2.3'4' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Name the formula above *1.1. Subgoal *1/2.2 (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2.2' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1))))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/2.2'' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1))))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We now use the second hypothesis by substituting (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1)))) for (ROTATE (+ -1 N) (APP X2 (LIST X1))) and throwing away the hypothesis. This produces Subgoal *1/2.2''' (IMPLIES (AND (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1)))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We generalize this conjecture, replacing (+ -1 N) by I and restricting the type of the new variable I to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1/2.2'4' (IMPLIES (AND (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (APP (DROPN I (APP X2 (LIST X1))) (FIRSTN I (APP X2 (LIST X1)))) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). By case analysis we reduce the conjecture to Subgoal *1/2.2'5' (IMPLIES (AND (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (APP (DROPN I (APP X2 (LIST X1))) (FIRSTN I (APP X2 (LIST X1)))) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Name the formula above *1.2. Subgoal *1/2.1 (IMPLIES (AND (NOT (ZP N)) (< (LEN (APP (CDR X) (LIST (CAR X)))) (+ -1 N)) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition SYNP, the :executable- counterpart of UNARY--, the :rewrite rule |(< y (+ (- c) x))| and the :type-prescription rule LEN, to Subgoal *1/2.1' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2.1'' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (ZP N)) (< (+ 1 (LEN (APP X2 (LIST X1)))) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/2.1''' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP X2 (LIST X1)))) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We generalize this conjecture, replacing (APP X2 (LIST X1)) by L and (+ -1 N) by I and restricting the types of the new variables L and I to be those of the terms they replace, as established by primitive type reasoning and APP and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1/2.1'4' (IMPLIES (AND (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). By case analysis we reduce the conjecture to Subgoal *1/2.1'5' (IMPLIES (AND (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Name the formula above *1.3. Subgoal *1/1 (IMPLIES (ZP N) (IMPLIES (AND (TRUE-LISTP X) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X))))). By case analysis we reduce the conjecture to Subgoal *1/1' (IMPLIES (AND (ZP N) (TRUE-LISTP X) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, ROTATE and SYNP and the :rewrite rule DEFAULT-LESS-THAN-2, to the following two conjectures. Subgoal *1/1.2 (IMPLIES (AND (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). Name the formula above *1.4. Subgoal *1/1.1 (IMPLIES (AND (ZP N) (TRUE-LISTP X) (NOT (ACL2-NUMBERP N)) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, to Subgoal *1/1.1' (IMPLIES (AND (TRUE-LISTP X) (NOT (ACL2-NUMBERP N)) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). We suspect that the term (NOT (ACL2-NUMBERP N)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1/1.1'' (IMPLIES (AND (TRUE-LISTP X) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). Name the formula above *1.5. Perhaps we can prove *1.5 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 (APP X 'NIL). This suggestion was produced using the :induction rules APP, LEN and TRUE-LISTP. If we let (:P X) denote *1.5 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 APP. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1.5/4 (IMPLIES (AND (NOT (ENDP X)) (EQUAL (CDR X) (APP (CDR X) NIL)) (TRUE-LISTP X) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.5/4' (IMPLIES (AND (CONSP X) (EQUAL (CDR X) (APP (CDR X) NIL)) (TRUE-LISTP X) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). But simplification reduces this to T, using the :definitions APP, LEN and TRUE-LISTP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. Subgoal *1.5/3 (IMPLIES (AND (NOT (ENDP X)) (< (LEN (CDR X)) 0) (TRUE-LISTP X) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). But we reduce the conjecture to T, by primitive type reasoning and the :type-prescription rule LEN. Subgoal *1.5/2 (IMPLIES (AND (NOT (ENDP X)) (NOT (TRUE-LISTP (CDR X))) (TRUE-LISTP X) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.5/1 (IMPLIES (AND (ENDP X) (TRUE-LISTP X) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.5/1' (IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X) (<= 0 (LEN X))) (EQUAL X (APP X NIL))). But simplification reduces this to T, using the :definition TRUE-LISTP, the :executable-counterparts of <, APP, CONSP, EQUAL and LEN and primitive type reasoning. That completes the proof of *1.5. We therefore turn our attention to *1.4, which is (IMPLIES (AND (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). Perhaps we can prove *1.4 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 (APP X 'NIL). This suggestion was produced using the :induction rules APP, LEN and TRUE-LISTP. If we let (:P N X) denote *1.4 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X)) (:P N (CDR X))) (:P N X)) (IMPLIES (ENDP X) (:P N X))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1.4/4 (IMPLIES (AND (NOT (ENDP X)) (EQUAL (CDR X) (APP (CDR X) NIL)) (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.4/4' (IMPLIES (AND (CONSP X) (EQUAL (CDR X) (APP (CDR X) NIL)) (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). But simplification reduces this to T, using the :definitions APP, LEN and TRUE-LISTP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. Subgoal *1.4/3 (IMPLIES (AND (NOT (ENDP X)) (< (LEN (CDR X)) N) (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.4/3' (IMPLIES (AND (CONSP X) (< (LEN (CDR X)) N) (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions APP, LEN and TRUE-LISTP and the :type-prescription rule LEN, to Subgoal *1.4/3'' (IMPLIES (AND (CONSP X) (< (LEN (CDR X)) N) (ZP N) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL X (CONS (CAR X) (APP (CDR X) NIL)))). This simplifies, using the :definition SYNP, primitive type reasoning, the :rewrite rule DEFAULT-LESS-THAN-2 and the :type-prescription rule LEN, to Subgoal *1.4/3''' (IMPLIES (AND (CONSP X) (ACL2-NUMBERP N) (< (LEN (CDR X)) N) (ZP N) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL X (CONS (CAR X) (APP (CDR X) NIL)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition SYNP, primitive type reasoning, the :rewrite rule DEFAULT-LESS-THAN-2 and the :type-prescription rule LEN, to a set of conjectures including Subgoal *1.4/3''' itself! Therefore, we ignore this specious simplification. See :DOC specious-simplification. This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition SYNP, primitive type reasoning, the :rewrite rule DEFAULT-LESS-THAN-2 and the :type-prescription rule LEN, to a set of conjectures including Subgoal *1.4/3''' itself! Therefore, we ignore this specious simplification. See :DOC specious-simplification. The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1.4/3'4' (IMPLIES (AND (CONSP (CONS X1 X2)) (ACL2-NUMBERP N) (< (LEN X2) N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (CONS X1 X2) (CONS X1 (APP X2 NIL)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition SYNP, primitive type reasoning, the :rewrite rules CONS-EQUAL and DEFAULT-LESS-THAN-2 and the :type-prescription rule LEN, to Subgoal *1.4/3'5' (IMPLIES (AND (ACL2-NUMBERP N) (< (LEN X2) N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL X2 (APP X2 NIL))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition SYNP, primitive type reasoning, the :rewrite rule DEFAULT-LESS-THAN-2 and the :type-prescription rule LEN, to a set of conjectures including Subgoal *1.4/3'5' itself! Therefore, we ignore this specious simplification. See :DOC specious-simplification. We generalize this conjecture, replacing (LEN X2) by I and restricting the type of the new variable I to be that of the term it replaces, as established by LEN. This produces Subgoal *1.4/3'6' (IMPLIES (AND (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). By case analysis we reduce the conjecture to Subgoal *1.4/3'7' (IMPLIES (AND (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition SYNP and the :rewrite rules DEFAULT-LESS-THAN-2 and REMOVE-WEAK-INEQUALITIES, to a set of conjectures including Subgoal *1.4/3'7' itself! Therefore, we ignore this specious simplification. See :DOC specious-simplification. Name the formula above *1.4.1. Subgoal *1.4/2 (IMPLIES (AND (NOT (ENDP X)) (NOT (TRUE-LISTP (CDR X))) (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.4/1 (IMPLIES (AND (ENDP X) (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.4/1' (IMPLIES (AND (NOT (CONSP X)) (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL X (APP X NIL))). But simplification reduces this to T, using the :definition TRUE-LISTP, the :executable-counterparts of APP, CONSP, EQUAL and LEN and primitive type reasoning. So we now return to *1.4.1, which is (IMPLIES (AND (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). Perhaps we can prove *1.4.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 X2 'NIL). This suggestion was produced using the :induction rules APP and TRUE-LISTP. If we let (:P I N X2) denote *1.4.1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X2)) (:P I N (CDR X2))) (:P I N X2)) (IMPLIES (ENDP X2) (:P I N X2))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.4.1/3 (IMPLIES (AND (NOT (ENDP X2)) (EQUAL (CDR X2) (APP (CDR X2) NIL)) (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.4.1/3' (IMPLIES (AND (CONSP X2) (EQUAL (CDR X2) (APP (CDR X2) NIL)) (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). But simplification reduces this to T, using the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions APP, SYNP and TRUE-LISTP, primitive type reasoning and the :rewrite rules CONS-CAR-CDR, DEFAULT-LESS-THAN-2 and REMOVE-WEAK-INEQUALITIES. Subgoal *1.4.1/2 (IMPLIES (AND (NOT (ENDP X2)) (NOT (TRUE-LISTP (CDR X2))) (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.4.1/1 (IMPLIES (AND (ENDP X2) (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.4.1/1' (IMPLIES (AND (NOT (CONSP X2)) (INTEGERP I) (<= 0 I) (ACL2-NUMBERP N) (< I N) (ZP N) (TRUE-LISTP X2) (<= N (+ 1 I))) (EQUAL X2 (APP X2 NIL))). But simplification reduces this to T, using the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions SYNP and TRUE-LISTP, the :executable-counterparts of APP, CONSP and EQUAL, primitive type reasoning and the :rewrite rules DEFAULT-LESS-THAN-2 and REMOVE-WEAK-INEQUALITIES. That completes the proofs of *1.4.1 and *1.4. We therefore turn our attention to *1.3, which is (IMPLIES (AND (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Perhaps we can prove *1.3 by induction. Six induction schemes are suggested by this conjecture. Subsumption reduces that number to four. 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 (ROTATE I L), but modified to accommodate (FIRSTN I X2). These suggestions were produced using the :induction rules DROPN, FIRSTN, LEN, ROTATE and TRUE-LISTP. If we let (:P I L N X1 X2) denote *1.3 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP I)) (:P (+ -1 I) (APP (CDR L) (LIST (CAR L))) N X1 (CDR X2))) (:P I L N X1 X2)) (IMPLIES (ZP I) (:P I L N X1 X2))). This induction is justified by the same argument used to admit ROTATE. Note, however, that the unmeasured variables X2 and L are being instantiated. When applied to the goal at hand the above induction scheme produces eight nontautological subgoals. Subgoal *1.3/8 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (CONS X1 (FIRSTN (+ -1 I) (CDR X2))))) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CAR, CDR, CONSP and LEN, primitive type reasoning and the :rewrite rules |(+ c (+ d x))| and REMOVE-WEAK-INEQUALITIES, to the following two conjectures. Subgoal *1.3/8.2 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (CONS X1 (FIRSTN (+ -1 I) (CDR X2))))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/8.2' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/8.2'' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/8.2''' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/8.2'4' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We now use the second hypothesis by substituting (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4))) for (ROTATE (+ -1 I) (APP L2 (LIST L1))) and throwing away the hypothesis. This produces Subgoal *1.3/8.2'5' (IMPLIES (AND (NOT (ZP I)) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We generalize this conjecture, replacing (+ -1 I) by J and restricting the type of the new variable J to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/8.2'6' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP (DROPN J X4) (CONS X1 (FIRSTN J X4))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). By case analysis we reduce the conjecture to Subgoal *1.3/8.2'7' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP (DROPN J X4) (CONS X1 (FIRSTN J X4))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). We generalize this conjecture, replacing (FIRSTN J X4) by FN and (DROPN J X4) by DN and restricting the type of the new variable FN to be that of the term it replaces, as established by FIRSTN. This produces Subgoal *1.3/8.2'8' (IMPLIES (AND (TRUE-LISTP FN) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP DN (CONS X1 FN)) (APP DN (LIST* X1 X3 FN)))). We suspect that the term (NOT (ZP I)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1.3/8.2'9' (IMPLIES (AND (TRUE-LISTP FN) (INTEGERP J) (<= 0 J) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP DN (CONS X1 FN)) (APP DN (LIST* X1 X3 FN)))). Name the formula above *1.3.1. Subgoal *1.3/8.1 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) NIL) (CONS X1 (FIRSTN (+ -1 I) NIL)))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (NOT X2) (<= N 1)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). But simplification reduces this to T, using the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1.3/7 (IMPLIES (AND (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CDR, CONSP and LEN, primitive type reasoning and the :rewrite rules |(+ c (+ d x))| and REMOVE-WEAK-INEQUALITIES, to Subgoal *1.3/7' (IMPLIES (AND (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3/7'' (IMPLIES (AND (EQUAL (LEN (CDR X2)) (+ -2 N)) (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions LEN and SYNP, the :executable-counterparts of <, BINARY-+ and UNARY--, primitive type reasoning, the :rewrite rules |(* a (/ a))|, |(* y x)|, |(+ c (+ d x))|, |(< x (/ y)) with (< 0 y)|, |(equal (+ (- c) x) y)| and SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-< and the :type-prescription rule LEN, to Subgoal *1.3/7''' (IMPLIES (AND (EQUAL N (+ 2 (LEN (CDR X2)))) (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (< (+ 2 (LEN (CDR L))) N) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). This simplifies, using the :definition SYNP, the :executable- counterparts of < and BINARY-+, primitive type reasoning, the :rewrite rules |(+ 0 x)|, |(+ c (+ d x))|, |(+ x (- x))|, |(+ y (+ x z))|, |(+ y x)|, BUBBLE-DOWN-+-MATCH-1, NORMALIZE-ADDENDS, REDUCE-ADDITIVE-CONSTANT-< and SIMPLIFY-SUMS-< and the :type-prescription rule LEN, to Subgoal *1.3/7'4' (IMPLIES (AND (NOT (ZP I)) (CONSP L) (< (LEN (CDR L)) (LEN (CDR X2))) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/7'5' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (CONSP L) (< (LEN (CDR L)) (LEN X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/7'6' (IMPLIES (AND (NOT (ZP I)) (CONSP L) (< (LEN (CDR L)) (LEN X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/7'7' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (< (LEN L2) (LEN X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/7'8' (IMPLIES (AND (NOT (ZP I)) (< (LEN L2) (LEN X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We generalize this conjecture, replacing (+ -1 I) by J and restricting the type of the new variable J to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/7'9' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (< (LEN L2) (LEN X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE J (APP L2 (LIST L1))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). By case analysis we reduce the conjecture to Subgoal *1.3/7'10' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (< (LEN L2) (LEN X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE J (APP L2 (LIST L1))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). We suspect that the term (NOT (ZP I)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1.3/7'11' (IMPLIES (AND (INTEGERP J) (<= 0 J) (< (LEN L2) (LEN X4)) (TRUE-LISTP X4)) (EQUAL (ROTATE J (APP L2 (LIST L1))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). Name the formula above *1.3.2. Subgoal *1.3/6 (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (CDR X2))) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.3/5 (IMPLIES (AND (NOT (ZP I)) (<= N (+ 1 (LEN (APP (CDR L) (LIST (CAR L)))))) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CONSP and LEN, primitive type reasoning and the :rewrite rules |(+ c (+ d x))| and REMOVE-WEAK-INEQUALITIES, to the following two conjectures. Subgoal *1.3/5.2 (IMPLIES (AND (NOT (ZP I)) (<= N (+ 1 (LEN (APP (CDR L) (LIST (CAR L)))))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/5.2' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (<= N (+ 1 (LEN (APP (CDR L) (LIST (CAR L)))))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/5.2'' (IMPLIES (AND (NOT (ZP I)) (<= N (+ 1 (LEN (APP (CDR L) (LIST (CAR L)))))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/5.2''' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (<= N (+ 1 (LEN (APP L2 (LIST L1))))) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/5.2'4' (IMPLIES (AND (NOT (ZP I)) (<= N (+ 1 (LEN (APP L2 (LIST L1))))) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We generalize this conjecture, replacing (APP L2 (LIST L1)) by L and (+ -1 I) by J and restricting the types of the new variables L and J to be those of the terms they replace, as established by primitive type reasoning and APP and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/5.2'5' (IMPLIES (AND (CONSP L) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (<= N (+ 1 (LEN L))) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE J L) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). By case analysis we reduce the conjecture to Subgoal *1.3/5.2'6' (IMPLIES (AND (CONSP L) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (<= N (+ 1 (LEN L))) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE J L) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). We suspect that the term (NOT (ZP I)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1.3/5.2'7' (IMPLIES (AND (CONSP L) (INTEGERP J) (<= 0 J) (<= N (+ 1 (LEN L))) (NOT (ZP N)) (< (+ 2 (LEN L2)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE J L) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). Name the formula above *1.3.3. Subgoal *1.3/5.1 (IMPLIES (AND (NOT (ZP I)) (<= N (+ 1 (LEN (APP (CDR L) (LIST (CAR L)))))) (CONSP L) (NOT (ZP N)) (< (+ 2 (LEN (CDR L))) N) (NOT X2) (<= N 1)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN I NIL) (CONS X1 (FIRSTN I NIL))))). But simplification reduces this to T, using the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1.3/4 (IMPLIES (AND (NOT (ZP I)) (< (+ -1 I) 0) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.3/3 (IMPLIES (AND (NOT (ZP I)) (NOT (INTEGERP (+ -1 I))) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.3/2 (IMPLIES (AND (NOT (ZP I)) (NOT (CONSP (APP (CDR L) (LIST (CAR L))))) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by primitive type reasoning and the :type-prescription rule APP. Subgoal *1.3/1 (IMPLIES (AND (ZP I) (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of <, INTEGERP, NOT and ZP and linear arithmetic, to Subgoal *1.3/1' (IMPLIES (AND (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE 0 L) (APP (DROPN 0 X2) (CONS X1 (FIRSTN 0 X2))))). This simplifies, using the :definitions APP, DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CONSP, DROPN, FIRSTN, LEN and ZP, primitive type reasoning and the :rewrite rule |(+ c (+ d x))|, to the following two conjectures. Subgoal *1.3/1.2 (IMPLIES (AND (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL L (APP X2 (LIST X1)))). This simplifies, using the :definition APP, to Subgoal *1.3/1.2' (IMPLIES (AND (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL L (CONS (CAR X2) (APP (CDR X2) (LIST X1))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/1.2'' (IMPLIES (AND (CONSP (CONS X3 X4)) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/1.2''' (IMPLIES (AND (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). Name the formula above *1.3.4. Subgoal *1.3/1.1 (IMPLIES (AND (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (NOT X2) (<= N 1)) (EQUAL L (LIST X1))). But simplification reduces this to T, using the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. So we now return to *1.3.4, which is (IMPLIES (AND (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). Perhaps we can prove *1.3.4 by induction. Four induction schemes are suggested by this conjecture. Subsumption reduces that number to three. These merge into two derived induction schemes. One of these has a score higher than the other. We will induct according to a scheme suggested by (APP X4 (CONS X1 'NIL)). This suggestion was produced using the :induction rules APP, LEN and TRUE-LISTP. If we let (:P L N X1 X3 X4) denote *1.3.4 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X4)) (:P L N X1 X3 (CDR X4))) (:P L N X1 X3 X4)) (IMPLIES (ENDP X4) (:P L N X1 X3 X4))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1.3.4/4 (IMPLIES (AND (NOT (ENDP X4)) (EQUAL L (CONS X3 (APP (CDR X4) (LIST X1)))) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.3.4/4' (IMPLIES (AND (CONSP X4) (EQUAL L (CONS X3 (APP (CDR X4) (LIST X1)))) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). This simplifies, using the :definitions APP, LEN, SYNP and TRUE-LISTP, the :executable-counterpart of BINARY-+, primitive type reasoning and the :rewrite rules |(+ c (+ d x))|, |(+ y (+ x z))|, CAR-CONS and CDR-CONS, to Subgoal *1.3.4/4'' (IMPLIES (AND (CONSP X4) (NOT (ZP N)) (< (+ 2 (LEN (APP (CDR X4) (LIST X1)))) N) (TRUE-LISTP (CDR X4))) (< (+ 3 (LEN (CDR X4))) N)). The destructor terms (CAR X4) and (CDR X4) can be eliminated by using CAR-CDR-ELIM to replace X4 by (CONS X5 X6), (CAR X4) by X5 and (CDR X4) by X6. This produces the following goal. Subgoal *1.3.4/4''' (IMPLIES (AND (CONSP (CONS X5 X6)) (NOT (ZP N)) (< (+ 2 (LEN (APP X6 (LIST X1)))) N) (TRUE-LISTP X6)) (< (+ 3 (LEN X6)) N)). This simplifies, using primitive type reasoning, to Subgoal *1.3.4/4'4' (IMPLIES (AND (NOT (ZP N)) (< (+ 2 (LEN (APP X6 (LIST X1)))) N) (TRUE-LISTP X6)) (< (+ 3 (LEN X6)) N)). Name the formula above *1.3.4.1. Subgoal *1.3.4/3 (IMPLIES (AND (NOT (ENDP X4)) (< (+ 2 (LEN (CDR X4))) N) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.3.4/3' (IMPLIES (AND (CONSP X4) (< (+ 2 (LEN (CDR X4))) N) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). This simplifies, using the :definitions APP, LEN, SYNP and TRUE-LISTP, the :executable-counterpart of BINARY-+ and the :rewrite rules |(+ c (+ d x))| and |(+ y (+ x z))|, to Subgoal *1.3.4/3'' (IMPLIES (AND (CONSP X4) (< (+ 2 (LEN (CDR X4))) N) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP (CDR X4)) (<= N (+ 3 (LEN (CDR X4))))) (EQUAL L (LIST* X3 (CAR X4) (APP (CDR X4) (LIST X1))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3.4/3''' (IMPLIES (AND (EQUAL (LEN (CDR X4)) (+ -3 N)) (CONSP X4) (< (+ 2 (LEN (CDR X4))) N) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP (CDR X4)) (<= N (+ 3 (LEN (CDR X4))))) (EQUAL L (LIST* X3 (CAR X4) (APP (CDR X4) (LIST X1))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definition SYNP, the :executable- counterparts of < and UNARY--, primitive type reasoning, the :rewrite rules |(* a (/ a))|, |(* y x)|, |(< x (/ y)) with (< 0 y)|, |(equal (+ (- c) x) y)| and SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-< and the :type-prescription rule LEN, to Subgoal *1.3.4/3'4' (IMPLIES (AND (EQUAL N (+ 3 (LEN (CDR X4)))) (CONSP X4) (< (+ 2 (LEN (CDR X4))) N) (CONSP L) (< (+ 1 (LEN L)) N) (TRUE-LISTP (CDR X4))) (EQUAL L (LIST* X3 (CAR X4) (APP (CDR X4) (LIST X1))))). This simplifies, using the :definition SYNP, the :executable- counterparts of < and BINARY-+, primitive type reasoning, the :rewrite rules |(+ 0 x)|, |(+ c (+ d x))|, |(+ x (- x))|, |(+ y (+ x z))|, |(+ y x)|, BUBBLE-DOWN-+-MATCH-1, NORMALIZE-ADDENDS, REDUCE-ADDITIVE-CONSTANT-< and SIMPLIFY-SUMS-< and the :type-prescription rule LEN, to Subgoal *1.3.4/3'5' (IMPLIES (AND (CONSP X4) (CONSP L) (< (LEN L) (+ 2 (LEN (CDR X4)))) (TRUE-LISTP (CDR X4))) (EQUAL L (LIST* X3 (CAR X4) (APP (CDR X4) (LIST X1))))). The destructor terms (CAR X4) and (CDR X4) can be eliminated by using CAR-CDR-ELIM to replace X4 by (CONS X5 X6), (CAR X4) by X5 and (CDR X4) by X6. This produces the following goal. Subgoal *1.3.4/3'6' (IMPLIES (AND (CONSP (CONS X5 X6)) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1.3.4/3'7' (IMPLIES (AND (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). Name the formula above *1.3.4.2. Subgoal *1.3.4/2 (IMPLIES (AND (NOT (ENDP X4)) (NOT (TRUE-LISTP (CDR X4))) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.3.4/1 (IMPLIES (AND (ENDP X4) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.3.4/1' (IMPLIES (AND (NOT (CONSP X4)) (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). This simplifies, using the :definitions APP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CONSP and LEN and primitive type reasoning, to Subgoal *1.3.4/1'' (IMPLIES (AND (CONSP L) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (NOT X4) (<= N 2)) (EQUAL L (LIST X3 X1))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of < and ZP, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3.4/1''' (IMPLIES (AND (CONSP L) (< (+ 1 (LEN L)) 2)) (EQUAL L (LIST X3 X1))). This simplifies, using the :executable-counterparts of <, BINARY-+ and NOT, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3.4/1'4' (IMPLIES (AND (EQUAL (LEN L) 0) (CONSP L)) (EQUAL L (LIST X3 X1))). Name the formula above *1.3.4.3. Perhaps we can prove *1.3.4.3 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (LEN L). This suggestion was produced using the :induction rule LEN. If we let (:P L X1 X3) denote *1.3.4.3 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP L)) (:P L X1 X3)) (IMPLIES (AND (CONSP L) (:P (CDR L) X1 X3)) (:P L X1 X3))). This induction is justified by the same argument used to admit LEN. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.3.4.3/3 (IMPLIES (AND (CONSP L) (EQUAL (CDR L) (LIST X3 X1)) (EQUAL (LEN L) 0)) (EQUAL L (LIST X3 X1))). But simplification reduces this to T, using the :definition LEN, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1.3.4.3/2 (IMPLIES (AND (CONSP L) (NOT (CONSP (CDR L))) (EQUAL (LEN L) 0)) (EQUAL L (LIST X3 X1))). But simplification reduces this to T, using the :definition LEN, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1.3.4.3/1 (IMPLIES (AND (CONSP L) (NOT (EQUAL (LEN (CDR L)) 0)) (EQUAL (LEN L) 0)) (EQUAL L (LIST X3 X1))). But simplification reduces this to T, using the :definition LEN, primitive type reasoning and the :type-prescription rule LEN. That completes the proof of *1.3.4.3. We therefore turn our attention to *1.3.4.2, which is (IMPLIES (AND (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). Perhaps we can prove *1.3.4.2 by induction. Four induction schemes are suggested by this conjecture. Subsumption reduces that number to three. These merge into two derived induction schemes. One of these has a score higher than the other. We will induct according to a scheme suggested by (APP X6 (CONS X1 'NIL)). This suggestion was produced using the :induction rules APP, LEN and TRUE-LISTP. If we let (:P L X1 X3 X5 X6) denote *1.3.4.2 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP X6)) (:P L X1 X3 X5 (CDR X6))) (:P L X1 X3 X5 X6)) (IMPLIES (ENDP X6) (:P L X1 X3 X5 X6))). This induction is justified by the same argument used to admit APP. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1.3.4.2/4 (IMPLIES (AND (NOT (ENDP X6)) (EQUAL L (LIST* X3 X5 (APP (CDR X6) (LIST X1)))) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.3.4.2/4' (IMPLIES (AND (CONSP X6) (EQUAL L (LIST* X3 X5 (APP (CDR X6) (LIST X1)))) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). This simplifies, using the :definitions APP, LEN, SYNP and TRUE-LISTP, the :executable-counterpart of BINARY-+, primitive type reasoning and the :rewrite rules |(+ c (+ d x))|, |(+ y (+ x z))|, CAR-CONS and CDR-CONS, to Subgoal *1.3.4.2/4'' (IMPLIES (AND (CONSP X6) (< (+ 2 (LEN (APP (CDR X6) (LIST X1)))) (+ 3 (LEN (CDR X6))))) (NOT (TRUE-LISTP (CDR X6)))). This simplifies, using the :definition SYNP, the :executable- counterpart of BINARY-+, primitive type reasoning, the :rewrite rules |(+ 0 x)|, |(+ c (+ d x))|, |(+ y (+ x z))| and REDUCE-ADDITIVE-CONSTANT-< and the :type-prescription rule LEN, to Subgoal *1.3.4.2/4''' (IMPLIES (AND (CONSP X6) (< (LEN (APP (CDR X6) (LIST X1))) (+ 1 (LEN (CDR X6))))) (NOT (TRUE-LISTP (CDR X6)))). The destructor terms (CAR X6) and (CDR X6) can be eliminated by using CAR-CDR-ELIM to replace X6 by (CONS X7 X8), (CAR X6) by X7 and (CDR X6) by X8. This produces the following goal. Subgoal *1.3.4.2/4'4' (IMPLIES (AND (CONSP (CONS X7 X8)) (< (LEN (APP X8 (LIST X1))) (+ 1 (LEN X8)))) (NOT (TRUE-LISTP X8))). This simplifies, using primitive type reasoning, to Subgoal *1.3.4.2/4'5' (IMPLIES (< (LEN (APP X8 (LIST X1))) (+ 1 (LEN X8))) (NOT (TRUE-LISTP X8))). Name the formula above *1.3.4.2.1. Subgoal *1.3.4.2/3 (IMPLIES (AND (NOT (ENDP X6)) (NOT (TRUE-LISTP (CDR X6))) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.3.4.2/2 (IMPLIES (AND (NOT (ENDP X6)) (<= (+ 2 (LEN (CDR X6))) (LEN L)) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.3.4.2/2' (IMPLIES (AND (CONSP X6) (<= (+ 2 (LEN (CDR X6))) (LEN L)) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). This simplifies, using the :definitions APP, LEN, SYNP and TRUE-LISTP, the :executable-counterpart of BINARY-+ and the :rewrite rules |(+ c (+ d x))| and |(+ y (+ x z))|, to Subgoal *1.3.4.2/2'' (IMPLIES (AND (CONSP X6) (<= (+ 2 (LEN (CDR X6))) (LEN L)) (CONSP L) (< (LEN L) (+ 3 (LEN (CDR X6)))) (TRUE-LISTP (CDR X6))) (EQUAL L (LIST* X3 X5 (CAR X6) (APP (CDR X6) (LIST X1))))). This simplifies, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3.4.2/2''' (IMPLIES (AND (EQUAL (LEN (CDR X6)) (+ -2 (LEN L))) (CONSP X6) (<= (+ 2 (LEN (CDR X6))) (LEN L)) (CONSP L) (< (LEN L) (+ 3 (LEN (CDR X6)))) (TRUE-LISTP (CDR X6))) (EQUAL L (LIST* X3 X5 (CAR X6) (APP (CDR X6) (LIST X1))))). This simplifies, using the :definition SYNP, the :executable- counterparts of < and UNARY--, primitive type reasoning, the :rewrite rules |(* a (/ a))|, |(* y x)|, |(< x (/ y)) with (< 0 y)|, |(equal (+ (- c) x) y)| and SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-< and the :type-prescription rule LEN, to Subgoal *1.3.4.2/2'4' (IMPLIES (AND (EQUAL (LEN L) (+ 2 (LEN (CDR X6)))) (CONSP X6) (CONSP L) (< (LEN L) (+ 3 (LEN (CDR X6)))) (TRUE-LISTP (CDR X6))) (EQUAL L (LIST* X3 X5 (CAR X6) (APP (CDR X6) (LIST X1))))). This simplifies, using the :definition SYNP, linear arithmetic, primitive type reasoning, the :rewrite rule REMOVE-STRICT-INEQUALITIES and the :type-prescription rule LEN, to Subgoal *1.3.4.2/2'5' (IMPLIES (AND (EQUAL (LEN L) (+ 2 (LEN (CDR X6)))) (CONSP X6) (CONSP L) (TRUE-LISTP (CDR X6))) (EQUAL L (LIST* X3 X5 (CAR X6) (APP (CDR X6) (LIST X1))))). The destructor terms (CAR X6) and (CDR X6) can be eliminated by using CAR-CDR-ELIM to replace X6 by (CONS X7 X8), (CAR X6) by X7 and (CDR X6) by X8. This produces the following goal. Subgoal *1.3.4.2/2'6' (IMPLIES (AND (CONSP (CONS X7 X8)) (EQUAL (LEN L) (+ 2 (LEN X8))) (CONSP L) (TRUE-LISTP X8)) (EQUAL L (LIST* X3 X5 X7 (APP X8 (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1.3.4.2/2'7' (IMPLIES (AND (EQUAL (LEN L) (+ 2 (LEN X8))) (CONSP L) (TRUE-LISTP X8)) (EQUAL L (LIST* X3 X5 X7 (APP X8 (LIST X1))))). Name the formula above *1.3.4.2.2. Subgoal *1.3.4.2/1 (IMPLIES (AND (ENDP X6) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). By the simple :definition ENDP we reduce the conjecture to Subgoal *1.3.4.2/1' (IMPLIES (AND (NOT (CONSP X6)) (CONSP L) (< (LEN L) (+ 2 (LEN X6))) (TRUE-LISTP X6)) (EQUAL L (LIST* X3 X5 (APP X6 (LIST X1))))). This simplifies, using the :definitions APP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CONSP and LEN and primitive type reasoning, to Subgoal *1.3.4.2/1'' (IMPLIES (AND (CONSP L) (< (LEN L) 2) (NOT X6)) (EQUAL L (LIST X3 X5 X1))). This simplifies, using trivial observations, to Subgoal *1.3.4.2/1''' (IMPLIES (AND (CONSP L) (< (LEN L) 2)) (EQUAL L (LIST X3 X5 X1))). Name the formula above *1.3.4.2.3. Perhaps we can prove *1.3.4.2.3 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (LEN L). This suggestion was produced using the :induction rule LEN. If we let (:P L X1 X3 X5) denote *1.3.4.2.3 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP L)) (:P L X1 X3 X5)) (IMPLIES (AND (CONSP L) (:P (CDR L) X1 X3 X5)) (:P L X1 X3 X5))). This induction is justified by the same argument used to admit LEN. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1.3.4.2.3/3 (IMPLIES (AND (CONSP L) (EQUAL (CDR L) (LIST X3 X5 X1)) (< (LEN L) 2)) (EQUAL L (LIST X3 X5 X1))). This simplifies, using the :definition LEN and primitive type reasoning, to Subgoal *1.3.4.2.3/3' (IMPLIES (AND (CONSP L) (EQUAL (CDR L) (LIST X3 X5 X1)) (< (+ 1 (LEN (CDR L))) 2)) (EQUAL L (CDR L))). This simplifies, using the :executable-counterparts of <, BINARY-+ and NOT, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3.4.2.3/3'' (IMPLIES (AND (EQUAL (LEN (CDR L)) 0) (CONSP L) (EQUAL (CDR L) (LIST X3 X5 X1))) (EQUAL L (CDR L))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2 and restrict the type of the new variable L2 to be that of the term it replaces, as established by primitive type reasoning. This produces the following goal. Subgoal *1.3.4.2.3/3''' (IMPLIES (AND (CONSP L2) (TRUE-LISTP L2) (CONSP (CONS L1 L2)) (EQUAL (LEN L2) 0) (EQUAL L2 (LIST X3 X5 X1))) (EQUAL (CONS L1 L2) L2)). But simplification reduces this to T, using the :definition LEN, the :executable-counterparts of BINARY-+, EQUAL and LEN, primitive type reasoning and the :rewrite rule CDR-CONS. Subgoal *1.3.4.2.3/2 (IMPLIES (AND (CONSP L) (<= 2 (LEN (CDR L))) (< (LEN L) 2)) (EQUAL L (LIST X3 X5 X1))). This simplifies, using the :definition LEN, to Subgoal *1.3.4.2.3/2' (IMPLIES (AND (CONSP L) (<= 2 (LEN (CDR L))) (< (+ 1 (LEN (CDR L))) 2)) (EQUAL L (LIST X3 X5 X1))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule LEN. Subgoal *1.3.4.2.3/1 (IMPLIES (AND (CONSP L) (NOT (CONSP (CDR L))) (< (LEN L) 2)) (EQUAL L (LIST X3 X5 X1))). This simplifies, using the :definition LEN, primitive type reasoning and the :rewrite rule CDR-CONS, to Subgoal *1.3.4.2.3/1' (IMPLIES (AND (CONSP L) (NOT (CONSP (CDR L)))) (<= 2 (+ 1 (LEN (CDR L))))). This simplifies, using the :executable-counterparts of <, BINARY-+ and NOT, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3.4.2.3/1'' (IMPLIES (AND (EQUAL (LEN (CDR L)) 0) (CONSP L)) (CONSP (CDR L))). This simplifies, using the :definition LEN and the :executable- counterpart of EQUAL, to Subgoal *1.3.4.2.3/1''' (IMPLIES (CONSP L) (CONSP (CDR L))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3.4.2.3/1'4' (IMPLIES (CONSP (CONS L1 L2)) (CONSP L2)). This simplifies, using primitive type reasoning, to Subgoal *1.3.4.2.3/1'5' (CONSP L2). We suspect that this conjecture is not a theorem. We might as well be trying to prove Subgoal *1.3.4.2.3/1'6' NIL. Summary Form: ( DEFTHM ROTATE-LEN-GENERALIZATION ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION ENDP) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION DROPN) (:INDUCTION FIRSTN) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:REWRITE |(* a (/ a))|) (:REWRITE |(* y x)|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ x (- x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE |(+ y x)|) (:REWRITE |(< x (/ y)) with (< 0 y)|) (:REWRITE |(< y (+ (- c) x))|) (:REWRITE |(equal (+ (- c) x) y)|) (:REWRITE BUBBLE-DOWN-+-MATCH-1) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE CONS-CAR-CDR) (:REWRITE CONS-EQUAL) (:REWRITE DEFAULT-LESS-THAN-2) (:REWRITE NORMALIZE-ADDENDS) (:REWRITE REDUCE-ADDITIVE-CONSTANT-<) (:REWRITE REMOVE-STRICT-INEQUALITIES) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<) (:REWRITE SIMPLIFY-SUMS-<) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION FIRSTN) (:TYPE-PRESCRIPTION LEN)) Time: 0.73 seconds (prove: 0.56, print: 0.17, other: 0.00) Prover steps counted: 28180 --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary- limit. --- *** Key checkpoints before reverting to proof by induction: *** Subgoal 2 (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) Subgoal 1 (IMPLIES (AND (TRUE-LISTP X) (NOT (ACL2-NUMBERP N)) (<= 0 (LEN X))) (EQUAL X (APP X NIL))) *** Key checkpoints under a top-level induction: *** Subgoal *1/2.3 (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/2.2 (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/2.1' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) ACL2 Error in ( DEFTHM ROTATE-LEN-GENERALIZATION ...): See :DOC failure. ******** FAILED ******** ACL2 >(defthm app-x-nil (implies (true-listp x) (equal x (app x nil)))) ACL2 Error in ( DEFTHM APP-X-NIL ...): A :REWRITE rule generated from APP-X-NIL is illegal because it rewrites the variable symbol X. See :DOC rewrite. Summary Form: ( DEFTHM APP-X-NIL ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( DEFTHM APP-X-NIL ...): See :DOC failure. ******** FAILED ******** ACL2 >(defthm app-x-nil (implies (true-listp x) (equal (app x nil) x))) Name the formula above *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 (APP X 'NIL). This suggestion was produced using the :induction rules APP and TRUE-LISTP. 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 APP. When applied to the goal at hand the above induction scheme produces three nontautological subgoals. Subgoal *1/3 (IMPLIES (AND (NOT (ENDP X)) (EQUAL (APP (CDR X) NIL) (CDR X)) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (CONSP X) (EQUAL (APP (CDR X) NIL) (CDR X)) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But simplification reduces this to T, using the :definitions APP and TRUE-LISTP, primitive type reasoning and the :rewrite rule CONS-CAR-CDR. Subgoal *1/2 (IMPLIES (AND (NOT (ENDP X)) (NOT (TRUE-LISTP (CDR X))) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1/1 (IMPLIES (AND (ENDP X) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). By the simple :definition ENDP we reduce the conjecture to Subgoal *1/1' (IMPLIES (AND (NOT (CONSP X)) (TRUE-LISTP X)) (EQUAL (APP X NIL) X)). But simplification reduces this to T, using the :definition TRUE-LISTP, the :executable-counterparts of APP, CONSP and EQUAL and primitive type reasoning. That completes the proof of *1. Q.E.D. Summary Form: ( DEFTHM APP-X-NIL ...) Rules: ((:DEFINITION APP) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION TRUE-LISTP) (:REWRITE CONS-CAR-CDR)) Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) Prover steps counted: 245 APP-X-NIL ACL2 >(defthm rotate-len-generalization (implies (and (true-listp x) (<= n (len x))) (equal (rotate n x) (app (dropn n x) (firstn n x))))) This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, ROTATE and SYNP, primitive type reasoning and the :rewrite rules APP-X-NIL and DEFAULT-LESS-THAN-2, to Goal' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). Name the formula above *1. Perhaps we can prove *1 by induction. Five 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 (ROTATE N X). This suggestion was produced using the :induction rules DROPN, FIRSTN and ROTATE. If we let (:P N X) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP N)) (:P (+ -1 N) (APP (CDR X) (LIST (CAR X))))) (:P N X)) (IMPLIES (ZP N) (:P N X))). This induction is justified by the same argument used to admit ROTATE. 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 (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE and TRUE-LISTP, the :executable-counterparts of APP, CAR, CDR, CONS, CONSP and LEN and primitive type reasoning, to Subgoal *1/5' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/5'' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1))))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/5''' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1))))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We now use the second hypothesis by substituting (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1)))) for (ROTATE (+ -1 N) (APP X2 (LIST X1))) and throwing away the hypothesis. This produces Subgoal *1/5'4' (IMPLIES (AND (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (APP (DROPN (+ -1 N) (APP X2 (LIST X1))) (FIRSTN (+ -1 N) (APP X2 (LIST X1)))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We generalize this conjecture, replacing (+ -1 N) by I and restricting the type of the new variable I to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1/5'5' (IMPLIES (AND (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (APP (DROPN I (APP X2 (LIST X1))) (FIRSTN I (APP X2 (LIST X1)))) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). By case analysis we reduce the conjecture to Subgoal *1/5'6' (IMPLIES (AND (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (APP (DROPN I (APP X2 (LIST X1))) (FIRSTN I (APP X2 (LIST X1)))) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Name the formula above *1.1. Subgoal *1/4 (IMPLIES (AND (NOT (ZP N)) (< (LEN (APP (CDR X) (LIST (CAR X)))) (+ -1 N)) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of APP, BINARY-+, CAR, CDR, CONS, CONSP, LEN and UNARY--, primitive type reasoning, the :rewrite rule |(< y (+ (- c) x))| and the :type-prescription rule LEN, to Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/4'' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (ZP N)) (< (+ 1 (LEN (APP X2 (LIST X1)))) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/4''' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP X2 (LIST X1)))) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We generalize this conjecture, replacing (APP X2 (LIST X1)) by L and (+ -1 N) by I and restricting the types of the new variables L and I to be those of the terms they replace, as established by primitive type reasoning and APP and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1/4'4' (IMPLIES (AND (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). By case analysis we reduce the conjecture to Subgoal *1/4'5' (IMPLIES (AND (CONSP L) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (< (+ 1 (LEN L)) N) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Name the formula above *1.2. Subgoal *1/3 (IMPLIES (AND (NOT (ZP N)) (NOT (ACL2-NUMBERP (+ -1 N))) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1/2 (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE and TRUE-LISTP, the :executable-counterparts of APP, CAR, CDR, CONS, CONSP, LEN and TRUE-LISTP and primitive type reasoning, to Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))). The destructor terms (CAR X) and (CDR X) can be eliminated by using CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2. This produces the following goal. Subgoal *1/2'' (IMPLIES (AND (CONSP (CONS X1 X2)) (NOT (ZP N)) (NOT (TRUE-LISTP (APP X2 (LIST X1)))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). This simplifies, using primitive type reasoning, to Subgoal *1/2''' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP X2 (LIST X1)))) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE (+ -1 N) (APP X2 (LIST X1))) (APP (DROPN (+ -1 N) X2) (CONS X1 (FIRSTN (+ -1 N) X2))))). We generalize this conjecture, replacing (APP X2 (LIST X1)) by L and (+ -1 N) by I and restricting the types of the new variables L and I to be those of the terms they replace, as established by primitive type reasoning and APP and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1/2'4' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (NOT (TRUE-LISTP L)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). By case analysis we reduce the conjecture to Subgoal *1/2'5' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Name the formula above *1.3. Subgoal *1/1 (IMPLIES (AND (ZP N) (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))). But simplification reduces this to T, using the :compound- recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN and ROTATE, primitive type reasoning and the :rewrite rule APP-X-NIL. So we now return to *1.3, which is (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Perhaps we can prove *1.3 by induction. Six induction schemes are suggested by this conjecture. Subsumption reduces that number to four. 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 (ROTATE I L), but modified to accommodate (FIRSTN I X2). These suggestions were produced using the :induction rules DROPN, FIRSTN, LEN, ROTATE and TRUE-LISTP. If we let (:P I L N X1 X2) denote *1.3 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ZP I)) (:P (+ -1 I) (APP (CDR L) (LIST (CAR L))) N X1 (CDR X2))) (:P I L N X1 X2)) (IMPLIES (ZP I) (:P I L N X1 X2))). This induction is justified by the same argument used to admit ROTATE. Note, however, that the unmeasured variables X2 and L are being instantiated. When applied to the goal at hand the above induction scheme produces eight nontautological subgoals. Subgoal *1.3/8 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (CONS X1 (FIRSTN (+ -1 I) (CDR X2))))) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CAR, CDR, CONSP and LEN, primitive type reasoning and the :rewrite rules |(+ c (+ d x))| and REMOVE-WEAK-INEQUALITIES, to the following two conjectures. Subgoal *1.3/8.2 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (CONS X1 (FIRSTN (+ -1 I) (CDR X2))))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/8.2' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/8.2'' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/8.2''' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/8.2'4' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4)))) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We now use the second hypothesis by substituting (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4))) for (ROTATE (+ -1 I) (APP L2 (LIST L1))) and throwing away the hypothesis. This produces Subgoal *1.3/8.2'5' (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP (DROPN (+ -1 I) X4) (CONS X1 (FIRSTN (+ -1 I) X4))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We generalize this conjecture, replacing (+ -1 I) by J and restricting the type of the new variable J to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/8.2'6' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP (DROPN J X4) (CONS X1 (FIRSTN J X4))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). By case analysis we reduce the conjecture to Subgoal *1.3/8.2'7' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP (DROPN J X4) (CONS X1 (FIRSTN J X4))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). We generalize this conjecture, replacing (FIRSTN J X4) by FN and (DROPN J X4) by DN and restricting the type of the new variable FN to be that of the term it replaces, as established by FIRSTN. This produces Subgoal *1.3/8.2'8' (IMPLIES (AND (TRUE-LISTP FN) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP DN (CONS X1 FN)) (APP DN (LIST* X1 X3 FN)))). We suspect that the terms (NOT (TRUE-LISTP L2)) and (NOT (ZP I)) are irrelevant to the truth of this conjecture and throw them out. We will thus try to prove Subgoal *1.3/8.2'9' (IMPLIES (AND (TRUE-LISTP FN) (INTEGERP J) (<= 0 J) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (APP DN (CONS X1 FN)) (APP DN (LIST* X1 X3 FN)))). Name the formula above *1.3.1. Subgoal *1.3/8.1 (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) NIL) (CONS X1 (FIRSTN (+ -1 I) NIL)))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (NOT X2) (<= N 1)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of < and ZP and linear arithmetic, to Subgoal *1.3/8.1' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) NIL) (CONS X1 (FIRSTN (+ -1 I) NIL)))) (CONSP L) (NOT (TRUE-LISTP (CDR L)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/8.1'' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) NIL) (CONS X1 (FIRSTN (+ -1 I) NIL)))) (NOT (TRUE-LISTP L2))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/8.1''' (IMPLIES (AND (NOT (ZP I)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) NIL) (CONS X1 (FIRSTN (+ -1 I) NIL)))) (NOT (TRUE-LISTP L2))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). We now use the second hypothesis by substituting (APP (DROPN (+ -1 I) NIL) (CONS X1 (FIRSTN (+ -1 I) NIL))) for (ROTATE (+ -1 I) (APP L2 (LIST L1))) and throwing away the hypothesis. This produces Subgoal *1.3/8.1'4' (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP L2))) (EQUAL (APP (DROPN (+ -1 I) NIL) (CONS X1 (FIRSTN (+ -1 I) NIL))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). We generalize this conjecture, replacing (+ -1 I) by J and restricting the type of the new variable J to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/8.1'5' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2))) (EQUAL (APP (DROPN J NIL) (CONS X1 (FIRSTN J NIL))) (APP (DROPN J NIL) (LIST* X1 NIL (FIRSTN J NIL))))). By case analysis we reduce the conjecture to Subgoal *1.3/8.1'6' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2))) (EQUAL (APP (DROPN J NIL) (CONS X1 (FIRSTN J NIL))) (APP (DROPN J NIL) (LIST* X1 NIL (FIRSTN J NIL))))). We generalize this conjecture, replacing (FIRSTN J NIL) by FN and (DROPN J NIL) by DN and restricting the type of the new variable FN to be that of the term it replaces, as established by FIRSTN. This produces Subgoal *1.3/8.1'7' (IMPLIES (AND (TRUE-LISTP FN) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2))) (EQUAL (APP DN (CONS X1 FN)) (APP DN (LIST* X1 NIL FN)))). We suspect that the terms (NOT (TRUE-LISTP L2)) and (NOT (ZP I)) are irrelevant to the truth of this conjecture and throw them out. We will thus try to prove Subgoal *1.3/8.1'8' (IMPLIES (AND (TRUE-LISTP FN) (INTEGERP J) (<= 0 J)) (EQUAL (APP DN (CONS X1 FN)) (APP DN (LIST* X1 NIL FN)))). Name the formula above *1.3.2. Subgoal *1.3/7 (IMPLIES (AND (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CDR, CONSP and LEN, primitive type reasoning and the :rewrite rules |(+ c (+ d x))| and REMOVE-WEAK-INEQUALITIES, to Subgoal *1.3/7' (IMPLIES (AND (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, linear arithmetic, primitive type reasoning and the :type-prescription rule LEN, to Subgoal *1.3/7'' (IMPLIES (AND (EQUAL (LEN (CDR X2)) (+ -2 N)) (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions SYNP and TRUE-LISTP, the :executable-counterparts of < and UNARY--, primitive type reasoning, the :rewrite rules |(* a (/ a))|, |(* y x)|, |(< x (/ y)) with (< 0 y)|, |(equal (+ (- c) x) y)| and SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-< and the :type-prescription rule LEN, to Subgoal *1.3/7''' (IMPLIES (AND (EQUAL N (+ 2 (LEN (CDR X2)))) (NOT (ZP I)) (< (+ 1 (LEN (CDR X2))) N) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). This simplifies, using the :definition SYNP, the :executable- counterparts of < and BINARY-+, primitive type reasoning, the :rewrite rules |(+ 0 x)|, |(+ c (+ d x))|, |(+ x (- x))|, |(+ y (+ x z))|, |(+ y x)|, BUBBLE-DOWN-+-MATCH-1, NORMALIZE-ADDENDS, REDUCE-ADDITIVE-CONSTANT-< and SIMPLIFY-SUMS-< and the :type-prescription rule LEN, to Subgoal *1.3/7'4' (IMPLIES (AND (NOT (ZP I)) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (CONSP X2) (TRUE-LISTP (CDR X2))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/7'5' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/7'6' (IMPLIES (AND (NOT (ZP I)) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/7'7' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/7'8' (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (TRUE-LISTP X4)) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We generalize this conjecture, replacing (+ -1 I) by J and restricting the type of the new variable J to be that of the term it replaces, as established by primitive type reasoning and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/7'9' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (TRUE-LISTP X4)) (EQUAL (ROTATE J (APP L2 (LIST L1))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). By case analysis we reduce the conjecture to Subgoal *1.3/7'10' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (TRUE-LISTP X4)) (EQUAL (ROTATE J (APP L2 (LIST L1))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). We suspect that the term (NOT (ZP I)) is irrelevant to the truth of this conjecture and throw it out. We will thus try to prove Subgoal *1.3/7'11' (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (TRUE-LISTP L2)) (TRUE-LISTP X4)) (EQUAL (ROTATE J (APP L2 (LIST L1))) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). Name the formula above *1.3.3. Subgoal *1.3/6 (IMPLIES (AND (NOT (ZP I)) (NOT (TRUE-LISTP (CDR X2))) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.3/5 (IMPLIES (AND (NOT (ZP I)) (< (+ -1 I) 0) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.3/4 (IMPLIES (AND (NOT (ZP I)) (NOT (INTEGERP (+ -1 I))) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER and primitive type reasoning. Subgoal *1.3/3 (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP (CDR L) (LIST (CAR L)))) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CONSP and LEN, primitive type reasoning and the :rewrite rules |(+ c (+ d x))| and REMOVE-WEAK-INEQUALITIES, to the following two conjectures. Subgoal *1.3/3.2 (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP (CDR L) (LIST (CAR L)))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) (CDR X2)) (LIST* X1 (CAR X2) (FIRSTN (+ -1 I) (CDR X2)))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/3.2' (IMPLIES (AND (CONSP (CONS X3 X4)) (NOT (ZP I)) (TRUE-LISTP (APP (CDR L) (LIST (CAR L)))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/3.2'' (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP (CDR L) (LIST (CAR L)))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/3.2''' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (TRUE-LISTP (APP L2 (LIST L1))) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/3.2'4' (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP L2 (LIST L1))) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) X4) (LIST* X1 X3 (FIRSTN (+ -1 I) X4))))). We generalize this conjecture, replacing (APP L2 (LIST L1)) by L and (+ -1 I) by J and restricting the types of the new variables L and J to be those of the terms they replace, as established by primitive type reasoning and APP and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/3.2'5' (IMPLIES (AND (CONSP L) (TRUE-LISTP L) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE J L) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). By case analysis we reduce the conjecture to Subgoal *1.3/3.2'6' (IMPLIES (AND (CONSP L) (TRUE-LISTP L) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE J L) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). We suspect that the terms (NOT (TRUE-LISTP L2)) and (NOT (ZP I)) are irrelevant to the truth of this conjecture and throw them out. We will thus try to prove Subgoal *1.3/3.2'7' (IMPLIES (AND (CONSP L) (TRUE-LISTP L) (INTEGERP J) (<= 0 J) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL (ROTATE J L) (APP (DROPN J X4) (LIST* X1 X3 (FIRSTN J X4))))). Name the formula above *1.3.4. Subgoal *1.3/3.1 (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP (CDR L) (LIST (CAR L)))) (CONSP L) (NOT (TRUE-LISTP (CDR L))) (NOT (ZP N)) (NOT X2) (<= N 1)) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN I NIL) (CONS X1 (FIRSTN I NIL))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of < and ZP and linear arithmetic, to Subgoal *1.3/3.1' (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP (CDR L) (LIST (CAR L)))) (CONSP L) (NOT (TRUE-LISTP (CDR L)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN I NIL) (CONS X1 (FIRSTN I NIL))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :definitions DROPN and FIRSTN and the :executable-counterparts of CAR and CDR, to Subgoal *1.3/3.1'' (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP (CDR L) (LIST (CAR L)))) (CONSP L) (NOT (TRUE-LISTP (CDR L)))) (EQUAL (ROTATE (+ -1 I) (APP (CDR L) (LIST (CAR L)))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3/3.1''' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (ZP I)) (TRUE-LISTP (APP L2 (LIST L1))) (NOT (TRUE-LISTP L2))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/3.1'4' (IMPLIES (AND (NOT (ZP I)) (TRUE-LISTP (APP L2 (LIST L1))) (NOT (TRUE-LISTP L2))) (EQUAL (ROTATE (+ -1 I) (APP L2 (LIST L1))) (APP (DROPN (+ -1 I) NIL) (LIST* X1 NIL (FIRSTN (+ -1 I) NIL))))). We generalize this conjecture, replacing (APP L2 (LIST L1)) by L and (+ -1 I) by J and restricting the types of the new variables L and J to be those of the terms they replace, as established by primitive type reasoning and APP and ZP-COMPOUND-RECOGNIZER. This produces Subgoal *1.3/3.1'5' (IMPLIES (AND (CONSP L) (TRUE-LISTP L) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2))) (EQUAL (ROTATE J L) (APP (DROPN J NIL) (LIST* X1 NIL (FIRSTN J NIL))))). By case analysis we reduce the conjecture to Subgoal *1.3/3.1'6' (IMPLIES (AND (CONSP L) (TRUE-LISTP L) (INTEGERP J) (<= 0 J) (NOT (ZP I)) (NOT (TRUE-LISTP L2))) (EQUAL (ROTATE J L) (APP (DROPN J NIL) (LIST* X1 NIL (FIRSTN J NIL))))). We suspect that the terms (NOT (TRUE-LISTP L2)) and (NOT (ZP I)) are irrelevant to the truth of this conjecture and throw them out. We will thus try to prove Subgoal *1.3/3.1'7' (IMPLIES (AND (CONSP L) (TRUE-LISTP L) (INTEGERP J) (<= 0 J)) (EQUAL (ROTATE J L) (APP (DROPN J NIL) (LIST* X1 NIL (FIRSTN J NIL))))). Name the formula above *1.3.5. Subgoal *1.3/2 (IMPLIES (AND (NOT (ZP I)) (NOT (CONSP (APP (CDR L) (LIST (CAR L))))) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). But we reduce the conjecture to T, by primitive type reasoning and the :type-prescription rule APP. Subgoal *1.3/1 (IMPLIES (AND (ZP I) (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of <, INTEGERP, NOT and ZP and linear arithmetic, to Subgoal *1.3/1' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE 0 L) (APP (DROPN 0 X2) (CONS X1 (FIRSTN 0 X2))))). This simplifies, using the :definitions APP, DROPN, FIRSTN, LEN, ROTATE, SYNP and TRUE-LISTP, the :executable-counterparts of BINARY-+, CONSP, DROPN, FIRSTN, LEN and ZP, primitive type reasoning and the :rewrite rule |(+ c (+ d x))|, to the following two conjectures. Subgoal *1.3/1.2 (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL L (APP X2 (LIST X1)))). This simplifies, using the :definition APP, to Subgoal *1.3/1.2' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (CONSP X2) (TRUE-LISTP (CDR X2)) (<= N (+ 2 (LEN (CDR X2))))) (EQUAL L (CONS (CAR X2) (APP (CDR X2) (LIST X1))))). The destructor terms (CAR X2) and (CDR X2) can be eliminated by using CAR-CDR-ELIM to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. This produces the following goal. Subgoal *1.3/1.2'' (IMPLIES (AND (CONSP (CONS X3 X4)) (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). This simplifies, using primitive type reasoning, to Subgoal *1.3/1.2''' (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (TRUE-LISTP X4) (<= N (+ 2 (LEN X4)))) (EQUAL L (CONS X3 (APP X4 (LIST X1))))). Name the formula above *1.3.6. Subgoal *1.3/1.1 (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (NOT (ZP N)) (NOT X2)) (< 1 N)). This simplifies, using the :compound-recognizer rule ZP-COMPOUND-RECOGNIZER, the :executable-counterparts of < and ZP and linear arithmetic, to Subgoal *1.3/1.1' (IMPLIES (CONSP L) (TRUE-LISTP L)). Name the formula above *1.3.7. Perhaps we can prove *1.3.7 by induction. One induction scheme is suggested by this conjecture. We will induct according to a scheme suggested by (TRUE-LISTP L). This suggestion was produced using the :induction rule TRUE-LISTP. If we let (:P L) denote *1.3.7 above then the induction scheme we'll use is (AND (IMPLIES (NOT (CONSP L)) (:P L)) (IMPLIES (AND (CONSP L) (:P (CDR L))) (:P L))). This induction is justified by the same argument used to admit TRUE-LISTP. When applied to the goal at hand the above induction scheme produces two nontautological subgoals. Subgoal *1.3.7/2 (IMPLIES (AND (CONSP L) (TRUE-LISTP (CDR L))) (TRUE-LISTP L)). But we reduce the conjecture to T, by primitive type reasoning. Subgoal *1.3.7/1 (IMPLIES (AND (CONSP L) (NOT (CONSP (CDR L)))) (TRUE-LISTP L)). This simplifies, using the :definition TRUE-LISTP, to Subgoal *1.3.7/1' (IMPLIES (AND (CONSP L) (NOT (CONSP (CDR L)))) (TRUE-LISTP (CDR L))). This simplifies, using the :definition TRUE-LISTP and primitive type reasoning, to Subgoal *1.3.7/1'' (IMPLIES (AND (CONSP L) (NOT (CONSP (CDR L)))) (NOT (CDR L))). The destructor terms (CAR L) and (CDR L) can be eliminated by using CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L) by L2. This produces the following goal. Subgoal *1.3.7/1''' (IMPLIES (AND (CONSP (CONS L1 L2)) (NOT (CONSP L2))) (NOT L2)). This simplifies, using primitive type reasoning, to Subgoal *1.3.7/1'4' (IMPLIES (NOT (CONSP L2)) (NOT L2)). Name the formula above *1.3.7.1. No induction schemes are suggested by *1.3.7.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ROTATE-LEN-GENERALIZATION ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DROPN) (:INDUCTION FIRSTN) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:REWRITE |(* a (/ a))|) (:REWRITE |(* y x)|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ x (- x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE |(+ y x)|) (:REWRITE |(< x (/ y)) with (< 0 y)|) (:REWRITE |(< y (+ (- c) x))|) (:REWRITE |(equal (+ (- c) x) y)|) (:REWRITE APP-X-NIL) (:REWRITE BUBBLE-DOWN-+-MATCH-1) (:REWRITE DEFAULT-LESS-THAN-2) (:REWRITE NORMALIZE-ADDENDS) (:REWRITE REDUCE-ADDITIVE-CONSTANT-<) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<) (:REWRITE SIMPLIFY-SUMS-<) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION FIRSTN) (:TYPE-PRESCRIPTION LEN)) Time: 0.51 seconds (prove: 0.41, print: 0.09, other: 0.00) Prover steps counted: 22239 --- 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' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *** Key checkpoints under a top-level induction: *** Subgoal *1/5' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) ACL2 Error in ( DEFTHM ROTATE-LEN-GENERALIZATION ...): See :DOC failure. ******** FAILED ******** ACL2 >:set-gag-mode :goals ACL2 >(defthm rotate-len-generalization (implies (and (true-listp x) (<= n (len x))) (equal (rotate n x) (app (dropn n x) (firstn n x))))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/5 Subgoal *1/5' Subgoal *1/5'' Subgoal *1/5''' Subgoal *1/5'4' Subgoal *1/5'5' Subgoal *1/5'6' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/5' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.1 (Subgoal *1/5'6') is pushed for proof by induction. ]) Subgoal *1/4 Subgoal *1/4' Subgoal *1/4'' Subgoal *1/4''' Subgoal *1/4'4' Subgoal *1/4'5' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.2 (Subgoal *1/4'5') is pushed for proof by induction. ]) Subgoal *1/3 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 (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.3 (Subgoal *1/2'5') is pushed for proof by induction. ]) Subgoal *1/1 So we now return to *1.3, which is (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Subgoal *1.3/8 Subgoal *1.3/8.2 Subgoal *1.3/8.2' Subgoal *1.3/8.2'' Subgoal *1.3/8.2''' Subgoal *1.3/8.2'4' Subgoal *1.3/8.2'5' Subgoal *1.3/8.2'6' Subgoal *1.3/8.2'7' Subgoal *1.3/8.2'8' Subgoal *1.3/8.2'9' *1.3.1 (Subgoal *1.3/8.2'9') is pushed for proof by induction. Subgoal *1.3/8.1 Subgoal *1.3/8.1' Subgoal *1.3/8.1'' Subgoal *1.3/8.1''' Subgoal *1.3/8.1'4' Subgoal *1.3/8.1'5' Subgoal *1.3/8.1'6' Subgoal *1.3/8.1'7' Subgoal *1.3/8.1'8' *1.3.2 (Subgoal *1.3/8.1'8') is pushed for proof by induction. Subgoal *1.3/7 Subgoal *1.3/7' Subgoal *1.3/7'' Subgoal *1.3/7''' Subgoal *1.3/7'4' Subgoal *1.3/7'5' Subgoal *1.3/7'6' Subgoal *1.3/7'7' Subgoal *1.3/7'8' Subgoal *1.3/7'9' Subgoal *1.3/7'10' Subgoal *1.3/7'11' *1.3.3 (Subgoal *1.3/7'11') is pushed for proof by induction. Subgoal *1.3/6 Subgoal *1.3/5 Subgoal *1.3/4 Subgoal *1.3/3 Subgoal *1.3/3.2 Subgoal *1.3/3.2' Subgoal *1.3/3.2'' Subgoal *1.3/3.2''' Subgoal *1.3/3.2'4' Subgoal *1.3/3.2'5' Subgoal *1.3/3.2'6' Subgoal *1.3/3.2'7' *1.3.4 (Subgoal *1.3/3.2'7') is pushed for proof by induction. Subgoal *1.3/3.1 Subgoal *1.3/3.1' Subgoal *1.3/3.1'' Subgoal *1.3/3.1''' Subgoal *1.3/3.1'4' Subgoal *1.3/3.1'5' Subgoal *1.3/3.1'6' Subgoal *1.3/3.1'7' *1.3.5 (Subgoal *1.3/3.1'7') is pushed for proof by induction. Subgoal *1.3/2 Subgoal *1.3/1 Subgoal *1.3/1' Subgoal *1.3/1.2 Subgoal *1.3/1.2' Subgoal *1.3/1.2'' Subgoal *1.3/1.2''' *1.3.6 (Subgoal *1.3/1.2''') is pushed for proof by induction. Subgoal *1.3/1.1 Subgoal *1.3/1.1' *1.3.7 (Subgoal *1.3/1.1') is pushed for proof by induction. So we now return to *1.3.7, which is (IMPLIES (CONSP L) (TRUE-LISTP L)). Subgoal *1.3.7/2 Subgoal *1.3.7/1 Subgoal *1.3.7/1' Subgoal *1.3.7/1'' Subgoal *1.3.7/1''' Subgoal *1.3.7/1'4' *1.3.7.1 (Subgoal *1.3.7/1'4') is pushed for proof by induction. So we now return to *1.3.7.1, which is (IMPLIES (NOT (CONSP L2)) (NOT L2)). No induction schemes are suggested by *1.3.7.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ROTATE-LEN-GENERALIZATION ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DROPN) (:INDUCTION FIRSTN) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:REWRITE |(* a (/ a))|) (:REWRITE |(* y x)|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ x (- x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE |(+ y x)|) (:REWRITE |(< x (/ y)) with (< 0 y)|) (:REWRITE |(< y (+ (- c) x))|) (:REWRITE |(equal (+ (- c) x) y)|) (:REWRITE APP-X-NIL) (:REWRITE BUBBLE-DOWN-+-MATCH-1) (:REWRITE DEFAULT-LESS-THAN-2) (:REWRITE NORMALIZE-ADDENDS) (:REWRITE REDUCE-ADDITIVE-CONSTANT-<) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<) (:REWRITE SIMPLIFY-SUMS-<) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION FIRSTN) (:TYPE-PRESCRIPTION LEN)) Time: 0.34 seconds (prove: 0.33, print: 0.01, other: 0.00) Prover steps counted: 22239 --- 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' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *** Key checkpoints under a top-level induction *** *** (see :DOC pso to view induction schemes): *** Subgoal *1/5' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) ACL2 Error in ( DEFTHM ROTATE-LEN-GENERALIZATION ...): See :DOC failure. ******** FAILED ******** ACL2 >:pbt 0 0 (EXIT-BOOT-STRAP-MODE) L 1 (DEFUN APP (X Y) ...) L 2 (DEFUN ROTATE (N X) ...) d 3 (INCLUDE-BOOK "arithmetic-5/top" :DIR ...) L 4 (DEFUN FIRSTN (N X) ...) L 5 (DEFUN DROPN (N X) ...) 6:x(DEFTHM APP-X-NIL ...) ACL2 >(include-book "arithmetic-5/top" :dir :system) The event ( INCLUDE-BOOK "arithmetic-5/top" ...) is redundant. See :DOC redundant-events. Summary Form: ( INCLUDE-BOOK "arithmetic-5/top" ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :REDUNDANT ACL2 >(defthm dropn-app (implies (and (natp n) (<= n (len x))) (equal (dropn n (app x y)) (app (dropn n x) y)))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (INTEGERP N) (<= 0 N) (<= N (LEN X))) (EQUAL (DROPN N (APP X Y)) (APP (DROPN N X) Y))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/5 Subgoal *1/4 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: ( DEFTHM DROPN-APP ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION LEN) (:DEFINITION NATP) (:DEFINITION NOT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION DROPN) (:INDUCTION LEN) (:REWRITE |(< y (+ (- c) x))|) (:REWRITE CDR-CONS) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:TYPE-PRESCRIPTION LEN)) Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 596 DROPN-APP ACL2 >(defthm rotate-len-generalization (implies (and (true-listp x) (<= n (len x))) (equal (rotate n x) (app (dropn n x) (firstn n x))))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/5 Subgoal *1/5' Subgoal *1/5'' Subgoal *1/5''' Subgoal *1/5'4' Subgoal *1/5'5' Subgoal *1/5'6' Subgoal *1/5'7' Subgoal *1/5'8' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/5'' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (APP (DROPN (+ -1 N) (CDR X)) (LIST (CAR X))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.1 (Subgoal *1/5'8') is pushed for proof by induction. ]) Subgoal *1/4 Subgoal *1/4' Subgoal *1/4'' Subgoal *1/4''' Subgoal *1/4'4' Subgoal *1/4'5' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.2 (Subgoal *1/4'5') is pushed for proof by induction. ]) Subgoal *1/3 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 (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.3 (Subgoal *1/2'5') is pushed for proof by induction. ]) Subgoal *1/1 So we now return to *1.3, which is (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Subgoal *1.3/8 Subgoal *1.3/8.2 Subgoal *1.3/8.2' Subgoal *1.3/8.2'' Subgoal *1.3/8.2''' Subgoal *1.3/8.2'4' Subgoal *1.3/8.2'5' Subgoal *1.3/8.2'6' Subgoal *1.3/8.2'7' Subgoal *1.3/8.2'8' Subgoal *1.3/8.2'9' *1.3.1 (Subgoal *1.3/8.2'9') is pushed for proof by induction. Subgoal *1.3/8.1 Subgoal *1.3/8.1' Subgoal *1.3/8.1'' Subgoal *1.3/8.1''' Subgoal *1.3/8.1'4' Subgoal *1.3/8.1'5' Subgoal *1.3/8.1'6' Subgoal *1.3/8.1'7' Subgoal *1.3/8.1'8' *1.3.2 (Subgoal *1.3/8.1'8') is pushed for proof by induction. Subgoal *1.3/7 Subgoal *1.3/7' Subgoal *1.3/7'' Subgoal *1.3/7''' Subgoal *1.3/7'4' Subgoal *1.3/7'5' Subgoal *1.3/7'6' Subgoal *1.3/7'7' Subgoal *1.3/7'8' Subgoal *1.3/7'9' Subgoal *1.3/7'10' Subgoal *1.3/7'11' *1.3.3 (Subgoal *1.3/7'11') is pushed for proof by induction. Subgoal *1.3/6 Subgoal *1.3/5 Subgoal *1.3/4 Subgoal *1.3/3 Subgoal *1.3/3.2 Subgoal *1.3/3.2' Subgoal *1.3/3.2'' Subgoal *1.3/3.2''' Subgoal *1.3/3.2'4' Subgoal *1.3/3.2'5' Subgoal *1.3/3.2'6' Subgoal *1.3/3.2'7' *1.3.4 (Subgoal *1.3/3.2'7') is pushed for proof by induction. Subgoal *1.3/3.1 Subgoal *1.3/3.1' Subgoal *1.3/3.1'' Subgoal *1.3/3.1''' Subgoal *1.3/3.1'4' Subgoal *1.3/3.1'5' Subgoal *1.3/3.1'6' Subgoal *1.3/3.1'7' *1.3.5 (Subgoal *1.3/3.1'7') is pushed for proof by induction. Subgoal *1.3/2 Subgoal *1.3/1 Subgoal *1.3/1' Subgoal *1.3/1.2 Subgoal *1.3/1.2' Subgoal *1.3/1.2'' Subgoal *1.3/1.2''' *1.3.6 (Subgoal *1.3/1.2''') is pushed for proof by induction. Subgoal *1.3/1.1 Subgoal *1.3/1.1' *1.3.7 (Subgoal *1.3/1.1') is pushed for proof by induction. So we now return to *1.3.7, which is (IMPLIES (CONSP L) (TRUE-LISTP L)). Subgoal *1.3.7/2 Subgoal *1.3.7/1 Subgoal *1.3.7/1' Subgoal *1.3.7/1'' Subgoal *1.3.7/1''' Subgoal *1.3.7/1'4' *1.3.7.1 (Subgoal *1.3.7/1'4') is pushed for proof by induction. So we now return to *1.3.7.1, which is (IMPLIES (NOT (CONSP L2)) (NOT L2)). No induction schemes are suggested by *1.3.7.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ROTATE-LEN-GENERALIZATION ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DROPN) (:INDUCTION FIRSTN) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:REWRITE |(* a (/ a))|) (:REWRITE |(* y x)|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ x (- x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE |(+ y x)|) (:REWRITE |(< x (/ y)) with (< 0 y)|) (:REWRITE |(< y (+ (- c) x))|) (:REWRITE |(equal (+ (- c) x) y)|) (:REWRITE APP-X-NIL) (:REWRITE BUBBLE-DOWN-+-MATCH-1) (:REWRITE DEFAULT-LESS-THAN-2) (:REWRITE DROPN-APP) (:REWRITE NORMALIZE-ADDENDS) (:REWRITE REDUCE-ADDITIVE-CONSTANT-<) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<) (:REWRITE SIMPLIFY-SUMS-<) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION FIRSTN) (:TYPE-PRESCRIPTION LEN)) Time: 0.35 seconds (prove: 0.34, print: 0.01, other: 0.00) Prover steps counted: 22968 --- 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' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *** Key checkpoints under a top-level induction *** *** (see :DOC pso to view induction schemes): *** Subgoal *1/5'' (IMPLIES (AND (NOT (ZP N)) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (APP (DROPN (+ -1 N) (CDR X)) (LIST (CAR X))) (FIRSTN (+ -1 N) (APP (CDR X) (LIST (CAR X)))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) ACL2 Error in ( DEFTHM ROTATE-LEN-GENERALIZATION ...): See :DOC failure. ******** FAILED ******** ACL2 >(defthm app-assoc (equal (app (app x y) z) (app x (app y z)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. 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 APP-ASSOC ...) Rules: ((:DEFINITION APP) (:DEFINITION ENDP) (:DEFINITION NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 400 APP-ASSOC ACL2 >(defthm firstn-app (implies (and (natp n) (<= n (len x))) (equal (firstn n (app x y)) (firstn n x)))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (INTEGERP N) (<= 0 N) (<= N (LEN X))) (EQUAL (FIRSTN N (APP X Y)) (FIRSTN N X))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/5 Subgoal *1/4 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: ( DEFTHM FIRSTN-APP ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NATP) (:DEFINITION NOT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION FIRSTN) (:INDUCTION LEN) (:REWRITE |(< y (+ (- c) x))|) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:TYPE-PRESCRIPTION LEN)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 512 FIRSTN-APP ACL2 >(defthm rotate-len-generalization (implies (and (true-listp x) (<= n (len x))) (equal (rotate n x) (app (dropn n x) (firstn n x))))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/5 Subgoal *1/5' Subgoal *1/4 Subgoal *1/4' Subgoal *1/4'' Subgoal *1/4''' Subgoal *1/4'4' Subgoal *1/4'5' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.1 (Subgoal *1/4'5') is pushed for proof by induction. ]) Subgoal *1/3 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 (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.2 (Subgoal *1/2'5') is pushed for proof by induction. ]) Subgoal *1/1 So we now return to *1.2, which is (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Subgoal *1.2/8 Subgoal *1.2/8.2 Subgoal *1.2/8.2' Subgoal *1.2/8.2'' Subgoal *1.2/8.2''' Subgoal *1.2/8.2'4' Subgoal *1.2/8.2'5' Subgoal *1.2/8.2'6' Subgoal *1.2/8.2'7' Subgoal *1.2/8.2'8' Subgoal *1.2/8.2'9' *1.2.1 (Subgoal *1.2/8.2'9') is pushed for proof by induction. Subgoal *1.2/8.1 Subgoal *1.2/8.1' Subgoal *1.2/8.1'' Subgoal *1.2/8.1''' Subgoal *1.2/8.1'4' Subgoal *1.2/8.1'5' Subgoal *1.2/8.1'6' Subgoal *1.2/8.1'7' Subgoal *1.2/8.1'8' *1.2.2 (Subgoal *1.2/8.1'8') is pushed for proof by induction. Subgoal *1.2/7 Subgoal *1.2/7' Subgoal *1.2/7'' Subgoal *1.2/7''' Subgoal *1.2/7'4' Subgoal *1.2/7'5' Subgoal *1.2/7'6' Subgoal *1.2/7'7' Subgoal *1.2/7'8' Subgoal *1.2/7'9' Subgoal *1.2/7'10' Subgoal *1.2/7'11' *1.2.3 (Subgoal *1.2/7'11') is pushed for proof by induction. Subgoal *1.2/6 Subgoal *1.2/5 Subgoal *1.2/4 Subgoal *1.2/3 Subgoal *1.2/3.2 Subgoal *1.2/3.2' Subgoal *1.2/3.2'' Subgoal *1.2/3.2''' Subgoal *1.2/3.2'4' Subgoal *1.2/3.2'5' Subgoal *1.2/3.2'6' Subgoal *1.2/3.2'7' *1.2.4 (Subgoal *1.2/3.2'7') is pushed for proof by induction. Subgoal *1.2/3.1 Subgoal *1.2/3.1' Subgoal *1.2/3.1'' Subgoal *1.2/3.1''' Subgoal *1.2/3.1'4' Subgoal *1.2/3.1'5' Subgoal *1.2/3.1'6' Subgoal *1.2/3.1'7' *1.2.5 (Subgoal *1.2/3.1'7') is pushed for proof by induction. Subgoal *1.2/2 Subgoal *1.2/1 Subgoal *1.2/1' Subgoal *1.2/1.2 Subgoal *1.2/1.2' Subgoal *1.2/1.2'' Subgoal *1.2/1.2''' *1.2.6 (Subgoal *1.2/1.2''') is pushed for proof by induction. Subgoal *1.2/1.1 Subgoal *1.2/1.1' *1.2.7 (Subgoal *1.2/1.1') is pushed for proof by induction. So we now return to *1.2.7, which is (IMPLIES (CONSP L) (TRUE-LISTP L)). Subgoal *1.2.7/2 Subgoal *1.2.7/1 Subgoal *1.2.7/1' Subgoal *1.2.7/1'' Subgoal *1.2.7/1''' Subgoal *1.2.7/1'4' *1.2.7.1 (Subgoal *1.2.7/1'4') is pushed for proof by induction. So we now return to *1.2.7.1, which is (IMPLIES (NOT (CONSP L2)) (NOT L2)). No induction schemes are suggested by *1.2.7.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ROTATE-LEN-GENERALIZATION ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DROPN) (:INDUCTION FIRSTN) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:REWRITE |(* a (/ a))|) (:REWRITE |(* y x)|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ x (- x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE |(+ y x)|) (:REWRITE |(< x (/ y)) with (< 0 y)|) (:REWRITE |(< y (+ (- c) x))|) (:REWRITE |(equal (+ (- c) x) y)|) (:REWRITE APP-ASSOC) (:REWRITE APP-X-NIL) (:REWRITE BUBBLE-DOWN-+-MATCH-1) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-LESS-THAN-2) (:REWRITE DROPN-APP) (:REWRITE FIRSTN-APP) (:REWRITE NORMALIZE-ADDENDS) (:REWRITE REDUCE-ADDITIVE-CONSTANT-<) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<) (:REWRITE SIMPLIFY-SUMS-<) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION FIRSTN) (:TYPE-PRESCRIPTION LEN)) Time: 0.30 seconds (prove: 0.29, print: 0.01, other: 0.00) Prover steps counted: 20143 --- 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' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *** Key checkpoints under a top-level induction *** *** (see :DOC pso to view induction schemes): *** Subgoal *1/4' (IMPLIES (AND (NOT (ZP N)) (< (+ 1 (LEN (APP (CDR X) (LIST (CAR X))))) N) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) ACL2 Error in ( DEFTHM ROTATE-LEN-GENERALIZATION ...): See :DOC failure. ******** FAILED ******** ACL2 >(defthm len-app (equal (len (app a b)) (+ (len a) (len b)))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM LEN-APP ...) Rules: ((:DEFINITION APP) (:DEFINITION LEN) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION LEN) (:REWRITE |(+ (+ x y) z)|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ y x)|) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION LEN)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 263 LEN-APP ACL2 >(defthm rotate-len-generalization (implies (and (true-listp x) (<= n (len x))) (equal (rotate n x) (app (dropn n x) (firstn n x))))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/5 Subgoal *1/5' Subgoal *1/4 Subgoal *1/4' Subgoal *1/4'' Subgoal *1/3 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 (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) *1.1 (Subgoal *1/2'5') is pushed for proof by induction. ]) Subgoal *1/1 So we now return to *1.1, which is (IMPLIES (AND (CONSP L) (NOT (TRUE-LISTP L)) (INTEGERP I) (<= 0 I) (NOT (ZP N)) (TRUE-LISTP X2) (<= N (+ 1 (LEN X2)))) (EQUAL (ROTATE I L) (APP (DROPN I X2) (CONS X1 (FIRSTN I X2))))). Subgoal *1.1/8 Subgoal *1.1/8.2 Subgoal *1.1/8.2' Subgoal *1.1/8.2'' Subgoal *1.1/8.2''' Subgoal *1.1/8.2'4' Subgoal *1.1/8.2'5' Subgoal *1.1/8.2'6' Subgoal *1.1/8.2'7' Subgoal *1.1/8.2'8' Subgoal *1.1/8.2'9' *1.1.1 (Subgoal *1.1/8.2'9') is pushed for proof by induction. Subgoal *1.1/8.1 Subgoal *1.1/8.1' Subgoal *1.1/8.1'' Subgoal *1.1/8.1''' Subgoal *1.1/8.1'4' Subgoal *1.1/8.1'5' Subgoal *1.1/8.1'6' Subgoal *1.1/8.1'7' Subgoal *1.1/8.1'8' *1.1.2 (Subgoal *1.1/8.1'8') is pushed for proof by induction. Subgoal *1.1/7 Subgoal *1.1/7' Subgoal *1.1/7'' Subgoal *1.1/7''' Subgoal *1.1/7'4' Subgoal *1.1/7'5' Subgoal *1.1/7'6' Subgoal *1.1/7'7' Subgoal *1.1/7'8' Subgoal *1.1/7'9' Subgoal *1.1/7'10' Subgoal *1.1/7'11' *1.1.3 (Subgoal *1.1/7'11') is pushed for proof by induction. Subgoal *1.1/6 Subgoal *1.1/5 Subgoal *1.1/4 Subgoal *1.1/3 Subgoal *1.1/3.2 Subgoal *1.1/3.2' Subgoal *1.1/3.2'' Subgoal *1.1/3.2''' Subgoal *1.1/3.2'4' Subgoal *1.1/3.2'5' Subgoal *1.1/3.2'6' Subgoal *1.1/3.2'7' *1.1.4 (Subgoal *1.1/3.2'7') is pushed for proof by induction. Subgoal *1.1/3.1 Subgoal *1.1/3.1' Subgoal *1.1/3.1'' Subgoal *1.1/3.1''' Subgoal *1.1/3.1'4' Subgoal *1.1/3.1'5' Subgoal *1.1/3.1'6' Subgoal *1.1/3.1'7' *1.1.5 (Subgoal *1.1/3.1'7') is pushed for proof by induction. Subgoal *1.1/2 Subgoal *1.1/1 Subgoal *1.1/1' Subgoal *1.1/1.2 Subgoal *1.1/1.2' Subgoal *1.1/1.2'' Subgoal *1.1/1.2''' *1.1.6 (Subgoal *1.1/1.2''') is pushed for proof by induction. Subgoal *1.1/1.1 Subgoal *1.1/1.1' *1.1.7 (Subgoal *1.1/1.1') is pushed for proof by induction. So we now return to *1.1.7, which is (IMPLIES (CONSP L) (TRUE-LISTP L)). Subgoal *1.1.7/2 Subgoal *1.1.7/1 Subgoal *1.1.7/1' Subgoal *1.1.7/1'' Subgoal *1.1.7/1''' Subgoal *1.1.7/1'4' *1.1.7.1 (Subgoal *1.1.7/1'4') is pushed for proof by induction. So we now return to *1.1.7.1, which is (IMPLIES (NOT (CONSP L2)) (NOT L2)). No induction schemes are suggested by *1.1.7.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ROTATE-LEN-GENERALIZATION ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART <) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART INTEGERP) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART TRUE-LISTP) (:EXECUTABLE-COUNTERPART UNARY--) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DROPN) (:INDUCTION FIRSTN) (:INDUCTION LEN) (:INDUCTION ROTATE) (:INDUCTION TRUE-LISTP) (:REWRITE |(* a (/ a))|) (:REWRITE |(* y x)|) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ x (- x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE |(+ y x)|) (:REWRITE |(< x (/ y)) with (< 0 y)|) (:REWRITE |(equal (+ (- c) x) y)|) (:REWRITE APP-ASSOC) (:REWRITE APP-X-NIL) (:REWRITE BUBBLE-DOWN-+-MATCH-1) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-LESS-THAN-2) (:REWRITE DROPN-APP) (:REWRITE FIRSTN-APP) (:REWRITE LEN-APP) (:REWRITE NORMALIZE-ADDENDS) (:REWRITE REDUCE-ADDITIVE-CONSTANT-<) (:REWRITE REMOVE-WEAK-INEQUALITIES) (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<) (:REWRITE SIMPLIFY-SUMS-<) (:TYPE-PRESCRIPTION APP) (:TYPE-PRESCRIPTION FIRSTN) (:TYPE-PRESCRIPTION LEN)) Time: 0.29 seconds (prove: 0.27, print: 0.01, other: 0.00) Prover steps counted: 18759 --- 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' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *** Key checkpoint under a top-level induction *** *** (see :DOC pso to view induction scheme): *** Subgoal *1/2' (IMPLIES (AND (NOT (ZP N)) (NOT (TRUE-LISTP (APP (CDR X) (LIST (CAR X))))) (CONSP X) (TRUE-LISTP (CDR X)) (<= N (+ 1 (LEN (CDR X))))) (EQUAL (ROTATE (+ -1 N) (APP (CDR X) (LIST (CAR X)))) (APP (DROPN (+ -1 N) (CDR X)) (CONS (CAR X) (FIRSTN (+ -1 N) (CDR X)))))) ACL2 Error in ( DEFTHM ROTATE-LEN-GENERALIZATION ...): See :DOC failure. ******** FAILED ******** ACL2 >(defthm true-listp-app (equal (true-listp (app x y)) (true-listp y))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. 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 TRUE-LISTP-APP ...) Rules: ((:DEFINITION APP) (:DEFINITION ENDP) (:DEFINITION NOT) (:DEFINITION TRUE-LISTP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:REWRITE CDR-CONS)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 257 TRUE-LISTP-APP ACL2 >(defthm rotate-len-generalization (implies (and (true-listp x) (<= n (len x))) (equal (rotate n x) (app (dropn n x) (firstn n x))))) Goal' ([ A key checkpoint: Goal' (IMPLIES (AND (TRUE-LISTP X) (ACL2-NUMBERP N) (<= N (LEN X))) (EQUAL (ROTATE N X) (APP (DROPN N X) (FIRSTN N X)))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/5 Subgoal *1/5' Subgoal *1/4 Subgoal *1/4' Subgoal *1/4'' Subgoal *1/3 Subgoal *1/2 Subgoal *1/2' Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal' is COMPLETED! Q.E.D. Summary Form: ( DEFTHM ROTATE-LEN-GENERALIZATION ...) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION ROTATE) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CDR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART LEN) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION DROPN) (:INDUCTION FIRSTN) (:INDUCTION ROTATE) (:REWRITE |(+ y x)|) (:REWRITE APP-ASSOC) (:REWRITE APP-X-NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE DEFAULT-LESS-THAN-2) (:REWRITE DROPN-APP) (:REWRITE FIRSTN-APP) (:REWRITE LEN-APP) (:REWRITE TRUE-LISTP-APP) (:TYPE-PRESCRIPTION LEN)) Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.00) Prover steps counted: 1745 ROTATE-LEN-GENERALIZATION ACL2 >(defthm rotate-len (implies (true-listp x) (equal (rotate (len x) x) x))) Goal' ([ A key checkpoint: Goal' (IMPLIES (TRUE-LISTP X) (EQUAL (APP (DROPN (LEN X) X) (FIRSTN (LEN X) X)) X)) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/3 Subgoal *1/2 Subgoal *1/2' Subgoal *1/2'' Subgoal *1/2''' Subgoal *1/2'4' Subgoal *1/2'5' Subgoal *1/2'6' Subgoal *1/2'7' Subgoal *1/2'8' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/2' (IMPLIES (AND (CONSP X) (EQUAL (APP (DROPN (LEN (CDR X)) (CDR X)) (FIRSTN (LEN (CDR X)) (CDR X))) (CDR X)) (TRUE-LISTP (CDR X))) (EQUAL (APP (DROPN (LEN (CDR X)) (CDR X)) (CONS (CAR X) (FIRSTN (LEN (CDR X)) (CDR X)))) X)) *1.1 (Subgoal *1/2'8') is pushed for proof by induction. ]) Subgoal *1/1 So we now return to *1.1, which is (IMPLIES (AND (TRUE-LISTP FN) (INTEGERP I) (<= 0 I)) (EQUAL (APP DN (CONS X1 FN)) (CONS X1 (APP DN FN)))). Subgoal *1.1/2 Subgoal *1.1/2' Subgoal *1.1/2.2 Subgoal *1.1/2.2' Subgoal *1.1/2.2'' *1.1.1 (Subgoal *1.1/2.2'') is pushed for proof by induction. Subgoal *1.1/2.1 Subgoal *1.1/2.1' Subgoal *1.1/2.1'' Subgoal *1.1/2.1''' Subgoal *1.1/2.1'4' Subgoal *1.1/2.1'5' *1.1.2 (Subgoal *1.1/2.1'5') is pushed for proof by induction. Subgoal *1.1/1 Subgoal *1.1/1' So we now return to *1.1.2, which is (IMPLIES (INTEGERP I) (< I 0)). No induction schemes are suggested by *1.1.2. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM ROTATE-LEN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION APP) (:DEFINITION DROPN) (:DEFINITION ENDP) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART APP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART LEN) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION APP) (:INDUCTION LEN) (:INDUCTION TRUE-LISTP) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE CONS-EQUAL) (:REWRITE ROTATE-LEN-GENERALIZATION) (:TYPE-PRESCRIPTION FIRSTN) (:TYPE-PRESCRIPTION LEN)) Time: 0.06 seconds (prove: 0.06, print: 0.00, other: 0.00) Prover steps counted: 4297 --- 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' (IMPLIES (TRUE-LISTP X) (EQUAL (APP (DROPN (LEN X) X) (FIRSTN (LEN X) X)) X)) *** Key checkpoint under a top-level induction *** *** (see :DOC pso to view induction scheme): *** Subgoal *1/2' (IMPLIES (AND (CONSP X) (EQUAL (APP (DROPN (LEN (CDR X)) (CDR X)) (FIRSTN (LEN (CDR X)) (CDR X))) (CDR X)) (TRUE-LISTP (CDR X))) (EQUAL (APP (DROPN (LEN (CDR X)) (CDR X)) (CONS (CAR X) (FIRSTN (LEN (CDR X)) (CDR X)))) X)) ACL2 Error in ( DEFTHM ROTATE-LEN ...): See :DOC failure. ******** FAILED ******** ACL2 >(defthm dropn-len (equal (dropn (len x) x) nil)) Goal' ([ A key checkpoint: Goal' (NOT (DROPN (LEN X) X)) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/2 Subgoal *1/2' ([ A key checkpoint while proving *1 (descended from Goal'): Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (NOT X)) *1.1 (Subgoal *1/2') is pushed for proof by induction. ]) Subgoal *1/1 So we now return to *1.1, which is (IMPLIES (NOT (CONSP X)) (NOT X)). No induction schemes are suggested by *1.1. Consequently, the proof attempt has failed. Summary Form: ( DEFTHM DROPN-LEN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION DROPN) (:DEFINITION LEN) (:DEFINITION NOT) (:DEFINITION SYNP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART ZP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION LEN) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ y (+ x z))|) (:TYPE-PRESCRIPTION LEN)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 229 --- 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' (NOT (DROPN (LEN X) X)) *** Key checkpoint under a top-level induction *** *** (see :DOC pso to view induction scheme): *** Subgoal *1/2' (IMPLIES (NOT (CONSP X)) (NOT X)) ACL2 Error in ( DEFTHM DROPN-LEN ...): See :DOC failure. ******** FAILED ******** ACL2 >(defthm dropn-len (implies (true-listp x) (equal (dropn (len x) x) nil))) Goal' ([ A key checkpoint: Goal' (IMPLIES (TRUE-LISTP X) (NOT (DROPN (LEN X) X))) *1 (Goal') is pushed for proof by induction. ]) Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal' is COMPLETED! Q.E.D. Summary Form: ( DEFTHM DROPN-LEN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION DROPN) (:DEFINITION LEN) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART DROPN) (:EXECUTABLE-COUNTERPART LEN) (:EXECUTABLE-COUNTERPART NOT) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION LEN) (:INDUCTION TRUE-LISTP) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ y (+ x z))|) (:TYPE-PRESCRIPTION LEN)) Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 310 DROPN-LEN ACL2 >(defthm firstn-len (implies (true-listp x) (equal (firstn (len x) x) x))) *1 (the initial Goal, a key checkpoint) is pushed for proof by induction. Subgoal *1/3 Subgoal *1/2 Subgoal *1/1 *1 is COMPLETED! Thus key checkpoint Goal is COMPLETED! Q.E.D. Summary Form: ( DEFTHM FIRSTN-LEN ...) Rules: ((:COMPOUND-RECOGNIZER ZP-COMPOUND-RECOGNIZER) (:DEFINITION FIRSTN) (:DEFINITION LEN) (:DEFINITION SYNP) (:DEFINITION TRUE-LISTP) (:EXECUTABLE-COUNTERPART BINARY-+) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART FIRSTN) (:EXECUTABLE-COUNTERPART LEN) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION LEN) (:INDUCTION TRUE-LISTP) (:REWRITE |(+ 0 x)|) (:REWRITE |(+ c (+ d x))|) (:REWRITE |(+ y (+ x z))|) (:REWRITE CONS-CAR-CDR) (:TYPE-PRESCRIPTION LEN)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 261 FIRSTN-LEN ACL2 >(defthm rotate-len (implies (true-listp x) (equal (rotate (len x) x) x))) Q.E.D. Summary Form: ( DEFTHM ROTATE-LEN ...) Rules: ((:DEFINITION APP) (:EXECUTABLE-COUNTERPART CONSP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE DROPN-LEN) (:REWRITE FIRSTN-LEN) (:REWRITE ROTATE-LEN-GENERALIZATION) (:TYPE-PRESCRIPTION LEN)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) Prover steps counted: 81 ROTATE-LEN ACL2 >