This is SBCL 1.0.29.11.debian, an implementation of ANSI Common Lisp. More information about SBCL is available at . SBCL is free software, provided as is, with absolutely no warranty. It is mostly in the public domain; some portions are provided under BSD-style licenses. See the CREDITS and COPYING files in the distribution for more information. ACL2 Version 3.6 built February 12, 2010 14:59:57. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 3.6. Level 1. Cbd "/home/petersk/workspace/benchmark/". Distributed books directory "/home/petersk/download/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> :ALL ACL2 !> Since TRS_ISBOOL is non-recursive, its admission is trivial. We observe that the type of TRS_ISBOOL is described by the theorem (OR (EQUAL (TRS_ISBOOL X) T) (EQUAL (TRS_ISBOOL X) NIL)). We used the :executable-counterpart of EQUAL and primitive type reasoning. Summary Form: ( DEFUN TRS_ISBOOL ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) TRS_ISBOOL ACL2 !> For the admission of TRS_ISSORT[A0] we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (NOT (AND (CONSP X) (EQ 'TRS_0 (CAR X)) (EQ (CDR X) NIL))) (CONSP X) (CONSP (CDR X)) (EQ 'TRS_S (CAR X))) (O< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (NOT (AND (CONSP X) (EQUAL 'TRS_0 (CAR X)) (EQUAL (CDR X) NIL))) (CONSP X) (CONSP (CDR X)) (EQUAL 'TRS_S (CAR X))) (O< (ACL2-COUNT (CADR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP and O<, the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (EQUAL 'TRS_S (CAR X))) (< (ACL2-COUNT (CADR X)) (+ 1 (ACL2-COUNT (CDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2 and restrict the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. These steps produce the following goal. Goal''' (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) (NOT (EQUAL X1 NIL)) (CONSP (LIST* X1 X3 X4)) (EQUAL 'TRS_S X1)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). By case analysis we reduce the conjecture to Goal'4' (IMPLIES (AND (CONSP (CONS X3 X4)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X4)) (EQUAL 'TRS_S X1)) (< (ACL2-COUNT X3) (+ 1 (ACL2-COUNT (CONS X3 X4))))). This simplifies, using the :definition ACL2-COUNT, the :executable- counterparts of EQUAL, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Goal'5' (< (ACL2-COUNT X3) (+ 1 1 (ACL2-COUNT X3) (ACL2-COUNT X4))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_ISSORT[A0]. Thus, we admit this function under the principle of definition. We observe that the type of TRS_ISSORT[A0] is described by the theorem (OR (EQUAL (TRS_ISSORT[A0] X) T) (EQUAL (TRS_ISSORT[A0] X) NIL)). We used the :executable-counterpart of EQUAL and primitive type reasoning. Summary Form: ( DEFUN TRS_ISSORT[A0] ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART SYMBOLP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) TRS_ISSORT[A0] ACL2 !> Since TRS_ISSORT[A61] is non-recursive, its admission is trivial. We observe that the type of TRS_ISSORT[A61] is described by the theorem (OR (EQUAL (TRS_ISSORT[A61] X) T) (EQUAL (TRS_ISSORT[A61] X) NIL)). We used primitive type reasoning. Summary Form: ( DEFUN TRS_ISSORT[A61] ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) TRS_ISSORT[A61] ACL2 !> For the admission of TRS_ISSORT[A32] we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (NOT (AND (CONSP X) (EQ 'TRS_NIL (CAR X)) (EQ (CDR X) NIL))) (CONSP X) (CONSP (CDR X)) (CONSP (CDDR X)) (EQ 'TRS_CONS (CAR X)) (TRS_ISSORT[A0] (CADR X))) (O< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (NOT (AND (CONSP X) (EQUAL 'TRS_NIL (CAR X)) (EQUAL (CDR X) NIL))) (CONSP X) (CONSP (CDR X)) (CONSP (CDDR X)) (EQUAL 'TRS_CONS (CAR X)) (TRS_ISSORT[A0] (CADR X))) (O< (ACL2-COUNT (CADDR X)) (ACL2-COUNT X))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP and O<, the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal'' (IMPLIES (AND (CONSP X) (CONSP (CDR X)) (CONSP (CDDR X)) (EQUAL 'TRS_CONS (CAR X)) (TRS_ISSORT[A0] (CADR X))) (< (ACL2-COUNT (CADDR X)) (+ 1 1 (ACL2-COUNT (CADR X)) (ACL2-COUNT (CDDR X))))). The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore, those terms are at the root of a chain of three rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X) by X1 and (CDR X) by X2 and restrict the type of the new variable X1 to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. (3) Finally, use CAR-CDR-ELIM to replace X4 by (CONS X5 X6), (CAR X4) by X5 and (CDR X4) by X6. These steps produce the following goal. Goal''' (IMPLIES (AND (CONSP (CONS X5 X6)) (CONSP (LIST* X3 X5 X6)) (SYMBOLP X1) (NOT (EQUAL X1 T)) (NOT (EQUAL X1 NIL)) (CONSP (LIST* X1 X3 X5 X6)) (EQUAL 'TRS_CONS X1) (TRS_ISSORT[A0] X3)) (< (ACL2-COUNT X5) (+ 1 1 (ACL2-COUNT X3) (ACL2-COUNT (CONS X5 X6))))). By case analysis we reduce the conjecture to Goal'4' (IMPLIES (AND (CONSP (CONS X5 X6)) (CONSP (LIST* X3 X5 X6)) (SYMBOLP X1) (NOT (EQUAL X1 T)) X1 (CONSP (LIST* X1 X3 X5 X6)) (EQUAL 'TRS_CONS X1) (TRS_ISSORT[A0] X3)) (< (ACL2-COUNT X5) (+ 1 1 (ACL2-COUNT X3) (ACL2-COUNT (CONS X5 X6))))). This simplifies, using the :definition ACL2-COUNT, the :executable- counterparts of EQUAL, NOT and SYMBOLP, primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS, to Goal'5' (IMPLIES (TRS_ISSORT[A0] X3) (< (ACL2-COUNT X5) (+ 1 1 (ACL2-COUNT X3) 1 (ACL2-COUNT X5) (ACL2-COUNT X6)))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_ISSORT[A32]. Thus, we admit this function under the principle of definition. We observe that the type of TRS_ISSORT[A32] is described by the theorem (OR (EQUAL (TRS_ISSORT[A32] X) T) (EQUAL (TRS_ISSORT[A32] X) NIL)). We used the :executable-counterpart of EQUAL and primitive type reasoning. Summary Form: ( DEFUN TRS_ISSORT[A32] ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART SYMBOLP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) TRS_ISSORT[A32] ACL2 !> For the admission of TRS_LE we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X0). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A0] X1)) (NOT (EQ (CAR X0) 'TRS_0)) (NOT (AND (EQ (CAR X0) 'TRS_S) (EQ (CAR X1) 'TRS_0))) T) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A0] X1) (NOT (EQUAL (CAR X0) 'TRS_0)) (NOT (AND (EQUAL (CAR X0) 'TRS_S) (EQUAL (CAR X1) 'TRS_0)))) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A0], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal'' (IMPLIES (AND (CONSP X0) (CONSP (CDR X0)) (EQUAL 'TRS_S (CAR X0)) (TRS_ISSORT[A0] (CADR X0)) (NOT (CDDR X0)) (TRS_ISSORT[A0] X1) (NOT (EQUAL (CAR X1) 'TRS_0))) (< (ACL2-COUNT (CADR X0)) (+ 1 1 (ACL2-COUNT (CADR X0))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_LE. Thus, we admit this function under the principle of definition. We observe that the type of TRS_LE is described by the theorem (AND (CONSP (TRS_LE X0 X1)) (TRUE-LISTP (TRS_LE X0 X1))). Summary Form: ( DEFUN TRS_LE ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_ISSORT[A0]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) TRS_LE ACL2 !> For the admission of TRS_EQ we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X0). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A0] X1)) (NOT (AND (EQ (CAR X0) 'TRS_0) (EQ (CAR X1) 'TRS_0))) (NOT (AND (EQ (CAR X0) 'TRS_0) (EQ (CAR X1) 'TRS_S))) (NOT (AND (EQ (CAR X0) 'TRS_S) (EQ (CAR X1) 'TRS_0))) T) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A0] X1) (NOT (AND (EQUAL (CAR X0) 'TRS_0) (EQUAL (CAR X1) 'TRS_0))) (NOT (AND (EQUAL (CAR X0) 'TRS_0) (EQUAL (CAR X1) 'TRS_S))) (NOT (AND (EQUAL (CAR X0) 'TRS_S) (EQUAL (CAR X1) 'TRS_0)))) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A0], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal'' (IMPLIES (AND (CONSP X0) (CONSP (CDR X0)) (EQUAL 'TRS_S (CAR X0)) (TRS_ISSORT[A0] (CADR X0)) (NOT (CDDR X0)) (TRS_ISSORT[A0] X1) (NOT (EQUAL (CAR X1) 'TRS_0))) (< (ACL2-COUNT (CADR X0)) (+ 1 1 (ACL2-COUNT (CADR X0))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_EQ. Thus, we admit this function under the principle of definition. We observe that the type of TRS_EQ is described by the theorem (AND (CONSP (TRS_EQ X0 X1)) (TRUE-LISTP (TRS_EQ X0 X1))). We used the :executable-counterpart of EQUAL and primitive type reasoning. Summary Form: ( DEFUN TRS_EQ ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_ISSORT[A0]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.01) TRS_EQ ACL2 !> Since TRS_EQUAL_SORT[A61] is non-recursive, its admission is trivial. We observe that the type of TRS_EQUAL_SORT[A61] is described by the theorem (AND (CONSP (TRS_EQUAL_SORT[A61] X0 X1)) (TRUE-LISTP (TRS_EQUAL_SORT[A61] X0 X1))). Summary Form: ( DEFUN TRS_EQUAL_SORT[A61] ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) TRS_EQUAL_SORT[A61] ACL2 !> For the admission of TRS_EQUAL_SORT[A0] we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X0). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A0] X1)) (NOT (AND (EQ (CAR X0) 'TRS_0) (EQ (CAR X1) 'TRS_0))) (NOT (AND (EQ (CAR X0) 'TRS_0) (EQ (CAR X1) 'TRS_S))) (NOT (AND (EQ (CAR X0) 'TRS_S) (EQ (CAR X1) 'TRS_0))) T) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A0] X1) (NOT (AND (EQUAL (CAR X0) 'TRS_0) (EQUAL (CAR X1) 'TRS_0))) (NOT (AND (EQUAL (CAR X0) 'TRS_0) (EQUAL (CAR X1) 'TRS_S))) (NOT (AND (EQUAL (CAR X0) 'TRS_S) (EQUAL (CAR X1) 'TRS_0)))) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A0], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal'' (IMPLIES (AND (CONSP X0) (CONSP (CDR X0)) (EQUAL 'TRS_S (CAR X0)) (TRS_ISSORT[A0] (CADR X0)) (NOT (CDDR X0)) (TRS_ISSORT[A0] X1) (NOT (EQUAL (CAR X1) 'TRS_0))) (< (ACL2-COUNT (CADR X0)) (+ 1 1 (ACL2-COUNT (CADR X0))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_EQUAL_SORT[A0]. Thus, we admit this function under the principle of definition. We observe that the type of TRS_EQUAL_SORT[A0] is described by the theorem (AND (CONSP (TRS_EQUAL_SORT[A0] X0 X1)) (TRUE-LISTP (TRS_EQUAL_SORT[A0] X0 X1))). We used the :executable-counterpart of EQUAL and primitive type reasoning. Summary Form: ( DEFUN TRS_EQUAL_SORT[A0] ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_ISSORT[A0]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) TRS_EQUAL_SORT[A0] ACL2 !> Since TRS_ISA_FALSE is non-recursive, its admission is trivial. We observe that the type of TRS_ISA_FALSE is described by the theorem (AND (CONSP (TRS_ISA_FALSE X0)) (TRUE-LISTP (TRS_ISA_FALSE X0))). Summary Form: ( DEFUN TRS_ISA_FALSE ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) TRS_ISA_FALSE ACL2 !> Since TRS_ISA_TRUE is non-recursive, its admission is trivial. We observe that the type of TRS_ISA_TRUE is described by the theorem (AND (CONSP (TRS_ISA_TRUE X0)) (TRUE-LISTP (TRS_ISA_TRUE X0))). Summary Form: ( DEFUN TRS_ISA_TRUE ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) TRS_ISA_TRUE ACL2 !> Since TRS_NOT is non-recursive, its admission is trivial. We observe that the type of TRS_NOT is described by the theorem (AND (CONSP (TRS_NOT X0)) (TRUE-LISTP (TRS_NOT X0))). Summary Form: ( DEFUN TRS_NOT ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) TRS_NOT ACL2 !> Since TRS_OR is non-recursive, its admission is trivial. We observe that the type of TRS_OR is described by the theorem (OR (AND (CONSP (TRS_OR X0 X1)) (TRUE-LISTP (TRS_OR X0 X1))) (EQUAL (TRS_OR X0 X1) X1)). Summary Form: ( DEFUN TRS_OR ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) TRS_OR ACL2 !> Since TRS_AND is non-recursive, its admission is trivial. We observe that the type of TRS_AND is described by the theorem (OR (AND (CONSP (TRS_AND X0 X1)) (TRUE-LISTP (TRS_AND X0 X1))) (EQUAL (TRS_AND X0 X1) X1)). Summary Form: ( DEFUN TRS_AND ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) TRS_AND ACL2 !> Since TRS_EQUAL_BOOL is non-recursive, its admission is trivial. We observe that the type of TRS_EQUAL_BOOL is described by the theorem (AND (CONSP (TRS_EQUAL_BOOL X0 X1)) (TRUE-LISTP (TRS_EQUAL_BOOL X0 X1))). We used the :executable-counterpart of EQUAL and primitive type reasoning. Summary Form: ( DEFUN TRS_EQUAL_BOOL ...) Rules: ((:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) TRS_EQUAL_BOOL ACL2 !> For the admission of TRS_IF1 we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X3). The non-trivial part of the measure conjecture is Goal (AND (IMPLIES (AND (AND (TRS_ISBOOL X0) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3)) (NOT (AND (EQ (CAR X0) 'TRS_TRUE) (EQ (CAR X3) 'TRS_NIL))) (AND (EQ (CAR X0) 'TRS_TRUE) (EQ (CAR X3) 'TRS_CONS))) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3))) (IMPLIES (AND (AND (TRS_ISBOOL X0) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3)) (NOT (AND (EQ (CAR X0) 'TRS_TRUE) (EQ (CAR X3) 'TRS_NIL))) (NOT (AND (EQ (CAR X0) 'TRS_FALSE) (EQ (CAR X3) 'TRS_NIL))) T) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3)))). By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture to the following two conjectures. Subgoal 2 (IMPLIES (AND (CONSP X0) (COND ((EQUAL 'TRS_TRUE (CAR X0)) (EQUAL (CDR X0) NIL)) ((EQUAL 'TRS_FALSE (CAR X0)) (EQUAL (CDR X0) NIL)) (T NIL)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3) (NOT (AND (EQUAL (CAR X0) 'TRS_TRUE) (EQUAL (CAR X3) 'TRS_NIL))) (EQUAL (CAR X0) 'TRS_TRUE) (EQUAL (CAR X3) 'TRS_CONS)) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 2' (IMPLIES (AND (CONSP X0) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3)) (EQUAL (CAR X0) 'TRS_TRUE) (EQUAL (CAR X3) 'TRS_CONS)) (< (ACL2-COUNT (CADDR X3)) (+ 1 (ACL2-COUNT (CDR X3))))). This simplifies, using the :definitions ACL2-COUNT and FIX, the :executable- counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 2'' (IMPLIES (AND (CONSP X0) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3)) (EQUAL (CAR X0) 'TRS_TRUE) (EQUAL (CAR X3) 'TRS_CONS)) (< (ACL2-COUNT (CADDR X3)) (+ 1 1 (ACL2-COUNT (CADR X3)) 1 (ACL2-COUNT (CADDR X3))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1 (IMPLIES (AND (CONSP X0) (COND ((EQUAL 'TRS_TRUE (CAR X0)) (EQUAL (CDR X0) NIL)) ((EQUAL 'TRS_FALSE (CAR X0)) (EQUAL (CDR X0) NIL)) (T NIL)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3) (NOT (AND (EQUAL (CAR X0) 'TRS_TRUE) (EQUAL (CAR X3) 'TRS_NIL))) (NOT (AND (EQUAL (CAR X0) 'TRS_FALSE) (EQUAL (CAR X3) 'TRS_NIL)))) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to the following two conjectures. Subgoal 1.2 (IMPLIES (AND (CONSP X0) (EQUAL 'TRS_TRUE (CAR X0)) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (EQUAL 'TRS_CONS (CAR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3))) (< (ACL2-COUNT (CADDR X3)) (+ 1 (ACL2-COUNT (CDR X3))))). This simplifies, using the :definitions ACL2-COUNT and FIX, the :executable- counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 1.2' (IMPLIES (AND (CONSP X0) (EQUAL 'TRS_TRUE (CAR X0)) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (EQUAL 'TRS_CONS (CAR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3))) (< (ACL2-COUNT (CADDR X3)) (+ 1 1 (ACL2-COUNT (CADR X3)) 1 (ACL2-COUNT (CADDR X3))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1.1 (IMPLIES (AND (CONSP X0) (EQUAL 'TRS_FALSE (CAR X0)) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (EQUAL 'TRS_CONS (CAR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3))) (< (ACL2-COUNT (CADDR X3)) (+ 1 (ACL2-COUNT (CDR X3))))). This simplifies, using the :definitions ACL2-COUNT and FIX, the :executable- counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 1.1' (IMPLIES (AND (CONSP X0) (EQUAL 'TRS_FALSE (CAR X0)) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (EQUAL 'TRS_CONS (CAR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3))) (< (ACL2-COUNT (CADDR X3)) (+ 1 1 (ACL2-COUNT (CADR X3)) 1 (ACL2-COUNT (CADDR X3))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_IF1. Thus, we admit this function under the principle of definition. We could deduce no constraints on the type of TRS_IF1. However, in normalizing the definition we used the :executable-counterpart of EQUAL and primitive type reasoning. Summary Form: ( DEFUN TRS_IF1 ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_ISBOOL) (:DEFINITION TRS_ISSORT[A32]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.04 seconds (prove: 0.02, print: 0.01, other: 0.01) TRS_IF1 ACL2 !> For the admission of TRS_MIN we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X1). The non-trivial part of the measure conjecture is Goal (AND (IMPLIES (AND (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1)) (NOT (EQ (CAR X1) 'TRS_NIL)) (EQ (TRS_EQUAL_BOOL (TRS_LE X0 (CADR X1)) '(TRS_TRUE)) '(TRS_FALSE))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1))) (IMPLIES (AND (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1)) (NOT (EQ (CAR X1) 'TRS_NIL)) (AND (EQ (CAR X1) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE X0 (CADR X1)) '(TRS_TRUE)) '(TRS_TRUE)))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1)))). By the simple :definition EQ we reduce the conjecture to the following two conjectures. Subgoal 2 (IMPLIES (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (EQUAL (TRS_EQUAL_BOOL (TRS_LE X0 (CADR X1)) '(TRS_TRUE)) '(TRS_FALSE))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<, TRS_EQUAL_BOOL, TRS_ISBOOL and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT, CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type- prescription rules ACL2-COUNT and TRS_LE, to Subgoal 2' (IMPLIES (AND (TRS_ISSORT[A0] X0) (CONSP X1) (CONSP (CDR X1)) (CONSP (CDDR X1)) (EQUAL 'TRS_CONS (CAR X1)) (TRS_ISSORT[A0] (CADR X1)) (TRS_ISSORT[A32] (CADDR X1)) (NOT (CDDDR X1)) (EQUAL 'TRS_FALSE (CAR (TRS_LE X0 (CADR X1)))) (NOT (CDR (TRS_LE X0 (CADR X1))))) (< (ACL2-COUNT (CADDR X1)) (+ 1 1 (ACL2-COUNT (CADR X1)) 1 (ACL2-COUNT (CADDR X1))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1 (IMPLIES (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (EQUAL (CAR X1) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE X0 (CADR X1)) '(TRS_TRUE)) '(TRS_TRUE))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<, TRS_EQUAL_BOOL, TRS_ISBOOL and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT, CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type- prescription rules ACL2-COUNT and TRS_LE, to the following three conjectures. Subgoal 1.3 (IMPLIES (AND (TRS_ISSORT[A0] X0) (CONSP X1) (CONSP (CDR X1)) (CONSP (CDDR X1)) (TRS_ISSORT[A0] (CADR X1)) (TRS_ISSORT[A32] (CADDR X1)) (NOT (CDDDR X1)) (EQUAL (CAR X1) 'TRS_CONS) (EQUAL 'TRS_TRUE (CAR (TRS_LE X0 (CADR X1))))) (< (ACL2-COUNT (CADDR X1)) (+ 1 1 (ACL2-COUNT (CADR X1)) 1 (ACL2-COUNT (CADDR X1))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1.2 (IMPLIES (AND (TRS_ISSORT[A0] X0) (CONSP X1) (CONSP (CDR X1)) (CONSP (CDDR X1)) (TRS_ISSORT[A0] (CADR X1)) (TRS_ISSORT[A32] (CADDR X1)) (NOT (CDDDR X1)) (EQUAL (CAR X1) 'TRS_CONS) (CDR (TRS_LE X0 (CADR X1)))) (< (ACL2-COUNT (CADDR X1)) (+ 1 1 (ACL2-COUNT (CADR X1)) 1 (ACL2-COUNT (CADDR X1))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1.1 (IMPLIES (AND (TRS_ISSORT[A0] X0) (CONSP X1) (CONSP (CDR X1)) (CONSP (CDDR X1)) (TRS_ISSORT[A0] (CADR X1)) (TRS_ISSORT[A32] (CADDR X1)) (NOT (CDDDR X1)) (EQUAL (CAR X1) 'TRS_CONS) (NOT (EQUAL 'TRS_FALSE (CAR (TRS_LE X0 (CADR X1)))))) (< (ACL2-COUNT (CADDR X1)) (+ 1 1 (ACL2-COUNT (CADR X1)) 1 (ACL2-COUNT (CADDR X1))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_MIN. Thus, we admit this function under the principle of definition. We could deduce no constraints on the type of TRS_MIN. Summary Form: ( DEFUN TRS_MIN ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_EQUAL_BOOL) (:DEFINITION TRS_ISBOOL) (:DEFINITION TRS_ISSORT[A32]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART TRS_ISBOOL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION TRS_LE)) Warnings: None Time: 0.03 seconds (prove: 0.02, print: 0.00, other: 0.01) TRS_MIN ACL2 !> For the admission of TRS_IF2 we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X3). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (AND (TRS_ISBOOL X0) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3)) (NOT (EQ (CAR X0) 'TRS_TRUE)) (AND (EQ (CAR X0) 'TRS_FALSE) (EQ (CAR X3) 'TRS_CONS))) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3))). By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture to Goal' (IMPLIES (AND (CONSP X0) (COND ((EQUAL 'TRS_TRUE (CAR X0)) (EQUAL (CDR X0) NIL)) ((EQUAL 'TRS_FALSE (CAR X0)) (EQUAL (CDR X0) NIL)) (T NIL)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3) (NOT (EQUAL (CAR X0) 'TRS_TRUE)) (EQUAL (CAR X0) 'TRS_FALSE) (EQUAL (CAR X3) 'TRS_CONS)) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal'' (IMPLIES (AND (CONSP X0) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3)) (EQUAL (CAR X0) 'TRS_FALSE) (EQUAL (CAR X3) 'TRS_CONS)) (< (ACL2-COUNT (CADDR X3)) (+ 1 (ACL2-COUNT (CDR X3))))). This simplifies, using the :definitions ACL2-COUNT and FIX, the :executable- counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal''' (IMPLIES (AND (CONSP X0) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3)) (EQUAL (CAR X0) 'TRS_FALSE) (EQUAL (CAR X3) 'TRS_CONS)) (< (ACL2-COUNT (CADDR X3)) (+ 1 1 (ACL2-COUNT (CADR X3)) 1 (ACL2-COUNT (CADDR X3))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_IF2. Thus, we admit this function under the principle of definition. We observe that the type of TRS_IF2 is described by the theorem (OR (AND (CONSP (TRS_IF2 X0 X1 X2 X3)) (TRUE-LISTP (TRS_IF2 X0 X1 X2 X3))) (EQUAL (TRS_IF2 X0 X1 X2 X3) X3)). We used primitive type reasoning. Summary Form: ( DEFUN TRS_IF2 ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_ISBOOL) (:DEFINITION TRS_ISSORT[A32]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) TRS_IF2 ACL2 !> For the admission of TRS_IF2PRIME we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X3). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (AND (TRS_ISBOOL X0) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3)) (NOT (EQ (CAR X0) 'TRS_TRUE)) (AND (EQ (CAR X0) 'TRS_FALSE) (EQ (CAR X3) 'TRS_CONS))) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3))). By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture to Goal' (IMPLIES (AND (CONSP X0) (COND ((EQUAL 'TRS_TRUE (CAR X0)) (EQUAL (CDR X0) NIL)) ((EQUAL 'TRS_FALSE (CAR X0)) (EQUAL (CDR X0) NIL)) (T NIL)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (TRS_ISSORT[A32] X3) (NOT (EQUAL (CAR X0) 'TRS_TRUE)) (EQUAL (CAR X0) 'TRS_FALSE) (EQUAL (CAR X3) 'TRS_CONS)) (O< (ACL2-COUNT (CADDR X3)) (ACL2-COUNT X3))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal'' (IMPLIES (AND (CONSP X0) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3)) (EQUAL (CAR X0) 'TRS_FALSE) (EQUAL (CAR X3) 'TRS_CONS)) (< (ACL2-COUNT (CADDR X3)) (+ 1 (ACL2-COUNT (CDR X3))))). This simplifies, using the :definitions ACL2-COUNT and FIX, the :executable- counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Goal''' (IMPLIES (AND (CONSP X0) (NOT (CDR X0)) (TRS_ISSORT[A0] X1) (TRS_ISSORT[A0] X2) (CONSP X3) (CONSP (CDR X3)) (CONSP (CDDR X3)) (TRS_ISSORT[A0] (CADR X3)) (TRS_ISSORT[A32] (CADDR X3)) (NOT (CDDDR X3)) (EQUAL (CAR X0) 'TRS_FALSE) (EQUAL (CAR X3) 'TRS_CONS)) (< (ACL2-COUNT (CADDR X3)) (+ 1 1 (ACL2-COUNT (CADR X3)) 1 (ACL2-COUNT (CADDR X3))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_IF2PRIME. Thus, we admit this function under the principle of definition. We observe that the type of TRS_IF2PRIME is described by the theorem (AND (CONSP (TRS_IF2PRIME X0 X1 X2 X3)) (TRUE-LISTP (TRS_IF2PRIME X0 X1 X2 X3))). Summary Form: ( DEFUN TRS_IF2PRIME ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_ISBOOL) (:DEFINITION TRS_ISSORT[A32]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT)) Warnings: None Time: 0.02 seconds (prove: 0.00, print: 0.01, other: 0.01) TRS_IF2PRIME ACL2 !> For the admission of TRS_DEL we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X1). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1)) (NOT (EQ (CAR X1) 'TRS_NIL)) (NOT (AND (EQ (CAR X1) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_FALSE))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1))). By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (NOT (AND (EQUAL (CAR X1) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_FALSE))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<, TRS_EQUAL_BOOL, TRS_ISBOOL and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT, CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type- prescription rules ACL2-COUNT and TRS_EQ, to Goal'' (IMPLIES (AND (TRS_ISSORT[A0] X0) (CONSP X1) (CONSP (CDR X1)) (CONSP (CDDR X1)) (EQUAL 'TRS_CONS (CAR X1)) (TRS_ISSORT[A0] (CADR X1)) (TRS_ISSORT[A32] (CADDR X1)) (NOT (CDDDR X1)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ X0 (CADR X1)))) (NOT (CDR (TRS_EQ X0 (CADR X1))))) (< (ACL2-COUNT (CADDR X1)) (+ 1 1 (ACL2-COUNT (CADR X1)) 1 (ACL2-COUNT (CADDR X1))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_DEL. Thus, we admit this function under the principle of definition. We could deduce no constraints on the type of TRS_DEL. Summary Form: ( DEFUN TRS_DEL ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_EQUAL_BOOL) (:DEFINITION TRS_ISBOOL) (:DEFINITION TRS_ISSORT[A32]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART TRS_ISBOOL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION TRS_EQ)) Warnings: None Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00) TRS_DEL ACL2 !> For the admission of TRS_DELPRIME we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X1). The non-trivial part of the measure conjecture is Goal (IMPLIES (AND (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1)) (NOT (EQ (CAR X1) 'TRS_NIL)) (NOT (AND (EQ (CAR X1) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_FALSE))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1))). By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (TRS_ISSORT[A0] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (NOT (AND (EQUAL (CAR X1) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_EQ X0 (CADR X1)) '(TRS_TRUE)) '(TRS_FALSE))) (O< (ACL2-COUNT (CADDR X1)) (ACL2-COUNT X1))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<, TRS_EQUAL_BOOL, TRS_ISBOOL and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT, CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type- prescription rules ACL2-COUNT and TRS_EQ, to Goal'' (IMPLIES (AND (TRS_ISSORT[A0] X0) (CONSP X1) (CONSP (CDR X1)) (CONSP (CDDR X1)) (EQUAL 'TRS_CONS (CAR X1)) (TRS_ISSORT[A0] (CADR X1)) (TRS_ISSORT[A32] (CADDR X1)) (NOT (CDDDR X1)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ X0 (CADR X1)))) (NOT (CDR (TRS_EQ X0 (CADR X1))))) (< (ACL2-COUNT (CADDR X1)) (+ 1 1 (ACL2-COUNT (CADR X1)) 1 (ACL2-COUNT (CADDR X1))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Q.E.D. That completes the proof of the measure theorem for TRS_DELPRIME. Thus, we admit this function under the principle of definition. We observe that the type of TRS_DELPRIME is described by the theorem (AND (CONSP (TRS_DELPRIME X0 X1)) (TRUE-LISTP (TRS_DELPRIME X0 X1))). Summary Form: ( DEFUN TRS_DELPRIME ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_EQUAL_BOOL) (:DEFINITION TRS_ISBOOL) (:DEFINITION TRS_ISSORT[A32]) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART TRS_ISBOOL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION TRS_EQ)) Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) TRS_DELPRIME ACL2 !> For the admission of TRS_EQUAL_SORT[A32] we will use the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X0). The non-trivial part of the measure conjecture is Goal (AND (IMPLIES (AND (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1)) (NOT (AND (EQ (CAR X0) 'TRS_NIL) (EQ (CAR X1) 'TRS_NIL))) (NOT (AND (EQ (CAR X0) 'TRS_NIL) (EQ (CAR X1) 'TRS_CONS))) (NOT (AND (EQ (CAR X0) 'TRS_CONS) (EQ (CAR X1) 'TRS_NIL))) T) (O< (ACL2-COUNT (CADDR X0)) (ACL2-COUNT X0))) (IMPLIES (AND (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1)) (NOT (AND (EQ (CAR X0) 'TRS_NIL) (EQ (CAR X1) 'TRS_NIL))) (NOT (AND (EQ (CAR X0) 'TRS_NIL) (EQ (CAR X1) 'TRS_CONS))) (NOT (AND (EQ (CAR X0) 'TRS_CONS) (EQ (CAR X1) 'TRS_NIL))) T) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0)))). By the simple :definition EQ we reduce the conjecture to the following two conjectures. Subgoal 2 (IMPLIES (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (AND (EQUAL (CAR X0) 'TRS_NIL) (EQUAL (CAR X1) 'TRS_NIL))) (NOT (AND (EQUAL (CAR X0) 'TRS_NIL) (EQUAL (CAR X1) 'TRS_CONS))) (NOT (AND (EQUAL (CAR X0) 'TRS_CONS) (EQUAL (CAR X1) 'TRS_NIL)))) (O< (ACL2-COUNT (CADDR X0)) (ACL2-COUNT X0))). This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O< and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 2' (IMPLIES (AND (CONSP X0) (CONSP (CDR X0)) (CONSP (CDDR X0)) (EQUAL 'TRS_CONS (CAR X0)) (TRS_ISSORT[A0] (CADR X0)) (TRS_ISSORT[A32] (CADDR X0)) (NOT (CDDDR X0)) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT (CADDR X0)) (+ 1 (ACL2-COUNT (CDR X0))))). This simplifies, using the :definitions ACL2-COUNT and FIX, the :executable- counterpart of ACL2-COUNT, the :rewrite rules COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 2'' (IMPLIES (AND (CONSP X0) (CONSP (CDR X0)) (CONSP (CDDR X0)) (EQUAL 'TRS_CONS (CAR X0)) (TRS_ISSORT[A0] (CADR X0)) (TRS_ISSORT[A32] (CADDR X0)) (NOT (CDDDR X0)) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT (CADDR X0)) (+ 1 1 (ACL2-COUNT (CADR X0)) 1 (ACL2-COUNT (CADDR X0))))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1 (IMPLIES (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (AND (EQUAL (CAR X0) 'TRS_NIL) (EQUAL (CAR X1) 'TRS_NIL))) (NOT (AND (EQUAL (CAR X0) 'TRS_NIL) (EQUAL (CAR X1) 'TRS_CONS))) (NOT (AND (EQUAL (CAR X0) 'TRS_CONS) (EQUAL (CAR X1) 'TRS_NIL)))) (O< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). This simplifies, using the :definitions O-FINP and O< and the :type- prescription rule ACL2-COUNT, to the following four conjectures. Subgoal 1.4 (IMPLIES (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X0) 'TRS_NIL)) (NOT (EQUAL (CAR X0) 'TRS_CONS))) (< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32]. Subgoal 1.3 (IMPLIES (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X0) 'TRS_NIL)) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). The destructor terms (CAR X0) and (CDR X0) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X0 by (CONS X2 X3), (CAR X0) by X2 and (CDR X0) by X3. (2) Use CAR-CDR-ELIM, again, to replace X3 by (CONS X4 X5), (CAR X3) by X4 and (CDR X3) by X5. These steps produce the following three goals. Subgoal 1.3.3 (IMPLIES (AND (NOT (CONSP X0)) (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X0) 'TRS_NIL)) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32]. Subgoal 1.3.2 (IMPLIES (AND (NOT (CONSP X3)) (CONSP (CONS X2 X3)) (TRS_ISSORT[A32] (CONS X2 X3)) (TRS_ISSORT[A32] X1) (NOT (EQUAL X2 'TRS_NIL)) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT (CAR X3)) (ACL2-COUNT (CONS X2 X3)))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32], primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal 1.3.1 (IMPLIES (AND (CONSP (CONS X4 X5)) (CONSP (LIST* X2 X4 X5)) (TRS_ISSORT[A32] (LIST* X2 X4 X5)) (TRS_ISSORT[A32] X1) (NOT (EQUAL X2 'TRS_NIL)) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT X4) (ACL2-COUNT (LIST* X2 X4 X5)))). This simplifies, using the :definitions ACL2-COUNT, FIX and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 1.3.1' (IMPLIES (AND (CONSP X5) (EQUAL 'TRS_CONS X2) (TRS_ISSORT[A0] X4) (TRS_ISSORT[A32] (CAR X5)) (NOT (CDR X5)) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT X4) (+ 1 1 (ACL2-COUNT X4) (ACL2-COUNT X5)))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1.2 (IMPLIES (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (NOT (EQUAL (CAR X0) 'TRS_NIL))) (< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). The destructor terms (CAR X0) and (CDR X0) can be eliminated. Furthermore, those terms are at the root of a chain of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace X0 by (CONS X2 X3), (CAR X0) by X2 and (CDR X0) by X3. (2) Use CAR-CDR-ELIM, again, to replace X3 by (CONS X4 X5), (CAR X3) by X4 and (CDR X3) by X5. These steps produce the following three goals. Subgoal 1.2.3 (IMPLIES (AND (NOT (CONSP X0)) (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (NOT (EQUAL (CAR X0) 'TRS_NIL))) (< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32]. Subgoal 1.2.2 (IMPLIES (AND (NOT (CONSP X3)) (CONSP (CONS X2 X3)) (TRS_ISSORT[A32] (CONS X2 X3)) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (NOT (EQUAL X2 'TRS_NIL))) (< (ACL2-COUNT (CAR X3)) (ACL2-COUNT (CONS X2 X3)))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32], primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS. Subgoal 1.2.1 (IMPLIES (AND (CONSP (CONS X4 X5)) (CONSP (LIST* X2 X4 X5)) (TRS_ISSORT[A32] (LIST* X2 X4 X5)) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (NOT (EQUAL X2 'TRS_NIL))) (< (ACL2-COUNT X4) (ACL2-COUNT (LIST* X2 X4 X5)))). This simplifies, using the :definitions ACL2-COUNT, FIX and TRS_ISSORT[A32], the :executable-counterparts of ACL2-COUNT and EQUAL, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to Subgoal 1.2.1' (IMPLIES (AND (CONSP X5) (EQUAL 'TRS_CONS X2) (TRS_ISSORT[A0] X4) (TRS_ISSORT[A32] (CAR X5)) (NOT (CDR X5)) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL))) (< (ACL2-COUNT X4) (+ 1 1 (ACL2-COUNT X4) (ACL2-COUNT X5)))). But simplification reduces this to T, using linear arithmetic, primitive type reasoning and the :type-prescription rule ACL2-COUNT. Subgoal 1.1 (IMPLIES (AND (TRS_ISSORT[A32] X0) (TRS_ISSORT[A32] X1) (NOT (EQUAL (CAR X1) 'TRS_NIL)) (NOT (EQUAL (CAR X1) 'TRS_CONS))) (< (ACL2-COUNT (CADR X0)) (ACL2-COUNT X0))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32]. Q.E.D. That completes the proof of the measure theorem for TRS_EQUAL_SORT[A32]. Thus, we admit this function under the principle of definition. We observe that the type of TRS_EQUAL_SORT[A32] is described by the theorem (AND (CONSP (TRS_EQUAL_SORT[A32] X0 X1)) (TRUE-LISTP (TRS_EQUAL_SORT[A32] X0 X1))). We used the :executable-counterpart of EQUAL, primitive type reasoning and the :type-prescription rule TRS_AND. Summary Form: ( DEFUN TRS_EQUAL_SORT[A32] ...) Rules: ((:DEFINITION ACL2-COUNT) (:DEFINITION EQ) (:DEFINITION FIX) (:DEFINITION NOT) (:DEFINITION O-FINP) (:DEFINITION O<) (:DEFINITION TRS_ISSORT[A32]) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART ACL2-COUNT) (:EXECUTABLE-COUNTERPART EQUAL) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:REWRITE COMMUTATIVITY-OF-+) (:REWRITE UNICITY-OF-0) (:TYPE-PRESCRIPTION ACL2-COUNT) (:TYPE-PRESCRIPTION TRS_AND)) Warnings: None Time: 0.03 seconds (prove: 0.03, print: 0.00, other: 0.00) TRS_EQUAL_SORT[A32] ACL2 !> [Note: A hint was supplied for our processing of the goal above. Thanks!] By the simple :definition EQ we reduce the conjecture to Goal' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) (LIST 'TRS_CONS TRS_X TRS_Y)) '(TRS_TRUE))). This simplifies, using the :definitions TRS_DELPRIME, TRS_EQUAL_BOOL, TRS_ISBOOL and TRS_ISSORT[A32], the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription rules TRS_EQ, TRS_ISSORT[A0] and TRS_ISSORT[A32], to Goal'' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). Name the formula above *1. Perhaps we can prove *1 by induction. Seven 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 (TRS_MIN TRS_X TRS_Y). This suggestion was produced using the :induction rules TRS_DELPRIME, TRS_ISSORT[A32] and TRS_MIN. If we let (:P TRS_X TRS_Y) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y))) (:P TRS_X TRS_Y)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (NOT (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)))) (:P TRS_X TRS_Y)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (:P (CADR TRS_Y) (CADDR TRS_Y))) (:P TRS_X TRS_Y)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE))) (:P TRS_X (CADDR TRS_Y))) (:P TRS_X TRS_Y)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (EQ (CAR TRS_Y) 'TRS_NIL)) (:P TRS_X TRS_Y))). This induction is justified by the same argument used to admit TRS_MIN. Note, however, that the unmeasured variable TRS_X is being instantiated. When applied to the goal at hand the above induction scheme produces thirteen nontautological subgoals. Subgoal *1/13 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (NOT (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/13' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (NOT (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_EQUAL_BOOL, TRS_ISBOOL and TRS_ISSORT[A32], the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type-prescription rule TRS_LE. Subgoal *1/12 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (EQUAL (TRS_DELPRIME (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)) (CADDR TRS_Y)) '(TRS_TRUE)) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/12' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (EQUAL (TRS_DELPRIME (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)) (CADDR TRS_Y)) '(TRS_TRUE)) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_DELPRIME, TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable- counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type-prescription rules TRS_EQ, TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/11 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (CDR (TRS_EQ (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)) (CADR TRS_Y))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/11' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (CDR (TRS_EQ (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)) (CADR TRS_Y))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_DELPRIME, TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable- counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type-prescription rules TRS_EQ, TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/10 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)) (CADR TRS_Y))))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/10' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)) (CADR TRS_Y))))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_DELPRIME, TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable- counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type-prescription rules TRS_EQ, TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/9 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (TRS_ISSORT[A0] (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/9' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (TRS_ISSORT[A0] (TRS_MIN (CADR TRS_Y) (CADDR TRS_Y)))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type- prescription rules TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/8 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (TRS_ISSORT[A32] (CADDR TRS_Y))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/8' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (TRS_ISSORT[A32] (CADDR TRS_Y))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32] and the :executable-counterpart of EQUAL. Subgoal *1/7 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (TRS_ISSORT[A0] (CADR TRS_Y))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/7' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (NOT (AND (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)))) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_FALSE)) (NOT (TRS_ISSORT[A0] (CADR TRS_Y))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32] and the :executable-counterpart of EQUAL. Subgoal *1/6 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X (CADDR TRS_Y)) (CADDR TRS_Y)) '(TRS_TRUE)) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/6' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X (CADDR TRS_Y)) (CADDR TRS_Y)) '(TRS_TRUE)) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_DELPRIME, TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable- counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type-prescription rules TRS_EQ, TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/5 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE))) (CDR (TRS_EQ (TRS_MIN TRS_X (CADDR TRS_Y)) TRS_X)) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/5' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)) (CDR (TRS_EQ (TRS_MIN TRS_X (CADDR TRS_Y)) TRS_X)) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type- prescription rules TRS_EQ, TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/4 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE))) (NOT (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X (CADDR TRS_Y)) TRS_X)))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/4' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)) (NOT (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X (CADDR TRS_Y)) TRS_X)))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type- prescription rules TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/3 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE))) (NOT (TRS_ISSORT[A0] (TRS_MIN TRS_X (CADDR TRS_Y)))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/3' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)) (NOT (TRS_ISSORT[A0] (TRS_MIN TRS_X (CADDR TRS_Y)))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definitions TRS_EQUAL_BOOL, TRS_ISBOOL, TRS_ISSORT[A32] and TRS_MIN, the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning and the :type- prescription rules TRS_ISSORT[A0], TRS_ISSORT[A32] and TRS_LE. Subgoal *1/2 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (NOT (EQ (CAR TRS_Y) 'TRS_NIL)) (AND (EQ (CAR TRS_Y) 'TRS_CONS) (EQ (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE))) (NOT (TRS_ISSORT[A32] (CADDR TRS_Y))) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/2' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (NOT (EQUAL (CAR TRS_Y) 'TRS_NIL)) (EQUAL (CAR TRS_Y) 'TRS_CONS) (EQUAL (TRS_EQUAL_BOOL (TRS_LE TRS_X (CADR TRS_Y)) '(TRS_TRUE)) '(TRS_TRUE)) (NOT (TRS_ISSORT[A32] (CADDR TRS_Y))) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). But simplification reduces this to T, using the :definition TRS_ISSORT[A32] and the :executable-counterpart of EQUAL. Subgoal *1/1 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y)) (EQ (CAR TRS_Y) 'TRS_NIL) (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). By the simple :definition EQ we reduce the conjecture to Subgoal *1/1' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A32] TRS_Y) (EQUAL (CAR TRS_Y) 'TRS_NIL) (TRS_ISSORT[A0] (TRS_MIN TRS_X TRS_Y)) (EQUAL 'TRS_FALSE (CAR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X))) (NOT (CDR (TRS_EQ (TRS_MIN TRS_X TRS_Y) TRS_X)))) (EQUAL (TRS_DELPRIME (TRS_MIN TRS_X TRS_Y) TRS_Y) '(TRS_TRUE))). This simplifies, using the :definitions TRS_DELPRIME, TRS_ISSORT[A32] and TRS_MIN, the :executable-counterpart of EQUAL, primitive type reasoning and the :type-prescription rule TRS_ISSORT[A0], to Subgoal *1/1'' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (CONSP TRS_Y) (NOT (CDR TRS_Y)) (EQUAL (CAR TRS_Y) 'TRS_NIL) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). The destructor terms (CAR TRS_Y) and (CDR TRS_Y) can be eliminated by using CAR-CDR-ELIM to replace TRS_Y by (CONS TRS_Y1 TRS_Y2), (CAR TRS_Y) by TRS_Y1 and (CDR TRS_Y) by TRS_Y2 and restrict the type of the new variable TRS_Y1 to be that of the term it replaces. This produces the following goal. Subgoal *1/1''' (IMPLIES (AND (SYMBOLP TRS_Y1) (NOT (EQUAL TRS_Y1 T)) (NOT (EQUAL TRS_Y1 NIL)) (CONSP (CONS TRS_Y1 TRS_Y2)) (TRS_ISSORT[A0] TRS_X) (NOT TRS_Y2) (EQUAL TRS_Y1 'TRS_NIL) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). By case analysis we reduce the conjecture to Subgoal *1/1'4' (IMPLIES (AND (SYMBOLP TRS_Y1) (NOT (EQUAL TRS_Y1 T)) TRS_Y1 (CONSP (CONS TRS_Y1 TRS_Y2)) (TRS_ISSORT[A0] TRS_X) (NOT TRS_Y2) (EQUAL TRS_Y1 'TRS_NIL) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). This simplifies, using the :executable-counterparts of CONS, CONSP, EQUAL, NOT and SYMBOLP, to Subgoal *1/1'5' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). 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. These merge into one derived induction scheme. We will induct according to a scheme suggested by (TRS_EQ TRS_X TRS_X). This suggestion was produced using the :induction rules TRS_EQ and TRS_ISSORT[A0]. If we let (:P TRS_X) denote *1.1 above then the induction scheme we'll use is (AND (IMPLIES (NOT (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X))) (:P TRS_X)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0))) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_S))) (NOT (AND (EQ (CAR TRS_X) 'TRS_S) (EQ (CAR TRS_X) 'TRS_0))) T (:P (CADR TRS_X))) (:P TRS_X)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0))) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_S))) (AND (EQ (CAR TRS_X) 'TRS_S) (EQ (CAR TRS_X) 'TRS_0))) (:P TRS_X)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0))) (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_S))) (:P TRS_X)) (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0))) (:P TRS_X))). This induction is justified by the same argument used to admit TRS_EQ. When applied to the goal at hand the above induction scheme produces four nontautological subgoals. Subgoal *1.1/4 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0))) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_S))) (NOT (AND (EQ (CAR TRS_X) 'TRS_S) (EQ (CAR TRS_X) 'TRS_0))) T (CDR (TRS_EQ (CADR TRS_X) (CADR TRS_X))) (TRS_ISSORT[A0] TRS_X) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). By the simple :definition EQ we reduce the conjecture to Subgoal *1.1/4' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_0) (EQUAL (CAR TRS_X) 'TRS_0))) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_0) (EQUAL (CAR TRS_X) 'TRS_S))) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_S) (EQUAL (CAR TRS_X) 'TRS_0))) (CDR (TRS_EQ (CADR TRS_X) (CADR TRS_X))) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). But simplification reduces this to T, using the :definitions TRS_EQ and TRS_ISSORT[A0], the :executable-counterpart of EQUAL, primitive type reasoning and the :type-prescription rules TRS_EQ and TRS_ISSORT[A0]. Subgoal *1.1/3 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0))) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_S))) (NOT (AND (EQ (CAR TRS_X) 'TRS_S) (EQ (CAR TRS_X) 'TRS_0))) T (NOT (EQUAL 'TRS_FALSE (CAR (TRS_EQ (CADR TRS_X) (CADR TRS_X))))) (TRS_ISSORT[A0] TRS_X) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). By the simple :definition EQ we reduce the conjecture to Subgoal *1.1/3' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_0) (EQUAL (CAR TRS_X) 'TRS_0))) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_0) (EQUAL (CAR TRS_X) 'TRS_S))) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_S) (EQUAL (CAR TRS_X) 'TRS_0))) (NOT (EQUAL 'TRS_FALSE (CAR (TRS_EQ (CADR TRS_X) (CADR TRS_X))))) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). But simplification reduces this to T, using the :definitions TRS_EQ and TRS_ISSORT[A0], the :executable-counterpart of EQUAL, primitive type reasoning and the :type-prescription rule TRS_ISSORT[A0]. Subgoal *1.1/2 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0))) (NOT (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_S))) (NOT (AND (EQ (CAR TRS_X) 'TRS_S) (EQ (CAR TRS_X) 'TRS_0))) T (NOT (TRS_ISSORT[A0] (CADR TRS_X))) (TRS_ISSORT[A0] TRS_X) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). By the simple :definition EQ we reduce the conjecture to Subgoal *1.1/2' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_0) (EQUAL (CAR TRS_X) 'TRS_0))) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_0) (EQUAL (CAR TRS_X) 'TRS_S))) (NOT (AND (EQUAL (CAR TRS_X) 'TRS_S) (EQUAL (CAR TRS_X) 'TRS_0))) (NOT (TRS_ISSORT[A0] (CADR TRS_X))) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). But simplification reduces this to T, using the :definition TRS_ISSORT[A0] and primitive type reasoning. Subgoal *1.1/1 (IMPLIES (AND (AND (TRS_ISSORT[A0] TRS_X) (TRS_ISSORT[A0] TRS_X)) (AND (EQ (CAR TRS_X) 'TRS_0) (EQ (CAR TRS_X) 'TRS_0)) (TRS_ISSORT[A0] TRS_X) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). By the simple :definition EQ we reduce the conjecture to Subgoal *1.1/1' (IMPLIES (AND (TRS_ISSORT[A0] TRS_X) (EQUAL (CAR TRS_X) 'TRS_0) (EQUAL 'TRS_FALSE (CAR (TRS_EQ TRS_X TRS_X)))) (CDR (TRS_EQ TRS_X TRS_X))). But simplification reduces this to T, using the :definitions TRS_EQ and TRS_ISSORT[A0], the :executable-counterparts of CAR and EQUAL and primitive type reasoning. That completes the proofs of *1.1 and *1. Q.E.D. Summary Form: ( DEFTHM TEST ...) Rules: ((:DEFINITION EQ) (:DEFINITION NOT) (:DEFINITION TRS_DELPRIME) (:DEFINITION TRS_EQ) (:DEFINITION TRS_EQUAL_BOOL) (:DEFINITION TRS_ISBOOL) (:DEFINITION TRS_ISSORT[A0]) (:DEFINITION TRS_ISSORT[A32]) (:DEFINITION TRS_MIN) (:ELIM CAR-CDR-ELIM) (:EXECUTABLE-COUNTERPART CAR) (:EXECUTABLE-COUNTERPART CONS) (:EXECUTABLE-COUNTERPART CONSP) (:EXECUTABLE-COUNTERPART EQUAL) (:EXECUTABLE-COUNTERPART NOT) (:EXECUTABLE-COUNTERPART SYMBOLP) (:EXECUTABLE-COUNTERPART TRS_ISBOOL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:INDUCTION TRS_DELPRIME) (:INDUCTION TRS_EQ) (:INDUCTION TRS_ISSORT[A0]) (:INDUCTION TRS_ISSORT[A32]) (:INDUCTION TRS_MIN) (:REWRITE CAR-CONS) (:REWRITE CDR-CONS) (:TYPE-PRESCRIPTION TRS_EQ) (:TYPE-PRESCRIPTION TRS_ISSORT[A0]) (:TYPE-PRESCRIPTION TRS_ISSORT[A32]) (:TYPE-PRESCRIPTION TRS_LE)) Warnings: None Time: 0.26 seconds (prove: 0.25, print: 0.01, other: 0.00) TEST ACL2 !>Bye.