GCL (GNU Common Lisp) 2.6.5 CLtL1 Oct 17 2004 12:48:32
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License: GPL due to GPL'ed components: (READLINE BFD UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter
Use (help) to get some basic information on how to use GCL.
ACL2 Version 2.9 built December 9, 2004 12:40:52.
Copyright (C) 2004 University of Texas at Austin
ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you
are welcome to redistribute it under certain conditions. For details,
see the GNU General Public License.
Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*
NIL).
See the documentation topic note-2-9 for recent changes.
NOTE!! Proof trees are disabled in ACL2. To enable them in emacs,
look under the ACL2 source directory in interface/emacs/README.doc;
and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2
command loop. Look in the ACL2 documentation under PROOF-TREE.
Loading /export/v/filer2/moore/acl2-init.lsp
Finished loading /export/v/filer2/moore/acl2-init.lsp
ACL2 Version 2.9. Level 1. Cbd
"/export/v/filer3/v0q005/text/marktoberdorf-04/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !>(certify-book "how-to-prove-thms")
CERTIFICATION ATTEMPT FOR
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp"
ACL2 Version 2.9
* Step 1: Read
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp"
and compute its check sum.
* Step 2: There were 115 forms in the file. The check sum is 190369092.
We now attempt to establish that each form, whether local or non-local,
is indeed an admissible embedded event form in the context of the previously
admitted ones. Note that proof-tree output is inhibited during this
check; see :DOC proof-tree.
ACL2 >>(DEFUN DUP (X)
(IF (CONSP X)
(CONS (CAR X)
(CONS (CAR X) (DUP (CDR X))))
NIL))
The admission of DUP 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 DUP is described by the
theorem (TRUE-LISTP (DUP X)). We used primitive type reasoning.
Summary
Form: ( DEFUN DUP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
DUP
ACL2 >>(DEFTHM DUP-EXAMPLES
(AND (EQUAL (DUP '(1 2 3)) '(1 1 2 2 3 3))
(EQUAL (DUP '(HELLO)) '(HELLO HELLO))
(EQUAL (DUP '(A B C . D))
'(A A B B C C)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of DUP, EQUAL and IF.
Q.E.D.
Summary
Form: ( DEFTHM DUP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART DUP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
DUP-EXAMPLES
ACL2 >>(DEFUN APP (X Y)
(IF (CONSP X)
(CONS (CAR X) (APP (CDR X) Y))
Y))
The admission of APP is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X). We observe that the type of APP is described by the
theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive
type reasoning.
Summary
Form: ( DEFUN APP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
APP
ACL2 >>(DEFTHM APP-EXAMPLES
(AND (EQUAL (APP '(1 2 3) '(4 5 6))
'(1 2 3 4 5 6))
(EQUAL (APP '(3 2 1) '(0)) '(3 2 1 0))
(EQUAL (APP '(A B C . D) '(E F))
'(A B C E F)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of APP, EQUAL and IF.
Q.E.D.
Summary
Form: ( DEFTHM APP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART APP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
APP-EXAMPLES
ACL2 >>(DEFUN MEMP (E X)
(IF (CONSP X)
(IF (EQUAL E (CAR X))
T (MEMP E (CDR X)))
NIL))
The admission of MEMP 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 MEMP is described by the
theorem (OR (EQUAL (MEMP E X) T) (EQUAL (MEMP E X) NIL)).
Summary
Form: ( DEFUN MEMP ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP
ACL2 >>(DEFTHM MEMP-EXAMPLES
(AND (MEMP 1 '(0 1 2 3))
(NOT (MEMP 5 '(0 1 2 3)))
(NOT (MEMP 2 '((0) (1) (2))))
(MEMP '(2) '((0) (1) (2)))
(NOT (MEMP 2 '(0 1 . 2))))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of IF and MEMP.
Q.E.D.
Summary
Form: ( DEFTHM MEMP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART MEMP)
(:EXECUTABLE-COUNTERPART NOT))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-EXAMPLES
ACL2 >>(DEFUN REV (X)
(IF (CONSP X)
(APP (REV (CDR X)) (CONS (CAR X) NIL))
NIL))
The admission of REV is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X). We observe that the type of REV is described by the
theorem (OR (CONSP (REV X)) (EQUAL (REV X) NIL)). We used primitive
type reasoning and the :type-prescription rule APP.
Summary
Form: ( DEFUN REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION APP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV
ACL2 >>(DEFTHM REV-EXAMPLES
(AND (EQUAL (REV '(1 2 3)) '(3 2 1))
(EQUAL (REV '(OK)) '(OK))
(EQUAL (REV '(1 2 3 . END)) '(3 2 1)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and REV.
Q.E.D.
Summary
Form: ( DEFTHM REV-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART REV))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV-EXAMPLES
ACL2 >>(DEFUN REV1 (X A)
(IF (CONSP X)
(REV1 (CDR X) (CONS (CAR X) A))
A))
The admission of REV1 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 REV1 is described by the
theorem (OR (CONSP (REV1 X A)) (EQUAL (REV1 X A) A)). We used primitive
type reasoning.
Summary
Form: ( DEFUN REV1 ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV1
ACL2 >>(DEFTHM REV1-EXAMPLES
(AND (EQUAL (REV1 '(1 2 3) NIL) '(3 2 1))
(EQUAL (REV1 '(OK) NIL) '(OK))
(EQUAL (REV1 '(1 2 3 . END) NIL)
'(3 2 1))
(EQUAL (REV1 '(A B C) '(1 2 3))
'(C B A 1 2 3)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and REV1.
Q.E.D.
Summary
Form: ( DEFTHM REV1-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART REV1))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV1-EXAMPLES
ACL2 >>(DEFUN PROPERP (X)
(IF (CONSP X)
(PROPERP (CDR X))
(EQUAL X NIL)))
The admission of PROPERP 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 PROPERP is described by
the theorem (OR (EQUAL (PROPERP X) T) (EQUAL (PROPERP X) NIL)). We
used primitive type reasoning.
Summary
Form: ( DEFUN PROPERP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP
ACL2 >>(DEFTHM PROPERP-EXAMPLES
(AND (PROPERP '(1 2 3))
(NOT (PROPERP '(1 2 3 . END)))
(PROPERP '((A . 1) (B . 2) (C . 3)))
(PROPERP NIL)
(NOT (PROPERP 7)))
:RULE-CLASSES NIL)
[SGC for 19 STRING pages..(8001 writable)..(T=2).GC finished]
But we reduce the conjecture to T, by the :executable-counterparts
of IF and PROPERP.
Q.E.D.
Summary
Form: ( DEFTHM PROPERP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART PROPERP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-EXAMPLES
ACL2 >>(DEFUN MAPNIL (X)
(IF (CONSP X)
(CONS NIL (MAPNIL (CDR X)))
NIL))
The admission of MAPNIL 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 MAPNIL is described by
the theorem (TRUE-LISTP (MAPNIL X)). We used primitive type reasoning.
Summary
Form: ( DEFUN MAPNIL ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAPNIL
ACL2 >>(DEFTHM MAPNIL-EXAMPLES
(AND (EQUAL (MAPNIL '(1 2 3)) '(NIL NIL NIL))
(EQUAL (MAPNIL '(HELLO)) '(NIL)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and MAPNIL.
Q.E.D.
Summary
Form: ( DEFTHM MAPNIL-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART MAPNIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAPNIL-EXAMPLES
ACL2 >>(DEFUN SWAPTREE (X)
(IF (CONSP X)
(CONS (SWAPTREE (CDR X))
(SWAPTREE (CAR X)))
X))
The admission of SWAPTREE 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 could deduce no constraints on the type
of SWAPTREE. However, in normalizing the definition we used primitive
type reasoning.
Summary
Form: ( DEFUN SWAPTREE ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SWAPTREE
ACL2 >>(DEFTHM SWAPTREE-EXAMPLES
(AND (EQUAL (SWAPTREE '((A . B) C . D))
'((D . C) B . A))
(EQUAL (SWAPTREE '(A B C D))
'((((NIL . D) . C) . B) . A)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and SWAPTREE.
Q.E.D.
Summary
Form: ( DEFTHM SWAPTREE-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART SWAPTREE))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SWAPTREE-EXAMPLES
ACL2 >>(DEFUN ZIPLISTS (X Y)
(IF (CONSP X)
(CONS (CONS (CAR X) (CAR Y))
(ZIPLISTS (CDR X) (CDR Y)))
NIL))
The admission of ZIPLISTS 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 ZIPLISTS is described
by the theorem (TRUE-LISTP (ZIPLISTS X Y)). We used primitive type
reasoning.
Summary
Form: ( DEFUN ZIPLISTS ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ZIPLISTS
ACL2 >>(DEFTHM ZIPLISTS-EXAMPLES
(AND (EQUAL (ZIPLISTS '(A B C) '(1 2 3 4))
'((A . 1) (B . 2) (C . 3)))
(EQUAL (ZIPLISTS '(A B C) '(1 2))
'((A . 1) (B . 2) (C))))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and ZIPLISTS.
Q.E.D.
Summary
Form: ( DEFTHM ZIPLISTS-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART ZIPLISTS))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ZIPLISTS-EXAMPLES
ACL2 >>(DEFUN LOOKUP (X A)
(IF (CONSP A)
(IF (EQUAL X (CAR (CAR A)))
(CDR (CAR A))
(LOOKUP X (CDR A)))
NIL))
The admission of LOOKUP 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 A). We could deduce no constraints on the type of LOOKUP.
Summary
Form: ( DEFUN LOOKUP ...)
Rules: NIL
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
LOOKUP
ACL2 >>(DEFTHM LOOKUP-EXAMPLES
(AND (EQUAL (LOOKUP 'B
'((A . 1) (B . 2) (C . 3) (A . 4)))
2)
(EQUAL (LOOKUP 'A
'((A . 1) (B . 2) (C . 3) (A . 4)))
1)
(EQUAL (LOOKUP 'X
'((A . 1) (B . 2) (C . 3) (A . 4)))
NIL)
(EQUAL (LOOKUP 'J '((I . 1) (J) (K . 123)))
NIL))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and LOOKUP.
Q.E.D.
Summary
Form: ( DEFTHM LOOKUP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART LOOKUP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LOOKUP-EXAMPLES
ACL2 >>(DEFUN FOUNDP (X A)
(IF (CONSP A)
(IF (EQUAL X (CAR (CAR A)))
T (FOUNDP X (CDR A)))
NIL))
The admission of FOUNDP 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 A). We observe that the type of FOUNDP is described by
the theorem (OR (EQUAL (FOUNDP X A) T) (EQUAL (FOUNDP X A) NIL)).
Summary
Form: ( DEFUN FOUNDP ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FOUNDP
ACL2 >>(DEFTHM FOUNDP-EXAMPLES
(AND (EQUAL (FOUNDP 'B
'((A . 1) (B . 2) (C . 3) (A . 4)))
T)
(EQUAL (FOUNDP 'A
'((A . 1) (B . 2) (C . 3) (A . 4)))
T)
(EQUAL (FOUNDP 'X
'((A . 1) (B . 2) (C . 3) (A . 4)))
NIL)
(EQUAL (FOUNDP 'J '((I . 1) (J) (K . 123)))
T))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, FOUNDP and IF.
Q.E.D.
Summary
Form: ( DEFTHM FOUNDP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART FOUNDP)
(:EXECUTABLE-COUNTERPART IF))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FOUNDP-EXAMPLES
ACL2 >>(DEFUN SUBP (X Y)
(IF (CONSP X)
(IF (MEMP (CAR X) Y)
(SUBP (CDR X) Y)
NIL)
T))
The admission of SUBP 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 SUBP is described by the
theorem (OR (EQUAL (SUBP X Y) T) (EQUAL (SUBP X Y) NIL)).
Summary
Form: ( DEFUN SUBP ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBP
ACL2 >>(DEFTHM SUBP-EXAMPLES
(AND (SUBP '(A B B A) '(A B))
(SUBP '(A B C) '(E D C B A))
(NOT (SUBP '(A B) '(A C A D A F))))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of IF and SUBP.
Q.E.D.
[SGC for 19 STRING pages..(8003 writable)..(T=1).GC finished]
Summary
Form: ( DEFTHM SUBP-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART SUBP))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
SUBP-EXAMPLES
ACL2 >>(DEFUN INT (X Y)
(IF (CONSP X)
(IF (MEMP (CAR X) Y)
(CONS (CAR X) (INT (CDR X) Y))
(INT (CDR X) Y))
NIL))
The admission of INT 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 INT is described by the
theorem (TRUE-LISTP (INT X Y)). We used primitive type reasoning.
Summary
Form: ( DEFUN INT ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
INT
ACL2 >>(DEFTHM INT-EXAMPLES
(AND (EQUAL (INT '(A B C) '(A B A D)) '(A B))
(EQUAL (INT '(A B C) '(X Y Z)) NIL)
(EQUAL (INT '(A A B B) '(A B C))
'(A A B B)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and INT.
Q.E.D.
Summary
Form: ( DEFTHM INT-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART INT))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INT-EXAMPLES
ACL2 >>(DEFUN MEM (E X)
(IF (CONSP X)
(IF (EQUAL E (CAR X)) X (MEM E (CDR X)))
NIL))
The admission of MEM is trivial, using the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X). We observe that the type of MEM is described by the
theorem (OR (CONSP (MEM E X)) (EQUAL (MEM E X) NIL)).
Summary
Form: ( DEFUN MEM ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEM
ACL2 >>(DEFUN LONESOMEP (E LST)
(IF (MEM E LST)
(NOT (MEM E (CDR (MEM E LST))))
NIL))
Since LONESOMEP is non-recursive, its admission is trivial. We observe
that the type of LONESOMEP is described by the theorem
(OR (EQUAL (LONESOMEP E LST) T) (EQUAL (LONESOMEP E LST) NIL)).
Summary
Form: ( DEFUN LONESOMEP ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LONESOMEP
ACL2 >>(DEFUN COLLECT-LONESOMEP (A B)
(IF (CONSP A)
(IF (LONESOMEP (CAR A) B)
(CONS (CAR A)
(COLLECT-LONESOMEP (CDR A) B))
(COLLECT-LONESOMEP (CDR A) B))
NIL))
The admission of COLLECT-LONESOMEP 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 A). We observe that the type of COLLECT-
LONESOMEP is described by the theorem (TRUE-LISTP (COLLECT-LONESOMEP A B)).
We used primitive type reasoning.
Summary
Form: ( DEFUN COLLECT-LONESOMEP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
COLLECT-LONESOMEP
ACL2 >>(DEFUN LEAVES (X)
(IF (CONSP X)
(APP (LEAVES (CAR X)) (LEAVES (CDR X)))
(CONS X NIL)))
The admission of LEAVES 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 LEAVES is described by
the theorem (CONSP (LEAVES X)). We used primitive type reasoning and
the :type-prescription rule APP.
Summary
Form: ( DEFUN LEAVES ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION APP))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
LEAVES
ACL2 >>(DEFUN LONESOMES (X)
(COLLECT-LONESOMEP (LEAVES X)
(LEAVES X)))
Since LONESOMES is non-recursive, its admission is trivial. We observe
that the type of LONESOMES is described by the theorem
(TRUE-LISTP (LONESOMES X)). We used the :type-prescription rule COLLECT-
LONESOMEP.
Summary
Form: ( DEFUN LONESOMES ...)
Rules: ((:TYPE-PRESCRIPTION COLLECT-LONESOMEP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LONESOMES
ACL2 >>(DEFTHM LONESOMES-EXAMPLES
(AND (EQUAL (LONESOMES '((A . B) C . A))
'(B C))
(EQUAL (LONESOMES '((A . A) . A)) NIL)
(EQUAL (LONESOMES '(((A . B) B . C) (X . Y) C . X))
'(A Y)))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the :executable-counterparts
of EQUAL, IF and LONESOMES.
Q.E.D.
Summary
Form: ( DEFTHM LONESOMES-EXAMPLES ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART IF)
(:EXECUTABLE-COUNTERPART LONESOMES))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LONESOMES-EXAMPLES
ACL2 >>(DEFUN TREECOPY (X)
(IF (CONSP X)
(CONS (TREECOPY (CAR X))
(TREECOPY (CDR X)))
X))
The admission of TREECOPY 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 could deduce no constraints on the type
of TREECOPY. However, in normalizing the definition we used primitive
type reasoning.
Summary
Form: ( DEFUN TREECOPY ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TREECOPY
ACL2 >>(DEFTHM TREECOPY-IS-ID (EQUAL (TREECOPY X) 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 (TREECOPY X). This
suggestion was produced using the :induction rule TREECOPY. 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 (CAR X))
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit TREECOPY,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(EQUAL (TREECOPY X) X)).
But simplification reduces this to T, using the :definition TREECOPY
and primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(EQUAL (TREECOPY (CAR X)) (CAR X))
(EQUAL (TREECOPY (CDR X)) (CDR X)))
(EQUAL (TREECOPY X) X)).
But simplification reduces this to T, using the :definition TREECOPY,
primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM TREECOPY-IS-ID ...)
Rules: ((:DEFINITION TREECOPY)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION TREECOPY)
(:REWRITE CAR-CDR-ELIM))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TREECOPY-IS-ID
ACL2 >>(DEFTHM ASSOCIATIVITY-OF-APP
(EQUAL (APP (APP A B) C)
(APP A (APP B C))))
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 A B). This
suggestion was produced using the :induction rule APP. If we let
(:P A B C) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
(IMPLIES (AND (CONSP A) (:P (CDR A) B C))
(:P A B C))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(EQUAL (APP (APP A B) C)
(APP A (APP B C)))).
But simplification reduces this to T, using the :definition APP and
primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
(EQUAL (APP (APP A B) C)
(APP A (APP B C)))).
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.
Q.E.D.
Summary
Form: ( DEFTHM ASSOCIATIVITY-OF-APP ...)
Rules: ((:DEFINITION APP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ASSOCIATIVITY-OF-APP
ACL2 >>(DEFTHM DUP-APP
(EQUAL (DUP (APP A B))
(APP (DUP A) (DUP B))))
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 A B). This
suggestion was produced using the :induction rules APP and DUP. If
we let (:P A B) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
(IMPLIES (AND (CONSP A) (:P (CDR A) B))
(:P A B))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(EQUAL (DUP (APP A B))
(APP (DUP A) (DUP B)))).
But simplification reduces this to T, using the :definitions APP and
DUP, the :executable-counterpart of CONSP and primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(EQUAL (DUP (APP (CDR A) B))
(APP (DUP (CDR A)) (DUP B))))
(EQUAL (DUP (APP A B))
(APP (DUP A) (DUP B)))).
But simplification reduces this to T, using the :definitions APP and
DUP, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule DUP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM DUP-APP ...)
Rules: ((:DEFINITION APP)
(:DEFINITION DUP)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:INDUCTION DUP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION DUP))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
DUP-APP
ACL2 >>(DEFTHM DUP-MAPNIL
(EQUAL (DUP (MAPNIL A))
(MAPNIL (DUP A))))
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 (DUP A). This suggestion
was produced using the :induction rules DUP and MAPNIL. If we let
(:P A) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A))
(IMPLIES (AND (CONSP A) (:P (CDR A)))
(:P A))).
This induction is justified by the same argument used to admit DUP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(EQUAL (DUP (MAPNIL A))
(MAPNIL (DUP A)))).
But simplification reduces this to T, using the :definitions DUP and
MAPNIL and the :executable-counterparts of DUP, EQUAL and MAPNIL.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(EQUAL (DUP (MAPNIL (CDR A)))
(MAPNIL (DUP (CDR A)))))
(EQUAL (DUP (MAPNIL A))
(MAPNIL (DUP A)))).
But simplification reduces this to T, using the :definitions DUP and
MAPNIL, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rules DUP and MAPNIL.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM DUP-MAPNIL ...)
Rules: ((:DEFINITION DUP)
(:DEFINITION MAPNIL)
(:EXECUTABLE-COUNTERPART DUP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART MAPNIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION DUP)
(:INDUCTION MAPNIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION DUP)
(:TYPE-PRESCRIPTION MAPNIL))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
DUP-MAPNIL
ACL2 >>(DEFTHM PROPERP-APP-NIL (PROPERP (APP A NIL)))
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 (APP A 'NIL). This
suggestion was produced using the :induction rule APP. If we let (:P A)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A))
(IMPLIES (AND (CONSP A) (:P (CDR A)))
(:P A))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(PROPERP (APP A NIL))).
But simplification reduces this to T, using the :definition APP and
the :executable-counterpart of PROPERP.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(PROPERP (APP (CDR A) NIL)))
(PROPERP (APP A NIL))).
But simplification reduces this to T, using the :definitions APP and
PROPERP, primitive type reasoning, the :rewrite rule CDR-CONS and the
:type-prescription rule PROPERP.
That completes the proof of *1.
Q.E.D.
The storage of PROPERP-APP-NIL depends upon the :type-prescription
rule PROPERP.
Summary
Form: ( DEFTHM PROPERP-APP-NIL ...)
Rules: ((:DEFINITION APP)
(:DEFINITION PROPERP)
(:EXECUTABLE-COUNTERPART PROPERP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION PROPERP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-APP-NIL
ACL2 >>(DEFTHM SWAPTREE-SWAPTREE
(EQUAL (SWAPTREE (SWAPTREE X)) 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 (SWAPTREE X). This
suggestion was produced using the :induction rule SWAPTREE. 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 (CAR X)))
(:P X))).
This induction is justified by the same argument used to admit SWAPTREE,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(EQUAL (SWAPTREE (SWAPTREE X)) X)).
But simplification reduces this to T, using the :definition SWAPTREE
and primitive type reasoning.
[SGC for 21 CFUN pages..(8013 writable)..(T=1).GC finished]
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(EQUAL (SWAPTREE (SWAPTREE (CDR X)))
(CDR X))
(EQUAL (SWAPTREE (SWAPTREE (CAR X)))
(CAR X)))
(EQUAL (SWAPTREE (SWAPTREE X)) X)).
But simplification reduces this to T, using the :definition SWAPTREE,
primitive type reasoning and the :rewrite rules CAR-CDR-ELIM, CAR-CONS
and CDR-CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM SWAPTREE-SWAPTREE ...)
Rules: ((:DEFINITION SWAPTREE)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION SWAPTREE)
(:REWRITE CAR-CDR-ELIM)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
SWAPTREE-SWAPTREE
ACL2 >>(DEFTHM MEMP-APP
(EQUAL (MEMP E (APP A B))
(OR (MEMP E A) (MEMP E B))))
This simplifies, using the :type-prescription rule MEMP, to the following
two conjectures.
Subgoal 2
(IMPLIES (MEMP E A)
(EQUAL (MEMP E (APP A B)) T)).
This simplifies, using primitive type reasoning and the :type-prescription
rule MEMP, to
Subgoal 2'
(IMPLIES (MEMP E A) (MEMP E (APP A B))).
Name the formula above *1.
Subgoal 1
(IMPLIES (NOT (MEMP E A))
(EQUAL (MEMP E (APP A B)) (MEMP E B))).
Normally we would attempt to prove this formula 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. 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 (MEMP E A), but modified
to accommodate (APP A B). These suggestions were produced using the
:induction rules APP and MEMP. If we let (:P A B E) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B E))
(IMPLIES (AND (CONSP A)
(NOT (EQUAL E (CAR A)))
(:P (CDR A) B E))
(:P A B E))
(IMPLIES (AND (CONSP A) (EQUAL E (CAR A)))
(:P A B E))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP A))
(EQUAL (MEMP E (APP A B))
(OR (MEMP E A) (MEMP E B)))).
But simplification reduces this to T, using the :definitions APP and
MEMP and primitive type reasoning.
Subgoal *1/2
(IMPLIES (AND (CONSP A)
(NOT (EQUAL E (CAR A)))
(EQUAL (MEMP E (APP (CDR A) B))
(OR (MEMP E (CDR A)) (MEMP E B))))
(EQUAL (MEMP E (APP A B))
(OR (MEMP E A) (MEMP E B)))).
But simplification reduces this to T, using the :definitions APP and
MEMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule MEMP.
Subgoal *1/1
(IMPLIES (AND (CONSP A) (EQUAL E (CAR A)))
(EQUAL (MEMP E (APP A B))
(OR (MEMP E A) (MEMP E B)))).
But simplification reduces this to T, using the :definitions APP and
MEMP, the :executable-counterpart of EQUAL, primitive type reasoning
and the :rewrite rule CAR-CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MEMP-APP ...)
Rules: ((:DEFINITION APP)
(:DEFINITION MEMP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:INDUCTION MEMP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MEMP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-APP
ACL2 >>(DEFTHM PROBLEM-6-1
(EQUAL (MEMP E (APP A A)) (MEMP E A))
:RULE-CLASSES NIL)
But simplification reduces this to T, using primitive type reasoning,
the :rewrite rule MEMP-APP and the :type-prescription rule MEMP.
Q.E.D.
Summary
Form: ( DEFTHM PROBLEM-6-1 ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE MEMP-APP)
(:TYPE-PRESCRIPTION MEMP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROBLEM-6-1
ACL2 >>(DEFTHM PROPERP-APP
(EQUAL (PROPERP (APP A B)) (PROPERP B)))
ACL2 Warning [Subsume] in ( DEFTHM PROPERP-APP ...): The newly proposed
:REWRITE rule PROPERP-APP probably subsumes the previously added :REWRITE
rule PROPERP-APP-NIL, in the sense that PROPERP-APP will now probably
be applied whenever the old rule would have been.
Name the formula above *1.
Perhaps we can prove *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 (APP A B). This
suggestion was produced using the :induction rule APP. If we let (:P A B)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
(IMPLIES (AND (CONSP A) (:P (CDR A) B))
(:P A B))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(EQUAL (PROPERP (APP A B))
(PROPERP B))).
But simplification reduces this to T, using the :definition APP and
primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(EQUAL (PROPERP (APP (CDR A) B))
(PROPERP B)))
(EQUAL (PROPERP (APP A B))
(PROPERP B))).
But simplification reduces this to T, using the :definitions APP and
PROPERP, primitive type reasoning and the :rewrite rule CDR-CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM PROPERP-APP ...)
Rules: ((:DEFINITION APP)
(:DEFINITION PROPERP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:REWRITE CDR-CONS))
Warnings: Subsume
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-APP
ACL2 >>(DEFTHM PROPERP-REV (PROPERP (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,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(PROPERP (REV X))).
But simplification reduces this to T, using the :definition REV and
the :executable-counterpart of PROPERP.
Subgoal *1/1
(IMPLIES (AND (CONSP X) (PROPERP (REV (CDR X))))
(PROPERP (REV X))).
But simplification reduces this to T, using the :definitions PROPERP
and REV, the :executable-counterpart of PROPERP, primitive type reasoning
and the :rewrite rules CDR-CONS and PROPERP-APP.
That completes the proof of *1.
Q.E.D.
The storage of PROPERP-REV depends upon the :type-prescription rule
PROPERP.
Summary
Form: ( DEFTHM PROPERP-REV ...)
Rules: ((:DEFINITION PROPERP)
(:DEFINITION REV)
(:EXECUTABLE-COUNTERPART PROPERP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION REV)
(:REWRITE CDR-CONS)
(:REWRITE PROPERP-APP)
(:TYPE-PRESCRIPTION PROPERP))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
PROPERP-REV
ACL2 >>(DEFTHM APP-RIGHT-IDENTITY
(IMPLIES (PROPERP 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 PROPERP.
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,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (CONSP X)) (PROPERP X))
(EQUAL (APP X NIL) X)).
But simplification reduces this to T, using the :definition PROPERP,
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))
(PROPERP X))
(EQUAL (APP X NIL) X)).
But simplification reduces this to T, using the :definitions APP and
PROPERP, primitive type reasoning and the :rewrite rule CAR-CDR-ELIM.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(NOT (PROPERP (CDR X)))
(PROPERP X))
(EQUAL (APP X NIL) X)).
But simplification reduces this to T, using the :definition PROPERP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM APP-RIGHT-IDENTITY ...)
Rules: ((:DEFINITION APP)
(:DEFINITION PROPERP)
(:EXECUTABLE-COUNTERPART APP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:INDUCTION PROPERP)
(:REWRITE CAR-CDR-ELIM))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
APP-RIGHT-IDENTITY
ACL2 >>(DEFTHM REV-APP
(EQUAL (REV (APP A B))
(APP (REV B) (REV A))))
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 A B). This
suggestion was produced using the :induction rules APP and REV. If
we let (:P A B) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
(IMPLIES (AND (CONSP A) (:P (CDR A) B))
(:P A B))).
This induction is justified by the same argument used to admit APP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(EQUAL (REV (APP A B))
(APP (REV B) (REV A)))).
But simplification reduces this to T, using the :definitions APP and
REV, primitive type reasoning and the :rewrite rules APP-RIGHT-IDENTITY
and PROPERP-REV.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(EQUAL (REV (APP (CDR A) B))
(APP (REV B) (REV (CDR A)))))
(EQUAL (REV (APP A B))
(APP (REV B) (REV A)))).
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 A)
(EQUAL (REV (APP (CDR A) B))
(APP (REV B) (REV (CDR A)))))
(EQUAL (APP (REV (APP (CDR A) B))
(LIST (CAR A)))
(APP (REV B)
(APP (REV (CDR A)) (LIST (CAR A)))))).
The destructor terms (CAR A) and (CDR A) can be eliminated by using
CAR-CDR-ELIM to replace A by (CONS A1 A2), (CAR A) by A1 and (CDR A)
by A2. This produces the following goal.
Subgoal *1/1''
(IMPLIES (AND (CONSP (CONS A1 A2))
(EQUAL (REV (APP A2 B))
(APP (REV B) (REV A2))))
(EQUAL (APP (REV (APP A2 B)) (LIST A1))
(APP (REV B)
(APP (REV A2) (LIST A1))))).
This simplifies, using primitive type reasoning, to
Subgoal *1/1'''
(IMPLIES (EQUAL (REV (APP A2 B))
(APP (REV B) (REV A2)))
(EQUAL (APP (REV (APP A2 B)) (LIST A1))
(APP (REV B)
(APP (REV A2) (LIST A1))))).
We now use the hypothesis by substituting (APP (REV B) (REV A2)) for
(REV (APP A2 B)) and throwing away the hypothesis. This produces
Subgoal *1/1'4'
(EQUAL (APP (APP (REV B) (REV A2)) (LIST A1))
(APP (REV B) (APP (REV A2) (LIST A1)))).
But we reduce the conjecture to T, by the simple :rewrite rule ASSOCIATIVITY-
OF-APP.
That completes the proof of *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-RIGHT-IDENTITY)
(:REWRITE ASSOCIATIVITY-OF-APP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE PROPERP-REV))
Warnings: None
Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
REV-APP
ACL2 >>(DEFTHM REV-REV
(IMPLIES (PROPERP Z)
(EQUAL (REV (REV Z)) Z)))
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 (REV Z). This suggestion
was produced using the :induction rules PROPERP and REV. If we let
(:P Z) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP Z)) (:P Z))
(IMPLIES (AND (CONSP Z) (:P (CDR Z)))
(:P Z))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT Z) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (CONSP Z)) (PROPERP Z))
(EQUAL (REV (REV Z)) Z)).
But simplification reduces this to T, using the :definition PROPERP,
the :executable-counterparts of CONSP, EQUAL and REV and primitive
type reasoning.
Subgoal *1/2
(IMPLIES (AND (CONSP Z)
(EQUAL (REV (REV (CDR Z))) (CDR Z))
(PROPERP Z))
(EQUAL (REV (REV Z)) Z)).
But simplification reduces this to T, using the :definitions APP, PROPERP
and REV, the :executable-counterparts of CONSP and REV, primitive type
reasoning and the :rewrite rules CAR-CDR-ELIM, CAR-CONS, CDR-CONS and
REV-APP.
Subgoal *1/1
(IMPLIES (AND (CONSP Z)
(NOT (PROPERP (CDR Z)))
(PROPERP Z))
(EQUAL (REV (REV Z)) Z)).
But simplification reduces this to T, using the :definition PROPERP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM REV-REV ...)
Rules: ((:DEFINITION APP)
(:DEFINITION PROPERP)
(:DEFINITION REV)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION PROPERP)
(:INDUCTION REV)
(:REWRITE CAR-CDR-ELIM)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE REV-APP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV-REV
ACL2 >>(DEFTHM TRIPLE-REV
(EQUAL (REV (REV (REV A))) (REV A)))
But simplification reduces this to T, using primitive type reasoning
and the :rewrite rules PROPERP-REV and REV-REV.
Q.E.D.
Summary
Form: ( DEFTHM TRIPLE-REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE PROPERP-REV)
(:REWRITE REV-REV))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRIPLE-REV
ACL2 >>(DEFTHM MEMP-REV
(EQUAL (MEMP E (REV X)) (MEMP E 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 (MEMP E X). This
suggestion was produced using the :induction rules MEMP and REV. If
we let (:P E X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP X)) (:P E X))
(IMPLIES (AND (CONSP X)
(NOT (EQUAL E (CAR X)))
(:P E (CDR X)))
(:P E X))
(IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
(:P E X))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP X))
(EQUAL (MEMP E (REV X)) (MEMP E X))).
But simplification reduces this to T, using the :definitions MEMP and
REV and the :executable-counterparts of CONSP and EQUAL.
Subgoal *1/2
(IMPLIES (AND (CONSP X)
(NOT (EQUAL E (CAR X)))
(EQUAL (MEMP E (REV (CDR X)))
(MEMP E (CDR X))))
(EQUAL (MEMP E (REV X)) (MEMP E X))).
But simplification reduces this to T, using the :definitions MEMP and
REV, the :executable-counterpart of CONSP, primitive type reasoning,
the :rewrite rules CAR-CONS, CDR-CONS and MEMP-APP and the :type-prescription
rule MEMP.
Subgoal *1/1
(IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
(EQUAL (MEMP E (REV X)) (MEMP E X))).
But simplification reduces this to T, using the :definitions MEMP and
REV, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and MEMP-APP and the :type-prescription
rule MEMP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MEMP-REV ...)
Rules: ((:DEFINITION MEMP)
(:DEFINITION REV)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MEMP)
(:INDUCTION REV)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE MEMP-APP)
(:TYPE-PRESCRIPTION MEMP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-REV
ACL2 >>(DEFTHM MEMP-DUP
(EQUAL (MEMP E (DUP X)) (MEMP E 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 (MEMP E X). This
suggestion was produced using the :induction rules DUP and MEMP. If
we let (:P E X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP X)) (:P E X))
(IMPLIES (AND (CONSP X)
(NOT (EQUAL E (CAR X)))
(:P E (CDR X)))
(:P E X))
(IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
(:P E X))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP X))
(EQUAL (MEMP E (DUP X)) (MEMP E X))).
But simplification reduces this to T, using the :definitions DUP and
MEMP and the :executable-counterparts of CONSP and EQUAL.
Subgoal *1/2
(IMPLIES (AND (CONSP X)
(NOT (EQUAL E (CAR X)))
(EQUAL (MEMP E (DUP (CDR X)))
(MEMP E (CDR X))))
(EQUAL (MEMP E (DUP X)) (MEMP E X))).
But simplification reduces this to T, using the :definitions DUP and
MEMP, primitive type reasoning, the :rewrite rules CAR-CONS and CDR-
CONS and the :type-prescription rule DUP.
Subgoal *1/1
(IMPLIES (AND (CONSP X) (EQUAL E (CAR X)))
(EQUAL (MEMP E (DUP X)) (MEMP E X))).
But simplification reduces this to T, using the :definitions DUP and
MEMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rule CAR-CONS and the :type-prescription rule DUP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MEMP-DUP ...)
Rules: ((:DEFINITION DUP)
(:DEFINITION MEMP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION DUP)
(:INDUCTION MEMP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION DUP))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MEMP-DUP
ACL2 >>(DEFTHM COMPLICATED-MEMP-THEOREM
(IMPLIES (MEMP E C)
(MEMP E (REV (DUP (DUP C)))))
:RULE-CLASSES NIL)
But we reduce the conjecture to T, by the simple :rewrite rules MEMP-
DUP and MEMP-REV.
Q.E.D.
Summary
Form: ( DEFTHM COMPLICATED-MEMP-THEOREM ...)
Rules: ((:REWRITE MEMP-DUP)
(:REWRITE MEMP-REV))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
COMPLICATED-MEMP-THEOREM
ACL2 >>(DEFUN LEAVES (X)
(IF (CONSP X)
(APP (LEAVES (CAR X)) (LEAVES (CDR X)))
(CONS X NIL)))
This event is redundant. See :DOC redundant-events.
Summary
Form: ( DEFUN LEAVES ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT
ACL2 >>(DEFTHM LEAVES-SWAPTREE
(EQUAL (LEAVES (SWAPTREE X))
(REV (LEAVES 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 (LEAVES X). This
suggestion was produced using the :induction rules LEAVES and SWAPTREE.
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 (CAR X))
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(EQUAL (LEAVES (SWAPTREE X))
(REV (LEAVES X)))).
But simplification reduces this to T, using the :definitions APP, LEAVES,
REV and SWAPTREE, the :executable-counterparts of CONSP and REV, primitive
type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(EQUAL (LEAVES (SWAPTREE (CAR X)))
(REV (LEAVES (CAR X))))
(EQUAL (LEAVES (SWAPTREE (CDR X)))
(REV (LEAVES (CDR X)))))
(EQUAL (LEAVES (SWAPTREE X))
(REV (LEAVES X)))).
But simplification reduces this to T, using the :definitions LEAVES
and SWAPTREE, primitive type reasoning and the :rewrite rules CAR-CONS,
CDR-CONS and REV-APP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM LEAVES-SWAPTREE ...)
Rules: ((:DEFINITION APP)
(:DEFINITION LEAVES)
(:DEFINITION REV)
(:DEFINITION SWAPTREE)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART REV)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEAVES)
(:INDUCTION SWAPTREE)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE REV-APP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEAVES-SWAPTREE
ACL2 >>(DEFTHM SUBP-CDR
(IMPLIES (SUBP X (CDR Y)) (SUBP X 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 two goals.
Subgoal 2
(IMPLIES (AND (NOT (CONSP Y)) (SUBP X (CDR Y)))
(SUBP X Y)).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, the :executable-counterpart of CONSP and the :rewrite rule DEFAULT-
CDR.
Subgoal 1
(IMPLIES (AND (CONSP (CONS Y1 Y2)) (SUBP X Y2))
(SUBP X (CONS Y1 Y2))).
This simplifies, using primitive type reasoning, to
Subgoal 1'
(IMPLIES (SUBP X Y2)
(SUBP X (CONS Y1 Y2))).
Normally we would attempt to prove this formula 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. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (SUBP X Y). This
suggestion was produced using the :induction rule SUBP. 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) (NOT (MEMP (CAR X) Y)))
(:P X Y))
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Y)
(:P (CDR X) Y))
(:P X Y))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP X))
(IMPLIES (SUBP X (CDR Y)) (SUBP X Y))).
By case analysis we reduce the conjecture to
Subgoal *1/3'
(IMPLIES (AND (NOT (CONSP X)) (SUBP X (CDR Y)))
(SUBP X Y)).
But simplification reduces this to T, using the :definition SUBP.
Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) Y)))
(IMPLIES (SUBP X (CDR Y)) (SUBP X Y))).
By case analysis we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP X)
(NOT (MEMP (CAR X) Y))
(SUBP X (CDR Y)))
(SUBP X Y)).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, the :executable-counterpart of CONSP and the :rewrite rule DEFAULT-
CDR.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Y)
(IMPLIES (SUBP (CDR X) (CDR Y))
(SUBP (CDR X) Y)))
(IMPLIES (SUBP X (CDR Y)) (SUBP X Y))).
By case analysis we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Y)
(IMPLIES (SUBP (CDR X) (CDR Y))
(SUBP (CDR X) Y))
(SUBP X (CDR Y)))
(SUBP X Y)).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning and the :type-prescription rules MEMP
and SUBP.
That completes the proof of *1.
Q.E.D.
The storage of SUBP-CDR depends upon the :type-prescription rule SUBP.
Summary
Form: ( DEFTHM SUBP-CDR ...)
Rules: ((:DEFINITION MEMP)
(:DEFINITION NOT)
(:DEFINITION SUBP)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION SUBP)
(:REWRITE DEFAULT-CDR)
(:TYPE-PRESCRIPTION MEMP)
(:TYPE-PRESCRIPTION SUBP))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
SUBP-CDR
ACL2 >>(DEFTHM SUBP-REFLEXIVE (SUBP X 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 (SUBP X X). This
suggestion was produced using the :induction rule SUBP. 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) (NOT (MEMP (CAR X) X)))
(:P X))
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) X)
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP X)) (SUBP X X)).
But simplification reduces this to T, using the :definition SUBP, the
:executable-counterpart of CDR and the :rewrite rules DEFAULT-CDR and
SUBP-CDR.
Subgoal *1/2
(IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) X)))
(SUBP X X)).
But simplification reduces this to T, using the :definition MEMP and
primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) X)
(SUBP (CDR X) (CDR X)))
(SUBP X X)).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rule SUBP-CDR and the
:type-prescription rule SUBP.
That completes the proof of *1.
Q.E.D.
The storage of SUBP-REFLEXIVE depends upon the :type-prescription rule
SUBP.
Summary
Form: ( DEFTHM SUBP-REFLEXIVE ...)
Rules: ((:DEFINITION MEMP)
(:DEFINITION SUBP)
(:EXECUTABLE-COUNTERPART CDR)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION SUBP)
(:REWRITE DEFAULT-CDR)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION SUBP))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
SUBP-REFLEXIVE
ACL2 >>(DEFTHM SUBP-INT
(IMPLIES (AND (PROPERP X) (SUBP X Y))
(EQUAL (INT X Y) X)))
[SGC for 439 CONS pages..(8013 writable)..(T=1).GC finished]
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 one.
We will induct according to a scheme suggested by (INT X Y). This
suggestion was produced using the :induction rules INT, PROPERP and
SUBP. 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)
(NOT (MEMP (CAR X) Y))
(:P (CDR X) Y))
(:P X Y))
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Y)
(:P (CDR X) Y))
(:P X Y))).
This induction is justified by the same argument used to admit INT,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following seven nontautological subgoals.
Subgoal *1/7
(IMPLIES (AND (NOT (CONSP X))
(PROPERP X)
(SUBP X Y))
(EQUAL (INT X Y) X)).
But simplification reduces this to T, using the :definitions INT, PROPERP
and SUBP, the :executable-counterparts of CONSP and EQUAL, primitive
type reasoning and the :rewrite rule SUBP-CDR.
Subgoal *1/6
(IMPLIES (AND (CONSP X)
(NOT (MEMP (CAR X) Y))
(EQUAL (INT (CDR X) Y) (CDR X))
(PROPERP X)
(SUBP X Y))
(EQUAL (INT X Y) X)).
But simplification reduces this to T, using the :definitions PROPERP
and SUBP.
Subgoal *1/5
(IMPLIES (AND (CONSP X)
(NOT (MEMP (CAR X) Y))
(NOT (SUBP (CDR X) Y))
(PROPERP X)
(SUBP X Y))
(EQUAL (INT X Y) X)).
But simplification reduces this to T, using the :definitions PROPERP
and SUBP.
Subgoal *1/4
(IMPLIES (AND (CONSP X)
(NOT (MEMP (CAR X) Y))
(NOT (PROPERP (CDR X)))
(PROPERP X)
(SUBP X Y))
(EQUAL (INT X Y) X)).
But simplification reduces this to T, using the :definition PROPERP.
Subgoal *1/3
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Y)
(EQUAL (INT (CDR X) Y) (CDR X))
(PROPERP X)
(SUBP X Y))
(EQUAL (INT X Y) X)).
But simplification reduces this to T, using the :definitions INT, PROPERP
and SUBP, primitive type reasoning, the :rewrite rule CAR-CDR-ELIM
and the :type-prescription rule MEMP.
Subgoal *1/2
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Y)
(NOT (SUBP (CDR X) Y))
(PROPERP X)
(SUBP X Y))
(EQUAL (INT X Y) X)).
But simplification reduces this to T, using the :definitions PROPERP
and SUBP and the :type-prescription rule MEMP.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Y)
(NOT (PROPERP (CDR X)))
(PROPERP X)
(SUBP X Y))
(EQUAL (INT X Y) X)).
But simplification reduces this to T, using the :definition PROPERP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM SUBP-INT ...)
Rules: ((:DEFINITION INT)
(:DEFINITION PROPERP)
(:DEFINITION SUBP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION INT)
(:INDUCTION PROPERP)
(:INDUCTION SUBP)
(:REWRITE CAR-CDR-ELIM)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION MEMP))
Warnings: None
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
SUBP-INT
ACL2 >>(DEFTHM INT-X-X
(IMPLIES (PROPERP X)
(EQUAL (INT X X) X)))
But simplification reduces this to T, using primitive type reasoning,
the :rewrite rules SUBP-INT and SUBP-REFLEXIVE and the :type-prescription
rule PROPERP.
Q.E.D.
Summary
Form: ( DEFTHM INT-X-X ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE SUBP-INT)
(:REWRITE SUBP-REFLEXIVE)
(:TYPE-PRESCRIPTION PROPERP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
INT-X-X
ACL2 >>(DEFTHM MEMP-SUBP
(IMPLIES (AND (SUBP Y Z) (MEMP E Y))
(MEMP E Z)))
ACL2 Warning [Free] in ( DEFTHM MEMP-SUBP ...): The :REWRITE rule
generated from MEMP-SUBP contains the free variable Y. This variable
will be chosen by searching for an instance of (SUBP Y Z) among the
hypotheses of the conjecture being rewritten. This is generally a
severe restriction on the applicability of the :REWRITE rule. See
:DOC free-variables.
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (MEMP E Y), but modified
to accommodate (SUBP Y Z). These suggestions were produced using the
:induction rules MEMP and SUBP. If we let (:P E Y Z) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP Y)) (:P E Y Z))
(IMPLIES (AND (CONSP Y)
(NOT (EQUAL E (CAR Y)))
(:P E (CDR Y) Z))
(:P E Y Z))
(IMPLIES (AND (CONSP Y) (EQUAL E (CAR Y)))
(:P E Y Z))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT Y) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.
Subgoal *1/4
(IMPLIES (AND (NOT (CONSP Y))
(SUBP Y Z)
(MEMP E Y))
(MEMP E Z)).
But simplification reduces this to T, using the :definitions MEMP and
SUBP and the :rewrite rule SUBP-CDR.
Subgoal *1/3
(IMPLIES (AND (CONSP Y)
(NOT (EQUAL E (CAR Y)))
(NOT (MEMP E (CDR Y)))
(SUBP Y Z)
(MEMP E Y))
(MEMP E Z)).
But simplification reduces this to T, using the :definitions MEMP and
SUBP and primitive type reasoning.
Subgoal *1/2
(IMPLIES (AND (CONSP Y)
(NOT (EQUAL E (CAR Y)))
(NOT (SUBP (CDR Y) Z))
(SUBP Y Z)
(MEMP E Y))
(MEMP E Z)).
But simplification reduces this to T, using the :definition SUBP.
Subgoal *1/1
(IMPLIES (AND (CONSP Y)
(EQUAL E (CAR Y))
(SUBP Y Z)
(MEMP E Y))
(MEMP E Z)).
But simplification reduces this to T, using the :definition SUBP.
That completes the proof of *1.
Q.E.D.
The storage of MEMP-SUBP depends upon the :type-prescription rule MEMP.
Summary
Form: ( DEFTHM MEMP-SUBP ...)
Rules: ((:DEFINITION MEMP)
(:DEFINITION SUBP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MEMP)
(:INDUCTION SUBP)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION MEMP))
Warnings: Free
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
MEMP-SUBP
ACL2 >>(DEFTHM SUBP-TRANSITIVE
(IMPLIES (AND (SUBP X Y) (SUBP Y Z))
(SUBP X Z)))
ACL2 Warning [Free] in ( DEFTHM SUBP-TRANSITIVE ...): The :REWRITE
rule generated from SUBP-TRANSITIVE contains the free variable Y.
This variable will be chosen by searching for an instance of (SUBP X Y)
among the hypotheses of the conjecture being rewritten. This is generally
a severe restriction on the applicability of the :REWRITE rule. See
:DOC free-variables.
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (SUBP X Z), but modified
to accommodate (SUBP X Y). These suggestions were produced using the
:induction rule SUBP. If we let (:P X Y Z) denote *1 above then the
induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P X Y Z))
(IMPLIES (AND (CONSP X) (NOT (MEMP (CAR X) Z)))
(:P X Y Z))
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Z)
(:P (CDR X) Y Z))
(:P X Y Z))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.
Subgoal *1/4
(IMPLIES (AND (NOT (CONSP X))
(SUBP X Y)
(SUBP Y Z))
(SUBP X Z)).
But simplification reduces this to T, using the :definition SUBP and
the :rewrite rule SUBP-CDR.
Subgoal *1/3
(IMPLIES (AND (CONSP X)
(NOT (MEMP (CAR X) Z))
(SUBP X Y)
(SUBP Y Z))
(SUBP X Z)).
This simplifies, using the :definition SUBP, the :rewrite rule MEMP-
SUBP and the :type-prescription rules MEMP and SUBP, to
Subgoal *1/3'
(IMPLIES (AND (CONSP X)
(NOT (MEMP (CAR X) Z))
(MEMP (CAR X) Y)
(SUBP (CDR X) Y)
(SUBP Y Z))
(SUBP (CDR X) Z)).
But simplification reduces this to T, using the :rewrite rule MEMP-
SUBP and the :type-prescription rules MEMP and SUBP.
Subgoal *1/2
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Z)
(SUBP (CDR X) Z)
(SUBP X Y)
(SUBP Y Z))
(SUBP X Z)).
But simplification reduces this to T, using the :definition SUBP, the
:rewrite rule MEMP-SUBP and the :type-prescription rules MEMP and SUBP.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(MEMP (CAR X) Z)
(NOT (SUBP (CDR X) Y))
(SUBP X Y)
(SUBP Y Z))
(SUBP X Z)).
But simplification reduces this to T, using the :definition SUBP.
That completes the proof of *1.
Q.E.D.
The storage of SUBP-TRANSITIVE depends upon the :type-prescription
rule SUBP.
Summary
Form: ( DEFTHM SUBP-TRANSITIVE ...)
Rules: ((:DEFINITION SUBP)
(:INDUCTION SUBP)
(:REWRITE MEMP-SUBP)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION MEMP)
(:TYPE-PRESCRIPTION SUBP))
Warnings: Free
Time: 0.02 seconds (prove: 0.02, print: 0.00, other: 0.00)
SUBP-TRANSITIVE
ACL2 >>(DEFTHM SUBP-APP-1
(EQUAL (SUBP (APP A B) C)
(AND (SUBP A C) (SUBP B C))))
This simplifies, using trivial observations, to the following two conjectures.
Subgoal 2
(IMPLIES (SUBP A C)
(EQUAL (SUBP (APP A B) C) (SUBP B C))).
Name the formula above *1.
Subgoal 1
(IMPLIES (NOT (SUBP A C))
(EQUAL (SUBP (APP A B) C) NIL)).
This simplifies, using primitive type reasoning, to
Subgoal 1'
(IMPLIES (NOT (SUBP A C))
(NOT (SUBP (APP A B) C))).
Normally we would attempt to prove this formula 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. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (SUBP A C), but modified
to accommodate (APP A B). These suggestions were produced using the
:induction rules APP and SUBP. If we let (:P A B C) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
(IMPLIES (AND (CONSP A) (NOT (MEMP (CAR A) C)))
(:P A B C))
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) C)
(:P (CDR A) B C))
(:P A B C))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP A))
(EQUAL (SUBP (APP A B) C)
(AND (SUBP A C) (SUBP B C)))).
But simplification reduces this to T, using the :definitions APP and
SUBP, primitive type reasoning and the :rewrite rule SUBP-CDR.
Subgoal *1/2
(IMPLIES (AND (CONSP A) (NOT (MEMP (CAR A) C)))
(EQUAL (SUBP (APP A B) C)
(AND (SUBP A C) (SUBP B C)))).
But simplification reduces this to T, using the :definitions APP and
SUBP, the :executable-counterpart of EQUAL, primitive type reasoning
and the :rewrite rule CAR-CONS.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) C)
(EQUAL (SUBP (APP (CDR A) B) C)
(AND (SUBP (CDR A) C) (SUBP B C))))
(EQUAL (SUBP (APP A B) C)
(AND (SUBP A C) (SUBP B C)))).
But simplification reduces this to T, using the :definitions APP and
SUBP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rules MEMP and SUBP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM SUBP-APP-1 ...)
Rules: ((:DEFINITION APP)
(:DEFINITION SUBP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:INDUCTION SUBP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION MEMP)
(:TYPE-PRESCRIPTION SUBP))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBP-APP-1
ACL2 >>(DEFTHM SUBP-APP-A-A (SUBP (APP A A) A))
ACL2 Warning [Subsume] in ( DEFTHM SUBP-APP-A-A ...): The previously
added rule SUBP-APP-1 subsumes the newly proposed :REWRITE rule SUBP-
APP-A-A, in the sense that the old rule rewrites a more general target.
Because the new rule will be tried first, it may nonetheless find application.
But we reduce the conjecture to T, by the :executable-counterpart of
IF and the simple :rewrite rules SUBP-APP-1 and SUBP-REFLEXIVE.
Q.E.D.
The storage of SUBP-APP-A-A depends upon the :type-prescription rule
SUBP.
Summary
Form: ( DEFTHM SUBP-APP-A-A ...)
Rules: ((:EXECUTABLE-COUNTERPART IF)
(:REWRITE SUBP-APP-1)
(:REWRITE SUBP-REFLEXIVE)
(:TYPE-PRESCRIPTION SUBP))
Warnings: Subsume
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SUBP-APP-A-A
ACL2 >>(DEFUN SETEQP (X Y)
(AND (SUBP X Y) (SUBP Y X)))
Since SETEQP is non-recursive, its admission is trivial. We observe
that the type of SETEQP is described by the theorem
(OR (EQUAL (SETEQP X Y) T) (EQUAL (SETEQP X Y) NIL)). We used the
:type-prescription rule SUBP.
Summary
Form: ( DEFUN SETEQP ...)
Rules: ((:TYPE-PRESCRIPTION SUBP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
SETEQP
ACL2 >>(DEFTHM SUBP-APP-2
(IMPLIES (SUBP A B) (SUBP A (APP B C))))
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (SUBP A (APP B C)),
but modified to accommodate (SUBP A B). These suggestions were produced
using the :induction rule SUBP. If we let (:P A B C) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
(IMPLIES (AND (CONSP A)
(NOT (MEMP (CAR A) (APP B C))))
(:P A B C))
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) (APP B C))
(:P (CDR A) B C))
(:P A B C))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.
Subgoal *1/4
(IMPLIES (AND (NOT (CONSP A)) (SUBP A B))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definition SUBP and
the :rewrite rule SUBP-CDR.
Subgoal *1/3
(IMPLIES (AND (CONSP A)
(NOT (MEMP (CAR A) (APP B C)))
(SUBP A B))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules MEMP-APP and MEMP-SUBP and the :type-
prescription rule SUBP.
Subgoal *1/2
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) (APP B C))
(SUBP (CDR A) (APP B C))
(SUBP A B))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rules MEMP and SUBP.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) (APP B C))
(NOT (SUBP (CDR A) B))
(SUBP A B))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rule SUBP.
That completes the proof of *1.
Q.E.D.
The storage of SUBP-APP-2 depends upon the :type-prescription rule
SUBP.
Summary
Form: ( DEFTHM SUBP-APP-2 ...)
Rules: ((:DEFINITION MEMP)
(:DEFINITION SUBP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION SUBP)
(:REWRITE MEMP-APP)
(:REWRITE MEMP-SUBP)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION MEMP)
(:TYPE-PRESCRIPTION SUBP))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBP-APP-2
ACL2 >>(DEFTHM SETEQ-REV (SETEQP (REV A) A))
ACL2 Warning [Non-rec] in ( DEFTHM SETEQ-REV ...): The :REWRITE rule
generated from SETEQ-REV will be triggered only by terms containing
the non-recursive function symbol SETEQP. Unless this function is
disabled, SETEQ-REV is unlikely ever to be used.
By the simple :definition SETEQP we reduce the conjecture to the following
two conjectures.
Subgoal 2
(SUBP (REV A) A).
Name the formula above *1.
Subgoal 1
(SUBP A (REV A)).
Normally we would attempt to prove this formula 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. One induction scheme is suggested
by this conjecture.
We will induct according to a scheme suggested by (REV A). This suggestion
was produced using the :induction rule REV. If we let (:P A) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A))
(IMPLIES (AND (CONSP A) (:P (CDR A)))
(:P A))).
This induction is justified by the same argument used to admit REV,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(SETEQP (REV A) A)).
But simplification reduces this to T, using the :definitions REV, SETEQP
and SUBP, the :executable-counterparts of CDR and SUBP and the :rewrite
rules DEFAULT-CDR and SUBP-CDR.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(SETEQP (REV (CDR A)) (CDR A)))
(SETEQP (REV A) A)).
By the simple :definition SETEQP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (AND (CONSP A)
(SUBP (REV (CDR A)) (CDR A))
(SUBP (CDR A) (REV (CDR A))))
(SETEQP (REV A) A)).
[SGC for 439 CONS pages..(8014 writable)..(T=1).GC finished]
But simplification reduces this to T, using the :definitions MEMP,
REV, SETEQP and SUBP, the :executable-counterpart of CONSP, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS, MEMP-APP, MEMP-
REV, SUBP-APP-1, SUBP-APP-2 and SUBP-CDR and the :type-prescription
rule SUBP.
That completes the proof of *1.
Q.E.D.
The storage of SETEQ-REV depends upon the :type-prescription rule SETEQP.
Summary
Form: ( DEFTHM SETEQ-REV ...)
Rules: ((:DEFINITION MEMP)
(:DEFINITION NOT)
(:DEFINITION REV)
(:DEFINITION SETEQP)
(:DEFINITION SUBP)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART SUBP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION REV)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE DEFAULT-CDR)
(:REWRITE MEMP-APP)
(:REWRITE MEMP-REV)
(:REWRITE SUBP-APP-1)
(:REWRITE SUBP-APP-2)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION SETEQP)
(:TYPE-PRESCRIPTION SUBP))
Warnings: Non-rec
Time: 0.02 seconds (prove: 0.01, print: 0.01, other: 0.00)
SETEQ-REV
ACL2 >>(DEFTHM SUBP-APP-3
(IMPLIES (SUBP A C) (SUBP A (APP B C))))
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. 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 (SUBP A (APP B C)),
but modified to accommodate (SUBP A C). These suggestions were produced
using the :induction rule SUBP. If we let (:P A B C) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
(IMPLIES (AND (CONSP A)
(NOT (MEMP (CAR A) (APP B C))))
(:P A B C))
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) (APP B C))
(:P (CDR A) B C))
(:P A B C))).
This induction is justified by the same argument used to admit SUBP,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.
Subgoal *1/4
(IMPLIES (AND (NOT (CONSP A)) (SUBP A C))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definition SUBP and
the :rewrite rules SUBP-APP-2 and SUBP-CDR.
Subgoal *1/3
(IMPLIES (AND (CONSP A)
(NOT (MEMP (CAR A) (APP B C)))
(SUBP A C))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules MEMP-APP and MEMP-SUBP and the :type-
prescription rule SUBP.
Subgoal *1/2
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) (APP B C))
(SUBP (CDR A) (APP B C))
(SUBP A C))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rules MEMP and SUBP.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(MEMP (CAR A) (APP B C))
(NOT (SUBP (CDR A) C))
(SUBP A C))
(SUBP A (APP B C))).
But simplification reduces this to T, using the :definitions MEMP and
SUBP, primitive type reasoning, the :rewrite rules MEMP-APP and MEMP-
SUBP and the :type-prescription rule SUBP.
That completes the proof of *1.
Q.E.D.
The storage of SUBP-APP-3 depends upon the :type-prescription rule
SUBP.
Summary
Form: ( DEFTHM SUBP-APP-3 ...)
Rules: ((:DEFINITION MEMP)
(:DEFINITION SUBP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION SUBP)
(:REWRITE MEMP-APP)
(:REWRITE MEMP-SUBP)
(:REWRITE SUBP-APP-2)
(:REWRITE SUBP-CDR)
(:TYPE-PRESCRIPTION MEMP)
(:TYPE-PRESCRIPTION SUBP))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
SUBP-APP-3
ACL2 >>(DEFTHM APP-COMMUTATIVE
(SETEQP (APP A B) (APP B A)))
ACL2 Warning [Non-rec] in ( DEFTHM APP-COMMUTATIVE ...): The :REWRITE
rule generated from APP-COMMUTATIVE will be triggered only by terms
containing the non-recursive function symbol SETEQP. Unless this function
is disabled, APP-COMMUTATIVE is unlikely ever to be used.
By the simple :definition SETEQP and the simple :rewrite rule SUBP-
APP-1 we reduce the conjecture to the following four conjectures.
Subgoal 4
(SUBP A (APP B A)).
But simplification reduces this to T, using the :rewrite rules SUBP-
APP-3 and SUBP-REFLEXIVE.
Subgoal 3
(SUBP B (APP B A)).
But simplification reduces this to T, using the :rewrite rules SUBP-
APP-2 and SUBP-REFLEXIVE.
Subgoal 2
(SUBP B (APP A B)).
But simplification reduces this to T, using the :rewrite rules SUBP-
APP-3 and SUBP-REFLEXIVE.
Subgoal 1
(SUBP A (APP A B)).
But simplification reduces this to T, using the :rewrite rules SUBP-
APP-2 and SUBP-REFLEXIVE.
Q.E.D.
The storage of APP-COMMUTATIVE depends upon the :type-prescription
rule SETEQP.
Summary
Form: ( DEFTHM APP-COMMUTATIVE ...)
Rules: ((:DEFINITION SETEQP)
(:REWRITE SUBP-APP-1)
(:REWRITE SUBP-APP-2)
(:REWRITE SUBP-APP-3)
(:REWRITE SUBP-REFLEXIVE)
(:TYPE-PRESCRIPTION SETEQP))
Warnings: Non-rec
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
APP-COMMUTATIVE
ACL2 >>(DEFUN LIST-OF-ATOMSP (X)
(IF (CONSP X)
(AND (NOT (CONSP (CAR X)))
(LIST-OF-ATOMSP (CDR X)))
T))
The admission of LIST-OF-ATOMSP 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 LIST-OF-ATOMSP
is described by the theorem
(OR (EQUAL (LIST-OF-ATOMSP X) T) (EQUAL (LIST-OF-ATOMSP X) NIL)).
Summary
Form: ( DEFUN LIST-OF-ATOMSP ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LIST-OF-ATOMSP
ACL2 >>(DEFTHM LIST-OF-ATOMSP-APP
(EQUAL (LIST-OF-ATOMSP (APP A B))
(AND (LIST-OF-ATOMSP A)
(LIST-OF-ATOMSP B))))
This simplifies, using trivial observations, to the following two conjectures.
Subgoal 2
(IMPLIES (LIST-OF-ATOMSP A)
(EQUAL (LIST-OF-ATOMSP (APP A B))
(LIST-OF-ATOMSP B))).
Name the formula above *1.
Subgoal 1
(IMPLIES (NOT (LIST-OF-ATOMSP A))
(EQUAL (LIST-OF-ATOMSP (APP A B)) NIL)).
This simplifies, using primitive type reasoning, to
Subgoal 1'
(IMPLIES (NOT (LIST-OF-ATOMSP A))
(NOT (LIST-OF-ATOMSP (APP A B)))).
Normally we would attempt to prove this formula 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. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (LIST-OF-ATOMSP A),
but modified to accommodate (APP A B). These suggestions were produced
using the :induction rules APP and LIST-OF-ATOMSP. If we let (:P A B)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B))
(IMPLIES (AND (CONSP A) (CONSP (CAR A)))
(:P A B))
(IMPLIES (AND (CONSP A)
(NOT (CONSP (CAR A)))
(:P (CDR A) B))
(:P A B))).
This induction is justified by the same argument used to admit LIST-
OF-ATOMSP, namely, the measure (ACL2-COUNT A) is decreasing according
to the relation O< (which is known to be well-founded on the domain
recognized by O-P). When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP A))
(EQUAL (LIST-OF-ATOMSP (APP A B))
(AND (LIST-OF-ATOMSP A)
(LIST-OF-ATOMSP B)))).
But simplification reduces this to T, using the :definitions APP and
LIST-OF-ATOMSP and primitive type reasoning.
Subgoal *1/2
(IMPLIES (AND (CONSP A) (CONSP (CAR A)))
(EQUAL (LIST-OF-ATOMSP (APP A B))
(AND (LIST-OF-ATOMSP A)
(LIST-OF-ATOMSP B)))).
But simplification reduces this to T, using the :definitions APP and
LIST-OF-ATOMSP, the :executable-counterpart of EQUAL, primitive type
reasoning and the :rewrite rule CAR-CONS.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(NOT (CONSP (CAR A)))
(EQUAL (LIST-OF-ATOMSP (APP (CDR A) B))
(AND (LIST-OF-ATOMSP (CDR A))
(LIST-OF-ATOMSP B))))
(EQUAL (LIST-OF-ATOMSP (APP A B))
(AND (LIST-OF-ATOMSP A)
(LIST-OF-ATOMSP B)))).
But simplification reduces this to T, using the :definitions APP and
LIST-OF-ATOMSP, the :executable-counterpart of EQUAL, primitive type
reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rule LIST-OF-ATOMSP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM LIST-OF-ATOMSP-APP ...)
Rules: ((:DEFINITION APP)
(:DEFINITION LIST-OF-ATOMSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:INDUCTION LIST-OF-ATOMSP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION LIST-OF-ATOMSP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LIST-OF-ATOMSP-APP
ACL2 >>(DEFTHM LIST-OF-ATOMSP-LEAVES
(LIST-OF-ATOMSP (LEAVES 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 (LEAVES X). This
suggestion was produced using the :induction rule LEAVES. 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 (CAR X))
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(LIST-OF-ATOMSP (LEAVES X))).
But simplification reduces this to T, using the :definitions LEAVES
and LIST-OF-ATOMSP, the :executable-counterpart of LIST-OF-ATOMSP,
primitive type reasoning and the :rewrite rules CAR-CONS and CDR-CONS.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(LIST-OF-ATOMSP (LEAVES (CAR X)))
(LIST-OF-ATOMSP (LEAVES (CDR X))))
(LIST-OF-ATOMSP (LEAVES X))).
But simplification reduces this to T, using the :definition LEAVES,
the :rewrite rule LIST-OF-ATOMSP-APP and the :type-prescription rule
LIST-OF-ATOMSP.
That completes the proof of *1.
Q.E.D.
The storage of LIST-OF-ATOMSP-LEAVES depends upon the :type-prescription
rule LIST-OF-ATOMSP.
Summary
Form: ( DEFTHM LIST-OF-ATOMSP-LEAVES ...)
Rules: ((:DEFINITION LEAVES)
(:DEFINITION LIST-OF-ATOMSP)
(:EXECUTABLE-COUNTERPART LIST-OF-ATOMSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEAVES)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE LIST-OF-ATOMSP-APP)
(:TYPE-PRESCRIPTION LIST-OF-ATOMSP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LIST-OF-ATOMSP-LEAVES
ACL2 >>(DEFTHM LEAVES-OF-LIST-OF-ATOMS
(IMPLIES (AND (PROPERP X) (LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))))
Name the formula above *1.
Perhaps we can prove *1 by induction. Four 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 (LEAVES X). This
suggestion was produced using the :induction rules APP, LEAVES, LIST-
OF-ATOMSP and PROPERP. 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 (CAR X))
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following ten nontautological subgoals.
Subgoal *1/10
(IMPLIES (AND (NOT (CONSP X))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
But simplification reduces this to T, using the :definition PROPERP,
the :executable-counterparts of APP, CONSP, EQUAL, LEAVES, LIST-OF-
ATOMSP and NOT and primitive type reasoning.
Subgoal *1/9
(IMPLIES (AND (CONSP X)
(EQUAL (LEAVES (CAR X))
(APP (CAR X) '(NIL)))
(EQUAL (LEAVES (CDR X))
(APP (CDR X) '(NIL)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
This simplifies, using the :definitions APP, LEAVES, LIST-OF-ATOMSP
and PROPERP and primitive type reasoning, to
Subgoal *1/9'
(IMPLIES (AND (CONSP X)
(EQUAL (LEAVES (CAR X))
(APP (CAR X) '(NIL)))
(EQUAL (LEAVES (CDR X))
(APP (CDR X) '(NIL)))
(PROPERP (CDR X))
(NOT (CONSP (CAR X)))
(LIST-OF-ATOMSP (CDR X)))
(EQUAL (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
(CONS (CAR X) (LEAVES (CDR X))))).
But simplification reduces this to T, using the :definitions APP and
LEAVES, the :executable-counterparts of CAR, CDR, CONSP, EQUAL and
LEAVES, primitive type reasoning and the :rewrite rule CONS-EQUAL.
Subgoal *1/8
(IMPLIES (AND (CONSP X)
(NOT (LIST-OF-ATOMSP (CAR X)))
(EQUAL (LEAVES (CDR X))
(APP (CDR X) '(NIL)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
This simplifies, using the :definitions APP, LEAVES, LIST-OF-ATOMSP
and PROPERP and primitive type reasoning, to
Subgoal *1/8'
(IMPLIES (AND (CONSP X)
(NOT (LIST-OF-ATOMSP (CAR X)))
(EQUAL (LEAVES (CDR X))
(APP (CDR X) '(NIL)))
(PROPERP (CDR X))
(NOT (CONSP (CAR X)))
(LIST-OF-ATOMSP (CDR X)))
(EQUAL (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
(CONS (CAR X) (LEAVES (CDR X))))).
But simplification reduces this to T, using the :definition LIST-OF-
ATOMSP.
Subgoal *1/7
(IMPLIES (AND (CONSP X)
(NOT (PROPERP (CAR X)))
(EQUAL (LEAVES (CDR X))
(APP (CDR X) '(NIL)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
This simplifies, using the :definitions APP, LEAVES, LIST-OF-ATOMSP
and PROPERP and primitive type reasoning, to
Subgoal *1/7'
(IMPLIES (AND (CONSP X)
(NOT (PROPERP (CAR X)))
(EQUAL (LEAVES (CDR X))
(APP (CDR X) '(NIL)))
(PROPERP (CDR X))
(NOT (CONSP (CAR X)))
(LIST-OF-ATOMSP (CDR X)))
(EQUAL (APP (LEAVES (CAR X)) (LEAVES (CDR X)))
(CONS (CAR X) (LEAVES (CDR X))))).
But simplification reduces this to T, using the :definitions APP, LEAVES
and PROPERP, the :executable-counterpart of CONSP, primitive type reasoning
and the :rewrite rules CAR-CONS and CDR-CONS.
Subgoal *1/6
(IMPLIES (AND (CONSP X)
(EQUAL (LEAVES (CAR X))
(APP (CAR X) '(NIL)))
(NOT (LIST-OF-ATOMSP (CDR X)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
But simplification reduces this to T, using the :definitions LIST-OF-
ATOMSP and PROPERP.
Subgoal *1/5
(IMPLIES (AND (CONSP X)
(NOT (LIST-OF-ATOMSP (CAR X)))
(NOT (LIST-OF-ATOMSP (CDR X)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
But simplification reduces this to T, using the :definitions LIST-OF-
ATOMSP and PROPERP.
Subgoal *1/4
(IMPLIES (AND (CONSP X)
(NOT (PROPERP (CAR X)))
(NOT (LIST-OF-ATOMSP (CDR X)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
But simplification reduces this to T, using the :definitions LIST-OF-
ATOMSP and PROPERP.
Subgoal *1/3
(IMPLIES (AND (CONSP X)
(EQUAL (LEAVES (CAR X))
(APP (CAR X) '(NIL)))
(NOT (PROPERP (CDR X)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
But simplification reduces this to T, using the :definition PROPERP.
Subgoal *1/2
(IMPLIES (AND (CONSP X)
(NOT (LIST-OF-ATOMSP (CAR X)))
(NOT (PROPERP (CDR X)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
But simplification reduces this to T, using the :definition PROPERP.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(NOT (PROPERP (CAR X)))
(NOT (PROPERP (CDR X)))
(PROPERP X)
(LIST-OF-ATOMSP X))
(EQUAL (LEAVES X) (APP X '(NIL)))).
But simplification reduces this to T, using the :definition PROPERP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM LEAVES-OF-LIST-OF-ATOMS ...)
Rules: ((:DEFINITION APP)
(:DEFINITION LEAVES)
(:DEFINITION LIST-OF-ATOMSP)
(:DEFINITION PROPERP)
(:EXECUTABLE-COUNTERPART APP)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART LEAVES)
(:EXECUTABLE-COUNTERPART LIST-OF-ATOMSP)
(:EXECUTABLE-COUNTERPART NOT)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION APP)
(:INDUCTION LEAVES)
(:INDUCTION LIST-OF-ATOMSP)
(:INDUCTION PROPERP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE CONS-EQUAL))
Warnings: None
Time: 0.03 seconds (prove: 0.01, print: 0.01, other: 0.01)
LEAVES-OF-LIST-OF-ATOMS
ACL2 >>(DEFTHM PROPERP-LEAVES (PROPERP (LEAVES 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 (LEAVES X). This
suggestion was produced using the :induction rule LEAVES. 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 (CAR X))
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit LEAVES,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(PROPERP (LEAVES X))).
But simplification reduces this to T, using the :definitions LEAVES
and PROPERP, the :executable-counterpart of PROPERP, primitive type
reasoning and the :rewrite rule CDR-CONS.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(PROPERP (LEAVES (CAR X)))
(PROPERP (LEAVES (CDR X))))
(PROPERP (LEAVES X))).
But simplification reduces this to T, using the :definition LEAVES,
the :rewrite rule PROPERP-APP and the :type-prescription rule PROPERP.
That completes the proof of *1.
Q.E.D.
The storage of PROPERP-LEAVES depends upon the :type-prescription rule
PROPERP.
Summary
Form: ( DEFTHM PROPERP-LEAVES ...)
Rules: ((:DEFINITION LEAVES)
(:DEFINITION PROPERP)
(:EXECUTABLE-COUNTERPART PROPERP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEAVES)
(:REWRITE CDR-CONS)
(:REWRITE PROPERP-APP)
(:TYPE-PRESCRIPTION PROPERP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
PROPERP-LEAVES
ACL2 >>(DEFTHM LEAVES-LEAVES
(EQUAL (LEAVES (LEAVES X))
(APP (LEAVES X) '(NIL))))
But simplification reduces this to T, using primitive type reasoning
and the :rewrite rules LEAVES-OF-LIST-OF-ATOMS, LIST-OF-ATOMSP-LEAVES
and PROPERP-LEAVES.
Q.E.D.
Summary
Form: ( DEFTHM LEAVES-LEAVES ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE LEAVES-OF-LIST-OF-ATOMS)
(:REWRITE LIST-OF-ATOMSP-LEAVES)
(:REWRITE PROPERP-LEAVES))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
LEAVES-LEAVES
ACL2 >>(DEFTHM LEMMA8-10A
(IMPLIES (NOT (MEM E LEAVES))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))))
Name the formula above *1.
Perhaps we can prove *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
(COLLECT-LONESOMEP LST LEAVES). This suggestion was produced using
the :induction rule COLLECT-LONESOMEP. If we let (:P E LEAVES LST)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP LST))
(:P E LEAVES LST))
(IMPLIES (AND (CONSP LST)
(NOT (LONESOMEP (CAR LST) LEAVES))
(:P E LEAVES (CDR LST)))
(:P E LEAVES LST))
(IMPLIES (AND (CONSP LST)
(LONESOMEP (CAR LST) LEAVES)
(:P E LEAVES (CDR LST)))
(:P E LEAVES LST))).
This induction is justified by the same argument used to admit COLLECT-
LONESOMEP, namely, the measure (ACL2-COUNT LST) is decreasing according
to the relation O< (which is known to be well-founded on the domain
recognized by O-P). When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (CONSP LST))
(NOT (MEM E LEAVES)))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and MEMP and the :executable-counterpart of CONSP.
Subgoal *1/2
(IMPLIES (AND (CONSP LST)
(NOT (LONESOMEP (CAR LST) LEAVES))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(NOT (MEM E LEAVES)))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and LONESOMEP and the :type-prescription rule MEM.
Subgoal *1/1
(IMPLIES (AND (CONSP LST)
(LONESOMEP (CAR LST) LEAVES)
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(NOT (MEM E LEAVES)))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
By the simple :definition LONESOMEP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (AND (CONSP LST)
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(NOT (MEM E LEAVES)))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rules COLLECT-LONESOMEP and MEM,
to
Subgoal *1/1''
(IMPLIES (AND (CONSP LST)
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(NOT (MEM E LEAVES)))
(NOT (EQUAL E (CAR LST)))).
But simplification reduces this to T, using trivial observations.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM LEMMA8-10A ...)
Rules: ((:DEFINITION COLLECT-LONESOMEP)
(:DEFINITION LONESOMEP)
(:DEFINITION MEMP)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COLLECT-LONESOMEP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION COLLECT-LONESOMEP)
(:TYPE-PRESCRIPTION MEM))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA8-10A
ACL2 >>(DEFTHM LEMMA8-10B
(IMPLIES (MEM E (CDR (MEM E LEAVES)))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))))
Name the formula above *1.
Perhaps we can prove *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
(COLLECT-LONESOMEP LST LEAVES). This suggestion was produced using
the :induction rule COLLECT-LONESOMEP. If we let (:P E LEAVES LST)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP LST))
(:P E LEAVES LST))
(IMPLIES (AND (CONSP LST)
(NOT (LONESOMEP (CAR LST) LEAVES))
(:P E LEAVES (CDR LST)))
(:P E LEAVES LST))
(IMPLIES (AND (CONSP LST)
(LONESOMEP (CAR LST) LEAVES)
(:P E LEAVES (CDR LST)))
(:P E LEAVES LST))).
This induction is justified by the same argument used to admit COLLECT-
LONESOMEP, namely, the measure (ACL2-COUNT LST) is decreasing according
to the relation O< (which is known to be well-founded on the domain
recognized by O-P). When applied to the goal at hand the above induction
scheme produces the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (CONSP LST))
(MEM E (CDR (MEM E LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
[SGC for 439 CONS pages..(8014 writable)..(T=1).GC finished]
But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and MEMP and the :executable-counterpart of CONSP.
Subgoal *1/2
(IMPLIES (AND (CONSP LST)
(NOT (LONESOMEP (CAR LST) LEAVES))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(MEM E (CDR (MEM E LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and LONESOMEP and the :type-prescription rule MEM.
Subgoal *1/1
(IMPLIES (AND (CONSP LST)
(LONESOMEP (CAR LST) LEAVES)
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(MEM E (CDR (MEM E LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
By the simple :definition LONESOMEP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (AND (CONSP LST)
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(MEM E (CDR (MEM E LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))).
This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rules COLLECT-LONESOMEP and MEM,
to
Subgoal *1/1''
(IMPLIES (AND (CONSP LST)
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES))))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(MEM E (CDR (MEM E LEAVES))))
(NOT (EQUAL E (CAR LST)))).
But simplification reduces this to T, using trivial observations.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM LEMMA8-10B ...)
Rules: ((:DEFINITION COLLECT-LONESOMEP)
(:DEFINITION LONESOMEP)
(:DEFINITION MEMP)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COLLECT-LONESOMEP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION COLLECT-LONESOMEP)
(:TYPE-PRESCRIPTION MEM))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
LEMMA8-10B
ACL2 >>(DEFTHM MEMP-COLLECT-LONESOMEP
(IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST)
(LONESOMEP E LEAVES))))
ACL2 Warning [Subsume] in ( DEFTHM MEMP-COLLECT-LONESOMEP ...): The
newly proposed :REWRITE rule MEMP-COLLECT-LONESOMEP probably subsumes
the previously added :REWRITE rules LEMMA8-10B and LEMMA8-10A, in the
sense that MEMP-COLLECT-LONESOMEP will now probably be applied whenever
the old rules would have been.
By case analysis we reduce the conjecture to
Goal'
(COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST) (LONESOMEP E LEAVES)))
((AND (MEMP E LST) (LONESOMEP E LEAVES))
NIL)
(T T)).
This simplifies, using the :definition LONESOMEP, to the following
four conjectures.
Subgoal 4
(IMPLIES (AND (NOT (MEMP E (COLLECT-LONESOMEP LST LEAVES)))
(MEMP E LST)
(MEM E LEAVES))
(MEM E (CDR (MEM E LEAVES)))).
Name the formula above *1.
Subgoal 3
(IMPLIES (MEMP E (COLLECT-LONESOMEP LST LEAVES))
(MEM E LEAVES)).
But simplification reduces this to T, using the :rewrite rule LEMMA8-
10A.
Subgoal 2
(IMPLIES (MEMP E (COLLECT-LONESOMEP LST LEAVES))
(MEMP E LST)).
Normally we would attempt to prove this formula 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. Two induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by (MEMP E LST), but
modified to accommodate (COLLECT-LONESOMEP LST LEAVES). These suggestions
were produced using the :induction rules COLLECT-LONESOMEP and MEMP.
If we let (:P E LEAVES LST) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (NOT (CONSP LST))
(:P E LEAVES LST))
(IMPLIES (AND (CONSP LST)
(NOT (EQUAL E (CAR LST)))
(:P E LEAVES (CDR LST)))
(:P E LEAVES LST))
(IMPLIES (AND (CONSP LST) (EQUAL E (CAR LST)))
(:P E LEAVES LST))).
This induction is justified by the same argument used to admit MEMP,
namely, the measure (ACL2-COUNT LST) is decreasing according to the
relation O< (which is known to be well-founded on the domain recognized
by O-P). When applied to the goal at hand the above induction scheme
produces the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (NOT (CONSP LST))
(IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST)
(LONESOMEP E LEAVES)))).
By case analysis we reduce the conjecture to
Subgoal *1/3'
(IMPLIES (NOT (CONSP LST))
(COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST) (LONESOMEP E LEAVES)))
((AND (MEMP E LST) (LONESOMEP E LEAVES))
NIL)
(T T))).
But simplification reduces this to T, using the :definitions COLLECT-
LONESOMEP and MEMP and the :executable-counterpart of CONSP.
Subgoal *1/2
(IMPLIES (AND (CONSP LST)
(NOT (EQUAL E (CAR LST)))
(IFF (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES))
(AND (MEMP E (CDR LST))
(LONESOMEP E LEAVES))))
(IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST)
(LONESOMEP E LEAVES)))).
By case analysis we reduce the conjecture to
Subgoal *1/2'
(IMPLIES (AND (CONSP LST)
(NOT (EQUAL E (CAR LST)))
(COND ((MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES))
(AND (MEMP E (CDR LST))
(LONESOMEP E LEAVES)))
((AND (MEMP E (CDR LST))
(LONESOMEP E LEAVES))
NIL)
(T T)))
(COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST) (LONESOMEP E LEAVES)))
((AND (MEMP E LST) (LONESOMEP E LEAVES))
NIL)
(T T))).
This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP, primitive type reasoning and the :type-prescription rules
MEM and MEMP, to the following four conjectures.
Subgoal *1/2.4
(IMPLIES (AND (CONSP LST)
(NOT (EQUAL E (CAR LST)))
(MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES))
(MEMP E (CDR LST))
(MEM E LEAVES)
(NOT (MEM E (CDR (MEM E LEAVES))))
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES)))))
(MEMP E
(CONS (CAR LST)
(COLLECT-LONESOMEP (CDR LST) LEAVES)))).
But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rules COLLECT-LONESOMEP and MEMP.
Subgoal *1/2.3
(IMPLIES (AND (CONSP LST)
(NOT (EQUAL E (CAR LST)))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(NOT (MEM E LEAVES))
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES)))))
(NOT (MEMP E
(CONS (CAR LST)
(COLLECT-LONESOMEP (CDR LST)
LEAVES))))).
But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and LEMMA8-10A
and the :type-prescription rule COLLECT-LONESOMEP.
Subgoal *1/2.2
(IMPLIES (AND (CONSP LST)
(NOT (EQUAL E (CAR LST)))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(NOT (MEMP E (CDR LST)))
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES)))))
(NOT (MEMP E
(CONS (CAR LST)
(COLLECT-LONESOMEP (CDR LST)
LEAVES))))).
But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rule COLLECT-LONESOMEP.
Subgoal *1/2.1
(IMPLIES (AND (CONSP LST)
(NOT (EQUAL E (CAR LST)))
(NOT (MEMP E (COLLECT-LONESOMEP (CDR LST) LEAVES)))
(MEM E (CDR (MEM E LEAVES)))
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES)))))
(NOT (MEMP E
(CONS (CAR LST)
(COLLECT-LONESOMEP (CDR LST)
LEAVES))))).
But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rules CAR-CONS, CDR-CONS and LEMMA8-10B
and the :type-prescription rules COLLECT-LONESOMEP and MEM.
Subgoal *1/1
(IMPLIES (AND (CONSP LST) (EQUAL E (CAR LST)))
(IFF (MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST)
(LONESOMEP E LEAVES)))).
By case analysis we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (AND (CONSP LST) (EQUAL E (CAR LST)))
(COND ((MEMP E (COLLECT-LONESOMEP LST LEAVES))
(AND (MEMP E LST) (LONESOMEP E LEAVES)))
((AND (MEMP E LST) (LONESOMEP E LEAVES))
NIL)
(T T))).
This simplifies, using the :definitions COLLECT-LONESOMEP, LONESOMEP
and MEMP and primitive type reasoning, to the following three conjectures.
Subgoal *1/1.3
(IMPLIES (AND (CONSP LST)
(NOT (MEM (CAR LST) LEAVES)))
(NOT (MEMP (CAR LST)
(COLLECT-LONESOMEP (CDR LST) LEAVES)))).
But simplification reduces this to T, using the :rewrite rule LEMMA8-
10A.
Subgoal *1/1.2
(IMPLIES (AND (CONSP LST)
(MEM (CAR LST) LEAVES)
(NOT (MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES)))))
(MEMP (CAR LST)
(CONS (CAR LST)
(COLLECT-LONESOMEP (CDR LST) LEAVES)))).
But simplification reduces this to T, using the :definition MEMP, primitive
type reasoning, the :rewrite rule CAR-CONS and the :type-prescription
rule COLLECT-LONESOMEP.
Subgoal *1/1.1
(IMPLIES (AND (CONSP LST)
(MEM (CAR LST)
(CDR (MEM (CAR LST) LEAVES))))
(NOT (MEMP (CAR LST)
(COLLECT-LONESOMEP (CDR LST) LEAVES)))).
But simplification reduces this to T, using the :rewrite rule LEMMA8-
10B and the :type-prescription rule MEM.
That completes the proof of *1.
Q.E.D.
The storage of MEMP-COLLECT-LONESOMEP depends upon the :type-prescription
rules LONESOMEP and MEMP.
Summary
Form: ( DEFTHM MEMP-COLLECT-LONESOMEP ...)
Rules: ((:DEFINITION COLLECT-LONESOMEP)
(:DEFINITION IFF)
(:DEFINITION LONESOMEP)
(:DEFINITION MEMP)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION COLLECT-LONESOMEP)
(:INDUCTION MEMP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE LEMMA8-10A)
(:REWRITE LEMMA8-10B)
(:TYPE-PRESCRIPTION COLLECT-LONESOMEP)
(:TYPE-PRESCRIPTION LONESOMEP)
(:TYPE-PRESCRIPTION MEM)
(:TYPE-PRESCRIPTION MEMP))
Warnings: Subsume
Time: 0.04 seconds (prove: 0.03, print: 0.01, other: 0.00)
MEMP-COLLECT-LONESOMEP
ACL2 >>(DEFTHM MEMP-LONESOMES
(IFF (MEMP E (LONESOMES X))
(AND (MEMP E (LEAVES X))
(LONESOMEP E (LEAVES X)))))
ACL2 Warning [Non-rec] in ( DEFTHM MEMP-LONESOMES ...): The :REWRITE
rule generated from MEMP-LONESOMES will be triggered only by terms
containing the non-recursive function symbol LONESOMES. Unless this
function is disabled, MEMP-LONESOMES is unlikely ever to be used.
By case analysis we reduce the conjecture to
Goal'
(COND ((MEMP E (LONESOMES X))
(AND (MEMP E (LEAVES X))
(LONESOMEP E (LEAVES X))))
((AND (MEMP E (LEAVES X))
(LONESOMEP E (LEAVES X)))
NIL)
(T T)).
But simplification reduces this to T, using the :definitions LONESOMEP
and LONESOMES, the :rewrite rule MEMP-COLLECT-LONESOMEP and the :type-
prescription rules MEM and MEMP.
Q.E.D.
The storage of MEMP-LONESOMES depends upon the :type-prescription rules
LONESOMEP and MEMP.
Summary
Form: ( DEFTHM MEMP-LONESOMES ...)
Rules: ((:DEFINITION IFF)
(:DEFINITION LONESOMEP)
(:DEFINITION LONESOMES)
(:REWRITE MEMP-COLLECT-LONESOMEP)
(:TYPE-PRESCRIPTION LONESOMEP)
(:TYPE-PRESCRIPTION MEM)
(:TYPE-PRESCRIPTION MEMP))
Warnings: Non-rec
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MEMP-LONESOMES
ACL2 >>(DEFUN NUMP (X)
(IF (CONSP X)
(AND (EQUAL (CAR X) NIL) (NUMP (CDR X)))
(EQUAL X NIL)))
The admission of NUMP 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 NUMP is described by the
theorem (OR (EQUAL (NUMP X) T) (EQUAL (NUMP X) NIL)). We used primitive
type reasoning.
Summary
Form: ( DEFUN NUMP ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
NUMP
ACL2 >>(DEFUN ADD (X Y)
(IF (CONSP X)
(CONS NIL (ADD (CDR X) Y))
(MAPNIL Y)))
The admission of ADD 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 ADD is described by the
theorem (TRUE-LISTP (ADD X Y)). We used primitive type reasoning and
the :type-prescription rule MAPNIL.
Summary
Form: ( DEFUN ADD ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:TYPE-PRESCRIPTION MAPNIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ADD
ACL2 >>(DEFUN MULT (X Y)
(IF (CONSP X)
(ADD Y (MULT (CDR X) Y))
NIL))
The admission of MULT 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 MULT is described by the
theorem (TRUE-LISTP (MULT X Y)). We used the :type-prescription rule
ADD.
Summary
Form: ( DEFUN MULT ...)
Rules: ((:TYPE-PRESCRIPTION ADD))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MULT
ACL2 >>(DEFUN RAISE (X Y)
(IF (CONSP Y)
(MULT X (RAISE X (CDR Y)))
'(NIL)))
The admission of RAISE 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 Y). We observe that the type of RAISE is described by
the theorem (TRUE-LISTP (RAISE X Y)). We used the :type-prescription
rule MULT.
Summary
Form: ( DEFUN RAISE ...)
Rules: ((:TYPE-PRESCRIPTION MULT))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
RAISE
ACL2 >>(DEFTHM NUMP-MAPNIL (NUMP (MAPNIL 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 (MAPNIL X). This
suggestion was produced using the :induction rule MAPNIL. 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 MAPNIL,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(NUMP (MAPNIL X))).
But simplification reduces this to T, using the :definition MAPNIL
and the :executable-counterpart of NUMP.
Subgoal *1/1
(IMPLIES (AND (CONSP X) (NUMP (MAPNIL (CDR X))))
(NUMP (MAPNIL X))).
But simplification reduces this to T, using the :definitions MAPNIL
and NUMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rules MAPNIL and NUMP.
That completes the proof of *1.
Q.E.D.
The storage of NUMP-MAPNIL depends upon the :type-prescription rule
NUMP.
[SGC for 4 SYMBOL pages..(8015 writable)..(T=1).GC finished]
Summary
Form: ( DEFTHM NUMP-MAPNIL ...)
Rules: ((:DEFINITION MAPNIL)
(:DEFINITION NUMP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NUMP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAPNIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MAPNIL)
(:TYPE-PRESCRIPTION NUMP))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
NUMP-MAPNIL
ACL2 >>(DEFTHM NUMP-ADD (NUMP (ADD X Y)))
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 (ADD X Y). This
suggestion was produced using the :induction rule ADD. 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 ADD,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(NUMP (ADD X Y))).
But simplification reduces this to T, using the :definition ADD and
the :rewrite rule NUMP-MAPNIL.
Subgoal *1/1
(IMPLIES (AND (CONSP X) (NUMP (ADD (CDR X) Y)))
(NUMP (ADD X Y))).
But simplification reduces this to T, using the :definitions ADD and
NUMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rules ADD and NUMP.
That completes the proof of *1.
Q.E.D.
The storage of NUMP-ADD depends upon the :type-prescription rule NUMP.
Summary
Form: ( DEFTHM NUMP-ADD ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION NUMP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE NUMP-MAPNIL)
(:TYPE-PRESCRIPTION ADD)
(:TYPE-PRESCRIPTION NUMP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NUMP-ADD
ACL2 >>(DEFTHM NUMP-MULT (NUMP (MULT X Y)))
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 (MULT X Y). This
suggestion was produced using the :induction rule MULT. 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 MULT,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(NUMP (MULT X Y))).
But simplification reduces this to T, using the :definition MULT and
the :executable-counterpart of NUMP.
Subgoal *1/1
(IMPLIES (AND (CONSP X) (NUMP (MULT (CDR X) Y)))
(NUMP (MULT X Y))).
But simplification reduces this to T, using the :definition MULT and
the :rewrite rule NUMP-ADD.
That completes the proof of *1.
Q.E.D.
The storage of NUMP-MULT depends upon the :type-prescription rule NUMP.
Summary
Form: ( DEFTHM NUMP-MULT ...)
Rules: ((:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART NUMP)
(:INDUCTION MULT)
(:REWRITE NUMP-ADD)
(:TYPE-PRESCRIPTION NUMP))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
NUMP-MULT
ACL2 >>(DEFTHM NUMP-RAISE (NUMP (RAISE X Y)))
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 (RAISE X Y). This
suggestion was produced using the :induction rule RAISE. If we let
(:P X Y) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP Y)) (:P X Y))
(IMPLIES (AND (CONSP Y) (:P X (CDR Y)))
(:P X Y))).
This induction is justified by the same argument used to admit RAISE,
namely, the measure (ACL2-COUNT Y) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP Y))
(NUMP (RAISE X Y))).
But simplification reduces this to T, using the :definition RAISE and
the :executable-counterpart of NUMP.
Subgoal *1/1
(IMPLIES (AND (CONSP Y) (NUMP (RAISE X (CDR Y))))
(NUMP (RAISE X Y))).
But simplification reduces this to T, using the :definition RAISE and
the :rewrite rule NUMP-MULT.
That completes the proof of *1.
Q.E.D.
The storage of NUMP-RAISE depends upon the :type-prescription rule
NUMP.
Summary
Form: ( DEFTHM NUMP-RAISE ...)
Rules: ((:DEFINITION RAISE)
(:EXECUTABLE-COUNTERPART NUMP)
(:INDUCTION RAISE)
(:REWRITE NUMP-MULT)
(:TYPE-PRESCRIPTION NUMP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NUMP-RAISE
ACL2 >>(DEFTHM ADD-IDENTITY
(IMPLIES (NUMP X)
(EQUAL (ADD 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 (NUMP X). This suggestion
was produced using the :induction rules ADD and NUMP. 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) (CAR X)) (:P X))
(IMPLIES (AND (CONSP X)
(NOT (CAR X))
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit NUMP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.
Subgoal *1/4
(IMPLIES (AND (NOT (CONSP X)) (NUMP X))
(EQUAL (ADD X NIL) X)).
But simplification reduces this to T, using the :definition NUMP, the
:executable-counterparts of ADD, CONSP and EQUAL and primitive type
reasoning.
Subgoal *1/3
(IMPLIES (AND (CONSP X) (CAR X) (NUMP X))
(EQUAL (ADD X NIL) X)).
But simplification reduces this to T, using the :definition NUMP and
primitive type reasoning.
Subgoal *1/2
(IMPLIES (AND (CONSP X)
(NOT (CAR X))
(EQUAL (ADD (CDR X) NIL) (CDR X))
(NUMP X))
(EQUAL (ADD X NIL) X)).
But simplification reduces this to T, using the :definitions ADD and
NUMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule ADD.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(NOT (CAR X))
(NOT (NUMP (CDR X)))
(NUMP X))
(EQUAL (ADD X NIL) X)).
But simplification reduces this to T, using the :definition NUMP and
the :executable-counterpart of EQUAL.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM ADD-IDENTITY ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION NUMP)
(:EXECUTABLE-COUNTERPART ADD)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:INDUCTION NUMP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION ADD))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ADD-IDENTITY
ACL2 >>(DEFTHM RAISE-MAPNIL
(EQUAL (RAISE I (MAPNIL J))
(RAISE I J)))
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 (RAISE I J). This
suggestion was produced using the :induction rules MAPNIL and RAISE.
If we let (:P I J) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (NOT (CONSP J)) (:P I J))
(IMPLIES (AND (CONSP J) (:P I (CDR J)))
(:P I J))).
This induction is justified by the same argument used to admit RAISE,
namely, the measure (ACL2-COUNT J) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP J))
(EQUAL (RAISE I (MAPNIL J))
(RAISE I J))).
But simplification reduces this to T, using the :definitions MAPNIL
and RAISE and the :executable-counterparts of CONSP and EQUAL.
Subgoal *1/1
(IMPLIES (AND (CONSP J)
(EQUAL (RAISE I (MAPNIL (CDR J)))
(RAISE I (CDR J))))
(EQUAL (RAISE I (MAPNIL J))
(RAISE I J))).
But simplification reduces this to T, using the :definitions MAPNIL
and RAISE, primitive type reasoning, the :rewrite rule CDR-CONS and
the :type-prescription rule MAPNIL.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM RAISE-MAPNIL ...)
Rules: ((:DEFINITION MAPNIL)
(:DEFINITION RAISE)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAPNIL)
(:INDUCTION RAISE)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MAPNIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
RAISE-MAPNIL
ACL2 >>(DEFTHM MULT-MAPNIL-1
(EQUAL (MULT (MAPNIL I) J) (MULT I J)))
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 (MULT I J). This
suggestion was produced using the :induction rules MAPNIL and MULT.
If we let (:P I J) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (MULT (MAPNIL I) J) (MULT I J))).
But simplification reduces this to T, using the :definitions MAPNIL
and MULT and the :executable-counterparts of CONSP and EQUAL.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (MULT (MAPNIL (CDR I)) J)
(MULT (CDR I) J)))
(EQUAL (MULT (MAPNIL I) J) (MULT I J))).
But simplification reduces this to T, using the :definitions MAPNIL
and MULT, primitive type reasoning, the :rewrite rule CDR-CONS and
the :type-prescription rule MAPNIL.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-MAPNIL-1 ...)
Rules: ((:DEFINITION MAPNIL)
(:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAPNIL)
(:INDUCTION MULT)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MAPNIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MULT-MAPNIL-1
ACL2 >>(DEFTHM MAPNIL-NUMP
(IMPLIES (NUMP X) (EQUAL (MAPNIL 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 (NUMP X). This suggestion
was produced using the :induction rules MAPNIL and NUMP. 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) (CAR X)) (:P X))
(IMPLIES (AND (CONSP X)
(NOT (CAR X))
(:P (CDR X)))
(:P X))).
This induction is justified by the same argument used to admit NUMP,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following four nontautological subgoals.
Subgoal *1/4
(IMPLIES (AND (NOT (CONSP X)) (NUMP X))
(EQUAL (MAPNIL X) X)).
But simplification reduces this to T, using the :definition NUMP, the
:executable-counterparts of CONSP, EQUAL and MAPNIL and primitive type
reasoning.
Subgoal *1/3
(IMPLIES (AND (CONSP X) (CAR X) (NUMP X))
(EQUAL (MAPNIL X) X)).
But simplification reduces this to T, using the :definition NUMP and
primitive type reasoning.
Subgoal *1/2
(IMPLIES (AND (CONSP X)
(NOT (CAR X))
(EQUAL (MAPNIL (CDR X)) (CDR X))
(NUMP X))
(EQUAL (MAPNIL X) X)).
But simplification reduces this to T, using the :definitions MAPNIL
and NUMP, the :executable-counterpart of EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule MAPNIL.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(NOT (CAR X))
(NOT (NUMP (CDR X)))
(NUMP X))
(EQUAL (MAPNIL X) X)).
But simplification reduces this to T, using the :definition NUMP and
the :executable-counterpart of EQUAL.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MAPNIL-NUMP ...)
Rules: ((:DEFINITION MAPNIL)
(:DEFINITION NUMP)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART MAPNIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MAPNIL)
(:INDUCTION NUMP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MAPNIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MAPNIL-NUMP
ACL2 >>(DEFTHM ADD-MAPNIL-1
(EQUAL (ADD (MAPNIL I) J) (ADD I J)))
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 (ADD I J). This
suggestion was produced using the :induction rules ADD and MAPNIL.
If we let (:P I J) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (ADD (MAPNIL I) J) (ADD I J))).
But simplification reduces this to T, using the :definitions ADD and
MAPNIL, the :executable-counterpart of CONSP and primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (ADD (MAPNIL (CDR I)) J)
(ADD (CDR I) J)))
(EQUAL (ADD (MAPNIL I) J) (ADD I J))).
But simplification reduces this to T, using the :definitions ADD and
MAPNIL, primitive type reasoning, the :rewrite rule CDR-CONS and the
:type-prescription rule MAPNIL.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM ADD-MAPNIL-1 ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MAPNIL)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:INDUCTION MAPNIL)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION MAPNIL))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ADD-MAPNIL-1
ACL2 >>(DEFTHM ADD-ASSOCIATIVITY
(EQUAL (ADD (ADD A B) C)
(ADD A (ADD B C))))
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 (ADD A B). This
suggestion was produced using the :induction rule ADD. If we let
(:P A B C) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
(IMPLIES (AND (CONSP A) (:P (CDR A) B C))
(:P A B C))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(EQUAL (ADD (ADD A B) C)
(ADD A (ADD B C)))).
But simplification reduces this to T, using the :definition ADD, primitive
type reasoning and the :rewrite rules ADD-MAPNIL-1, MAPNIL-NUMP and
NUMP-ADD.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(EQUAL (ADD (ADD (CDR A) B) C)
(ADD (CDR A) (ADD B C))))
(EQUAL (ADD (ADD A B) C)
(ADD A (ADD B C)))).
But simplification reduces this to T, using the :definition ADD, primitive
type reasoning, the :rewrite rule CDR-CONS and the :type-prescription
rule ADD.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM ADD-ASSOCIATIVITY ...)
Rules: ((:DEFINITION ADD)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:REWRITE ADD-MAPNIL-1)
(:REWRITE CDR-CONS)
(:REWRITE MAPNIL-NUMP)
(:REWRITE NUMP-ADD)
(:TYPE-PRESCRIPTION ADD))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ADD-ASSOCIATIVITY
ACL2 >>(DEFTHM MULT-ADD-DISTRIBUTIVITY-2
(EQUAL (MULT (ADD I J) K)
(ADD (MULT I K) (MULT J K))))
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (MULT I K), but modified
to accommodate (ADD I J). These suggestions were produced using the
:induction rules ADD and MULT. If we let (:P I J K) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J K))
(IMPLIES (AND (CONSP I) (:P (CDR I) J K))
(:P I J K))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (MULT (ADD I J) K)
(ADD (MULT I K) (MULT J K)))).
But simplification reduces this to T, using the :definitions ADD and
MULT, the :executable-counterpart of CONSP, primitive type reasoning
and the :rewrite rules MAPNIL-NUMP, MULT-MAPNIL-1 and NUMP-MULT.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (MULT (ADD (CDR I) J) K)
(ADD (MULT (CDR I) K) (MULT J K))))
(EQUAL (MULT (ADD I J) K)
(ADD (MULT I K) (MULT J K)))).
But simplification reduces this to T, using the :definitions ADD and
MULT, primitive type reasoning, the :rewrite rules ADD-ASSOCIATIVITY
and CDR-CONS and the :type-prescription rule ADD.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-ADD-DISTRIBUTIVITY-2 ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:INDUCTION MULT)
(:REWRITE ADD-ASSOCIATIVITY)
(:REWRITE CDR-CONS)
(:REWRITE MAPNIL-NUMP)
(:REWRITE MULT-MAPNIL-1)
(:REWRITE NUMP-MULT)
(:TYPE-PRESCRIPTION ADD))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MULT-ADD-DISTRIBUTIVITY-2
ACL2 >>(DEFTHM MULT-ASSOCIATIVE
(EQUAL (MULT (MULT A B) C)
(MULT A (MULT B C))))
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 (MULT A B). This
suggestion was produced using the :induction rule MULT. If we let
(:P A B C) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP A)) (:P A B C))
(IMPLIES (AND (CONSP A) (:P (CDR A) B C))
(:P A B C))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT A) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP A))
(EQUAL (MULT (MULT A B) C)
(MULT A (MULT B C)))).
But simplification reduces this to T, using the :definition MULT and
the :executable-counterparts of CONSP and EQUAL.
Subgoal *1/1
(IMPLIES (AND (CONSP A)
(EQUAL (MULT (MULT (CDR A) B) C)
(MULT (CDR A) (MULT B C))))
(EQUAL (MULT (MULT A B) C)
(MULT A (MULT B C)))).
But simplification reduces this to T, using the :definition MULT, primitive
type reasoning and the :rewrite rule MULT-ADD-DISTRIBUTIVITY-2.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-ASSOCIATIVE ...)
Rules: ((:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MULT)
(:REWRITE MULT-ADD-DISTRIBUTIVITY-2))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MULT-ASSOCIATIVE
ACL2 >>(DEFTHM RAISE-ADD
(EQUAL (RAISE B (ADD I J))
(MULT (RAISE B I) (RAISE B J))))
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. However, one of these is flawed and so we are left with one
viable candidate.
We will induct according to a scheme suggested by (RAISE B I), but
modified to accommodate (ADD I J). These suggestions were produced
using the :induction rules ADD and RAISE. If we let (:P B I J) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P B I J))
(IMPLIES (AND (CONSP I) (:P B (CDR I) J))
(:P B I J))).
This induction is justified by the same argument used to admit RAISE,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (RAISE B (ADD I J))
(MULT (RAISE B I) (RAISE B J)))).
But simplification reduces this to T, using the :definitions ADD, MULT
and RAISE, the :executable-counterparts of CDR and CONSP, primitive
type reasoning and the :rewrite rules ADD-IDENTITY, NUMP-RAISE and
RAISE-MAPNIL.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (RAISE B (ADD (CDR I) J))
(MULT (RAISE B (CDR I)) (RAISE B J))))
(EQUAL (RAISE B (ADD I J))
(MULT (RAISE B I) (RAISE B J)))).
But simplification reduces this to T, using the :definitions ADD and
RAISE, primitive type reasoning, the :rewrite rules CDR-CONS and MULT-
ASSOCIATIVE and the :type-prescription rule ADD.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM RAISE-ADD ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MULT)
(:DEFINITION RAISE)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:INDUCTION RAISE)
(:REWRITE ADD-IDENTITY)
(:REWRITE CDR-CONS)
(:REWRITE MULT-ASSOCIATIVE)
(:REWRITE NUMP-RAISE)
(:REWRITE RAISE-MAPNIL)
(:TYPE-PRESCRIPTION ADD))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
RAISE-ADD
ACL2 >>(DEFTHM ADD-IDENTITY-2
(IMPLIES (NOT (CONSP J))
(EQUAL (ADD I J) (MAPNIL I))))
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 (ADD I J). This
suggestion was produced using the :induction rules ADD and MAPNIL.
If we let (:P I J) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (CONSP I)) (NOT (CONSP J)))
(EQUAL (ADD I J) (MAPNIL I))).
But simplification reduces this to T, using the :definitions ADD and
MAPNIL and the :executable-counterpart of EQUAL.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (ADD (CDR I) J) (MAPNIL (CDR I)))
(NOT (CONSP J)))
(EQUAL (ADD I J) (MAPNIL I))).
But simplification reduces this to T, using the :definitions ADD and
MAPNIL and primitive type reasoning.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM ADD-IDENTITY-2 ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MAPNIL)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:INDUCTION MAPNIL))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
ADD-IDENTITY-2
ACL2 >>(DEFTHM ADD-CONS
(EQUAL (ADD I (CONS X J))
(CONS NIL (ADD I J))))
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 (ADD I J). This
suggestion was produced using the :induction rule ADD. If we let
(:P I J X) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J X))
(IMPLIES (AND (CONSP I) (:P (CDR I) J X))
(:P I J X))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (ADD I (CONS X J))
(CONS NIL (ADD I J)))).
But simplification reduces this to T, using the :definitions ADD and
MAPNIL, primitive type reasoning and the :rewrite rule CDR-CONS.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (ADD (CDR I) (CONS X J))
(CONS NIL (ADD (CDR I) J))))
(EQUAL (ADD I (CONS X J))
(CONS NIL (ADD I J)))).
But simplification reduces this to T, using the :definition ADD and
primitive type reasoning.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM ADD-CONS ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MAPNIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ADD-CONS
ACL2 >>(DEFTHM ADD-COMMUTATIVITY
(EQUAL (ADD I J) (ADD J I)))
ACL2 Warning [Subsume] in ( DEFTHM ADD-COMMUTATIVITY ...): The newly
proposed :REWRITE rule ADD-COMMUTATIVITY probably subsumes the previously
added :REWRITE rules ADD-CONS, ADD-IDENTITY-2, ADD-ASSOCIATIVITY, ADD-
MAPNIL-1 and ADD-IDENTITY, in the sense that ADD-COMMUTATIVITY will
now probably be applied whenever the old rules would have been.
Name the formula above *1.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. We will choose arbitrarily among these.
We will induct according to a scheme suggested by (ADD I J). This
suggestion was produced using the :induction rule ADD. If we let (:P I J)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (ADD I J) (ADD J I))).
But simplification reduces this to T, using the :definition ADD, primitive
type reasoning and the :rewrite rule ADD-IDENTITY-2.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (ADD (CDR I) J) (ADD J (CDR I))))
(EQUAL (ADD I J) (ADD J I))).
This simplifies, using the :definition ADD, to
Subgoal *1/1'
(IMPLIES (AND (CONSP I)
(EQUAL (ADD (CDR I) J) (ADD J (CDR I))))
(EQUAL (CONS NIL (ADD J (CDR I)))
(ADD J I))).
The destructor terms (CAR I) and (CDR I) can be eliminated by using
CAR-CDR-ELIM to replace I by (CONS I1 I2), (CAR I) by I1 and (CDR I)
by I2. This produces the following goal.
Subgoal *1/1''
(IMPLIES (AND (CONSP (CONS I1 I2))
(EQUAL (ADD I2 J) (ADD J I2)))
(EQUAL (CONS NIL (ADD J I2))
(ADD J (CONS I1 I2)))).
But we reduce the conjecture to T, by the simple :rewrite rule ADD-
CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM ADD-COMMUTATIVITY ...)
Rules: ((:DEFINITION ADD)
(:ELIM CAR-CDR-ELIM)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:REWRITE ADD-CONS)
(:REWRITE ADD-IDENTITY-2))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
ADD-COMMUTATIVITY
ACL2 >>(DEFTHM ADD-MAPNIL-2
(EQUAL (ADD I (MAPNIL J)) (ADD I J)))
ACL2 Warning [Subsume] in ( DEFTHM ADD-MAPNIL-2 ...): The previously
added rule ADD-COMMUTATIVITY subsumes the newly proposed :REWRITE rule
ADD-MAPNIL-2, in the sense that the old rule rewrites a more general
target. Because the new rule will be tried first, it may nonetheless
find application.
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 (ADD I J). This
suggestion was produced using the :induction rule ADD. If we let (:P I J)
denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (ADD I (MAPNIL J)) (ADD I J))).
But simplification reduces this to T, using the :definition ADD, primitive
type reasoning and the :rewrite rules MAPNIL-NUMP and NUMP-MAPNIL.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (ADD (CDR I) (MAPNIL J))
(ADD (CDR I) J)))
(EQUAL (ADD I (MAPNIL J)) (ADD I J))).
But simplification reduces this to T, using the :definition ADD and
primitive type reasoning.
That completes the proof of *1.
[SGC for 21 CFUN pages..(8042 writable)..(T=1).GC finished]
Q.E.D.
Summary
Form: ( DEFTHM ADD-MAPNIL-2 ...)
Rules: ((:DEFINITION ADD)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:REWRITE MAPNIL-NUMP)
(:REWRITE NUMP-MAPNIL))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
ADD-MAPNIL-2
ACL2 >>(DEFTHM ADD-COMMUTATIVITY2
(EQUAL (ADD I (ADD J K))
(ADD J (ADD I K))))
ACL2 Warning [Subsume] in ( DEFTHM ADD-COMMUTATIVITY2 ...): The previously
added rule ADD-COMMUTATIVITY subsumes the newly proposed :REWRITE rule
ADD-COMMUTATIVITY2, in the sense that the old rule rewrites a more
general target. Because the new rule will be tried first, it may nonetheless
find application.
Name the formula above *1.
Perhaps we can prove *1 by induction. Four induction schemes are suggested
by this conjecture. Subsumption reduces that number to two. We will
choose arbitrarily among these.
We will induct according to a scheme suggested by (ADD J K). This
suggestion was produced using the :induction rule ADD. If we let
(:P I J K) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP J)) (:P I J K))
(IMPLIES (AND (CONSP J) (:P I (CDR J) K))
(:P I J K))).
This induction is justified by the same argument used to admit ADD,
namely, the measure (ACL2-COUNT J) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP J))
(EQUAL (ADD I (ADD J K))
(ADD J (ADD I K)))).
But simplification reduces this to T, using the :definition ADD, primitive
type reasoning and the :rewrite rules ADD-MAPNIL-2, MAPNIL-NUMP and
NUMP-ADD.
Subgoal *1/1
(IMPLIES (AND (CONSP J)
(EQUAL (ADD I (ADD (CDR J) K))
(ADD (CDR J) (ADD I K))))
(EQUAL (ADD I (ADD J K))
(ADD J (ADD I K)))).
But simplification reduces this to T, using the :definition ADD, primitive
type reasoning and the :rewrite rule ADD-CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM ADD-COMMUTATIVITY2 ...)
Rules: ((:DEFINITION ADD)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:REWRITE ADD-CONS)
(:REWRITE ADD-MAPNIL-2)
(:REWRITE MAPNIL-NUMP)
(:REWRITE NUMP-ADD))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
ADD-COMMUTATIVITY2
ACL2 >>(DEFTHM MULT-ZERO
(IMPLIES (NOT (CONSP J))
(EQUAL (MULT I J) NIL)))
This simplifies, using primitive type reasoning, to
Goal'
(IMPLIES (NOT (CONSP J))
(NOT (MULT I J))).
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 (MULT I J). This
suggestion was produced using the :induction rule MULT. If we let
(:P I J) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (AND (NOT (CONSP I)) (NOT (CONSP J)))
(NOT (MULT I J))).
But simplification reduces this to T, using the :definition MULT.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(NOT (MULT (CDR I) J))
(NOT (CONSP J)))
(NOT (MULT I J))).
But simplification reduces this to T, using the :definition MULT, the
:executable-counterpart of MAPNIL and the :rewrite rules ADD-COMMUTATIVITY
and ADD-IDENTITY-2.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-ZERO ...)
Rules: ((:DEFINITION MULT)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART MAPNIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MULT)
(:REWRITE ADD-COMMUTATIVITY)
(:REWRITE ADD-IDENTITY-2))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MULT-ZERO
ACL2 >>(DEFTHM MULT-CONS
(EQUAL (MULT I (CONS X J))
(ADD I (MULT I J))))
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 one.
We will induct according to a scheme suggested by (MULT I J). This
suggestion was produced using the :induction rules ADD and MULT. If
we let (:P I J X) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J X))
(IMPLIES (AND (CONSP I) (:P (CDR I) J X))
(:P I J X))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (MULT I (CONS X J))
(ADD I (MULT I J)))).
But simplification reduces this to T, using the :definition MULT, the
:executable-counterparts of EQUAL and MAPNIL and the :rewrite rules
ADD-COMMUTATIVITY and ADD-IDENTITY-2.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (MULT (CDR I) (CONS X J))
(ADD (CDR I) (MULT (CDR I) J))))
(EQUAL (MULT I (CONS X J))
(ADD I (MULT I J)))).
This simplifies, using the :definitions ADD and MULT, primitive type
reasoning and the :rewrite rule CDR-CONS, to
Subgoal *1/1'
(IMPLIES (AND (CONSP I)
(EQUAL (MULT (CDR I) (CONS X J))
(ADD (CDR I) (MULT (CDR I) J))))
(EQUAL (CONS NIL (ADD J (MULT (CDR I) (CONS X J))))
(ADD I (ADD J (MULT (CDR I) J))))).
But simplification reduces this to T, using the :definition ADD, primitive
type reasoning and the :rewrite rule ADD-COMMUTATIVITY2.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-CONS ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART MAPNIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:INDUCTION MULT)
(:REWRITE ADD-COMMUTATIVITY)
(:REWRITE ADD-COMMUTATIVITY2)
(:REWRITE ADD-IDENTITY-2)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MULT-CONS
ACL2 >>(DEFTHM MULT-COMMUTATIVITY
(EQUAL (MULT I J) (MULT J I)))
ACL2 Warning [Subsume] in ( DEFTHM MULT-COMMUTATIVITY ...): The newly
proposed :REWRITE rule MULT-COMMUTATIVITY probably subsumes the previously
added :REWRITE rules MULT-CONS, MULT-ZERO, MULT-ASSOCIATIVE, MULT-ADD-
DISTRIBUTIVITY-2 and MULT-MAPNIL-1, in the sense that MULT-COMMUTATIVITY
will now probably be applied whenever the old rules would have been.
Name the formula above *1.
Perhaps we can prove *1 by induction. Two induction schemes are suggested
by this conjecture. We will choose arbitrarily among these.
We will induct according to a scheme suggested by (MULT I J). This
suggestion was produced using the :induction rule MULT. If we let
(:P I J) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (MULT I J) (MULT J I))).
But simplification reduces this to T, using the :definition MULT, the
:executable-counterpart of EQUAL and the :rewrite rule MULT-ZERO.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (MULT (CDR I) J)
(MULT J (CDR I))))
(EQUAL (MULT I J) (MULT J I))).
This simplifies, using the :definition MULT, to
Subgoal *1/1'
(IMPLIES (AND (CONSP I)
(EQUAL (MULT (CDR I) J)
(MULT J (CDR I))))
(EQUAL (ADD J (MULT J (CDR I)))
(MULT J I))).
The destructor terms (CAR I) and (CDR I) can be eliminated by using
CAR-CDR-ELIM to replace I by (CONS I1 I2), (CAR I) by I1 and (CDR I)
by I2. This produces the following goal.
Subgoal *1/1''
(IMPLIES (AND (CONSP (CONS I1 I2))
(EQUAL (MULT I2 J) (MULT J I2)))
(EQUAL (ADD J (MULT J I2))
(MULT J (CONS I1 I2)))).
But we reduce the conjecture to T, by the simple :rewrite rule MULT-
CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-COMMUTATIVITY ...)
Rules: ((:DEFINITION MULT)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART EQUAL)
(:INDUCTION MULT)
(:REWRITE MULT-CONS)
(:REWRITE MULT-ZERO))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
MULT-COMMUTATIVITY
ACL2 >>(DEFTHM MULT-MAPNIL-2
(EQUAL (MULT I (MAPNIL J)) (MULT I J)))
ACL2 Warning [Subsume] in ( DEFTHM MULT-MAPNIL-2 ...): The previously
added rule MULT-COMMUTATIVITY subsumes the newly proposed :REWRITE
rule MULT-MAPNIL-2, in the sense that the old rule rewrites a more
general target. Because the new rule will be tried first, it may nonetheless
find application.
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 (MULT I J). This
suggestion was produced using the :induction rule MULT. If we let
(:P I J) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J))
(IMPLIES (AND (CONSP I) (:P (CDR I) J))
(:P I J))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (MULT I (MAPNIL J)) (MULT I J))).
But simplification reduces this to T, using the :definition MULT and
the :executable-counterpart of EQUAL.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (MULT (CDR I) (MAPNIL J))
(MULT (CDR I) J)))
(EQUAL (MULT I (MAPNIL J)) (MULT I J))).
But simplification reduces this to T, using the :definition MULT, primitive
type reasoning and the :rewrite rule ADD-MAPNIL-1.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-MAPNIL-2 ...)
Rules: ((:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MULT)
(:REWRITE ADD-MAPNIL-1))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MULT-MAPNIL-2
ACL2 >>(DEFTHM MULT-ADD-DISTRIBUTIVITY-1
(EQUAL (MULT K (ADD I J))
(ADD (MULT K I) (MULT K J))))
ACL2 Warning [Subsume] in ( DEFTHM MULT-ADD-DISTRIBUTIVITY-1 ...):
The previously added rule MULT-COMMUTATIVITY subsumes the newly proposed
:REWRITE rule MULT-ADD-DISTRIBUTIVITY-1, in the sense that the old
rule rewrites a more general target. Because the new rule will be
tried first, it may nonetheless find application.
This simplifies, using the :rewrite rule MULT-COMMUTATIVITY, to
Goal'
(EQUAL (MULT K (ADD I J))
(ADD (MULT I K) (MULT J K))).
Name the formula above *1.
Perhaps we can prove *1 by induction. Four induction schemes are suggested
by this conjecture. These merge into three derived induction schemes.
However, two of these are flawed and so we are left with one viable
candidate.
We will induct according to a scheme suggested by (MULT I K), but modified
to accommodate (ADD I J). These suggestions were produced using the
:induction rules ADD and MULT. If we let (:P I J K) denote *1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP I)) (:P I J K))
(IMPLIES (AND (CONSP I) (:P (CDR I) J K))
(:P I J K))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT I) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP I))
(EQUAL (MULT K (ADD I J))
(ADD (MULT I K) (MULT J K)))).
But simplification reduces this to T, using the :definitions ADD and
MULT, the :executable-counterpart of CONSP, primitive type reasoning
and the :rewrite rules MAPNIL-NUMP, MULT-COMMUTATIVITY, MULT-MAPNIL-
2 and NUMP-MULT.
Subgoal *1/1
(IMPLIES (AND (CONSP I)
(EQUAL (MULT K (ADD (CDR I) J))
(ADD (MULT (CDR I) K) (MULT J K))))
(EQUAL (MULT K (ADD I J))
(ADD (MULT I K) (MULT J K)))).
But simplification reduces this to T, using the :definitions ADD and
MULT, primitive type reasoning and the :rewrite rules ADD-COMMUTATIVITY,
ADD-COMMUTATIVITY2 and MULT-CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-ADD-DISTRIBUTIVITY-1 ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION ADD)
(:INDUCTION MULT)
(:REWRITE ADD-COMMUTATIVITY)
(:REWRITE ADD-COMMUTATIVITY2)
(:REWRITE MAPNIL-NUMP)
(:REWRITE MULT-COMMUTATIVITY)
(:REWRITE MULT-CONS)
(:REWRITE MULT-MAPNIL-2)
(:REWRITE NUMP-MULT))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MULT-ADD-DISTRIBUTIVITY-1
ACL2 >>(DEFTHM MULT-COMMUTATIVITY2
(EQUAL (MULT I (MULT J K))
(MULT J (MULT I K))))
ACL2 Warning [Subsume] in ( DEFTHM MULT-COMMUTATIVITY2 ...): The previously
added rule MULT-COMMUTATIVITY subsumes the newly proposed :REWRITE
rule MULT-COMMUTATIVITY2, in the sense that the old rule rewrites a
more general target. Because the new rule will be tried first, it
may nonetheless find application.
Name the formula above *1.
Perhaps we can prove *1 by induction. Four induction schemes are suggested
by this conjecture. Subsumption reduces that number to two. We will
choose arbitrarily among these.
We will induct according to a scheme suggested by (MULT J K). This
suggestion was produced using the :induction rule MULT. If we let
(:P I J K) denote *1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP J)) (:P I J K))
(IMPLIES (AND (CONSP J) (:P I (CDR J) K))
(:P I J K))).
This induction is justified by the same argument used to admit MULT,
namely, the measure (ACL2-COUNT J) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP J))
(EQUAL (MULT I (MULT J K))
(MULT J (MULT I K)))).
But simplification reduces this to T, using the :definition MULT, the
:executable-counterparts of CONSP and EQUAL and the :rewrite rule MULT-
COMMUTATIVITY.
Subgoal *1/1
(IMPLIES (AND (CONSP J)
(EQUAL (MULT I (MULT (CDR J) K))
(MULT (CDR J) (MULT I K))))
(EQUAL (MULT I (MULT J K))
(MULT J (MULT I K)))).
But simplification reduces this to T, using the :definition MULT, primitive
type reasoning and the :rewrite rule MULT-ADD-DISTRIBUTIVITY-1.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MULT-COMMUTATIVITY2 ...)
Rules: ((:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION MULT)
(:REWRITE MULT-ADD-DISTRIBUTIVITY-1)
(:REWRITE MULT-COMMUTATIVITY))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MULT-COMMUTATIVITY2
ACL2 >>(DEFTHM REV1-IS-APP-REV
(EQUAL (REV1 X A) (APP (REV X) A)))
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 (REV1 X A). This
suggestion was produced using the :induction rules REV and REV1. If
we let (:P A X) denote *1 above then the induction scheme we'll use
is
(AND (IMPLIES (NOT (CONSP X)) (:P A X))
(IMPLIES (AND (CONSP X)
(:P (CONS (CAR X) A) (CDR X)))
(:P A X))).
This induction is justified by the same argument used to admit REV1,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). Note, however, that the unmeasured variable A is being instantiated.
When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(EQUAL (REV1 X A) (APP (REV X) A))).
But simplification reduces this to T, using the :definitions APP, REV
and REV1, the :executable-counterpart of CONSP and primitive type reasoning.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(EQUAL (REV1 (CDR X) (CONS (CAR X) A))
(APP (REV (CDR X)) (CONS (CAR X) A))))
(EQUAL (REV1 X A) (APP (REV X) A))).
But simplification reduces this to T, using the :definitions APP, REV
and REV1, the :executable-counterpart of CONSP, primitive type reasoning
and the :rewrite rules ASSOCIATIVITY-OF-APP, CAR-CONS and CDR-CONS.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM REV1-IS-APP-REV ...)
Rules: ((:DEFINITION APP)
(:DEFINITION REV)
(:DEFINITION REV1)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION REV)
(:INDUCTION REV1)
(:REWRITE ASSOCIATIVITY-OF-APP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
REV1-IS-APP-REV
ACL2 >>(DEFTHM REV1-NIL-IS-REV
(EQUAL (REV1 X NIL) (REV X)))
ACL2 Warning [Subsume] in ( DEFTHM REV1-NIL-IS-REV ...): The previously
added rule REV1-IS-APP-REV subsumes the newly proposed :REWRITE rule
REV1-NIL-IS-REV, in the sense that the old rule rewrites a more general
target. Because the new rule will be tried first, it may nonetheless
find application.
By the simple :rewrite rule REV1-IS-APP-REV we reduce the conjecture
to
Goal'
(EQUAL (APP (REV X) NIL) (REV X)).
But simplification reduces this to T, using primitive type reasoning
and the :rewrite rules APP-RIGHT-IDENTITY and PROPERP-REV.
Q.E.D.
Summary
Form: ( DEFTHM REV1-NIL-IS-REV ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE APP-RIGHT-IDENTITY)
(:REWRITE PROPERP-REV)
(:REWRITE REV1-IS-APP-REV))
Warnings: Subsume
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REV1-NIL-IS-REV
ACL2 >>(DEFUN FACT (N)
(IF (CONSP N)
(MULT N (FACT (CDR N)))
'(NIL)))
The admission of FACT 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 FACT is described by the
theorem (TRUE-LISTP (FACT N)). We used the :type-prescription rule
MULT.
Summary
Form: ( DEFUN FACT ...)
Rules: ((:TYPE-PRESCRIPTION MULT))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FACT
ACL2 >>(DEFUN FACT1 (N A)
(IF (CONSP N)
(FACT1 (CDR N) (MULT N A))
A))
The admission of FACT1 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 FACT1 is described by
the theorem (OR (TRUE-LISTP (FACT1 N A)) (EQUAL (FACT1 N A) A)). We
used the :type-prescription rule MULT.
Summary
Form: ( DEFUN FACT1 ...)
Rules: ((:TYPE-PRESCRIPTION MULT))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
FACT1
ACL2 >>(DEFTHM FACT1-IS-FACT-GENERALIZED
(IMPLIES (NUMP A)
(EQUAL (FACT1 N A) (MULT (FACT N) A))))
This simplifies, using the :rewrite rule MULT-COMMUTATIVITY, to
Goal'
(IMPLIES (NUMP A)
(EQUAL (FACT1 N A) (MULT A (FACT N)))).
Name the formula above *1.
Perhaps we can prove *1 by induction. Four 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 (FACT1 N A). This
suggestion was produced using the :induction rules FACT and FACT1.
If we let (:P A N) denote *1 above then the induction scheme we'll
use is
(AND (IMPLIES (NOT (CONSP N)) (:P A N))
(IMPLIES (AND (CONSP N) (:P (MULT N A) (CDR N)))
(:P A N))).
This induction is justified by the same argument used to admit FACT1,
namely, the measure (ACL2-COUNT N) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). Note, however, that the unmeasured variable A is being instantiated.
When applied to the goal at hand the above induction scheme produces
the following three nontautological subgoals.
Subgoal *1/3
(IMPLIES (AND (NOT (CONSP N)) (NUMP A))
(EQUAL (FACT1 N A) (MULT A (FACT N)))).
But simplification reduces this to T, using the :definitions ADD, FACT,
FACT1 and MULT, the :executable-counterparts of CDR and CONSP, primitive
type reasoning, the :rewrite rules ADD-COMMUTATIVITY, MAPNIL-NUMP and
MULT-COMMUTATIVITY and the :type-prescription rule NUMP.
Subgoal *1/2
(IMPLIES (AND (CONSP N)
(EQUAL (FACT1 (CDR N) (MULT N A))
(MULT (MULT N A) (FACT (CDR N))))
(NUMP A))
(EQUAL (FACT1 N A) (MULT A (FACT N)))).
By the simple :rewrite rule MULT-ASSOCIATIVE we reduce the conjecture
to
Subgoal *1/2'
(IMPLIES (AND (CONSP N)
(EQUAL (FACT1 (CDR N) (MULT N A))
(MULT N (MULT A (FACT (CDR N)))))
(NUMP A))
(EQUAL (FACT1 N A) (MULT A (FACT N)))).
But simplification reduces this to T, using the :definitions FACT,
FACT1 and MULT, primitive type reasoning and the :rewrite rules MULT-
ADD-DISTRIBUTIVITY-1 and MULT-COMMUTATIVITY2.
Subgoal *1/1
(IMPLIES (AND (CONSP N)
(NOT (NUMP (MULT N A)))
(NUMP A))
(EQUAL (FACT1 N A) (MULT A (FACT N)))).
But we reduce the conjecture to T, by the simple :rewrite rule NUMP-
MULT.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM FACT1-IS-FACT-GENERALIZED ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION FACT)
(:DEFINITION FACT1)
(:DEFINITION MULT)
(:DEFINITION NOT)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION FACT)
(:INDUCTION FACT1)
(:REWRITE ADD-COMMUTATIVITY)
(:REWRITE MAPNIL-NUMP)
(:REWRITE MULT-ADD-DISTRIBUTIVITY-1)
(:REWRITE MULT-ASSOCIATIVE)
(:REWRITE MULT-COMMUTATIVITY)
(:REWRITE MULT-COMMUTATIVITY2)
(:REWRITE NUMP-MULT)
(:TYPE-PRESCRIPTION NUMP))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
FACT1-IS-FACT-GENERALIZED
ACL2 >>(DEFTHM NUMP-FACT (NUMP (FACT N)))
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 (FACT N). This suggestion
was produced using the :induction rule FACT. If we let (:P N) denote
*1 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (CONSP N)) (:P N))
(IMPLIES (AND (CONSP N) (:P (CDR N)))
(:P N))).
This induction is justified by the same argument used to admit FACT,
namely, the measure (ACL2-COUNT N) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP N))
(NUMP (FACT N))).
But simplification reduces this to T, using the :definition FACT and
the :executable-counterpart of NUMP.
Subgoal *1/1
(IMPLIES (AND (CONSP N) (NUMP (FACT (CDR N))))
(NUMP (FACT N))).
But simplification reduces this to T, using the :definitions FACT and
MULT and the :rewrite rule NUMP-ADD.
That completes the proof of *1.
Q.E.D.
The storage of NUMP-FACT depends upon the :type-prescription rule NUMP.
Summary
Form: ( DEFTHM NUMP-FACT ...)
Rules: ((:DEFINITION FACT)
(:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART NUMP)
(:INDUCTION FACT)
(:REWRITE NUMP-ADD)
(:TYPE-PRESCRIPTION NUMP))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
NUMP-FACT
ACL2 >>(DEFTHM FACT1-IS-FACT
(EQUAL (FACT1 N '(NIL)) (FACT N)))
But simplification reduces this to T, using the :definitions ADD and
MULT, the :executable-counterparts of CDR, CONSP and NUMP, primitive
type reasoning and the :rewrite rules ADD-COMMUTATIVITY, FACT1-IS-FACT-
GENERALIZED, MAPNIL-NUMP, MULT-COMMUTATIVITY and NUMP-FACT.
Q.E.D.
Summary
Form: ( DEFTHM FACT1-IS-FACT ...)
Rules: ((:DEFINITION ADD)
(:DEFINITION MULT)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART NUMP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE ADD-COMMUTATIVITY)
(:REWRITE FACT1-IS-FACT-GENERALIZED)
(:REWRITE MAPNIL-NUMP)
(:REWRITE MULT-COMMUTATIVITY)
(:REWRITE NUMP-FACT))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
FACT1-IS-FACT
ACL2 >>(DEFUN MC-FLATTEN (X A)
(IF (CONSP X)
(MC-FLATTEN (CAR X)
(MC-FLATTEN (CDR X) A))
(CONS X A)))
The admission of MC-FLATTEN 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 MC-FLATTEN is
described by the theorem (CONSP (MC-FLATTEN X A)). We used primitive
type reasoning.
Summary
Form: ( DEFUN MC-FLATTEN ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
MC-FLATTEN
ACL2 >>(DEFTHM MC-FLATTEN-IS-LEAVES-GENERALIZED
(EQUAL (MC-FLATTEN X A)
(APP (LEAVES X) A)))
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 (MC-FLATTEN X A).
This suggestion was produced using the :induction rules LEAVES and
MC-FLATTEN. If we let (:P A X) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (NOT (CONSP X)) (:P A X))
(IMPLIES (AND (CONSP X)
(:P (MC-FLATTEN (CDR X) A) (CAR X))
(:P A (CDR X)))
(:P A X))).
This induction is justified by the same argument used to admit MC-FLATTEN,
namely, the measure (ACL2-COUNT X) is decreasing according to the relation
O< (which is known to be well-founded on the domain recognized by O-
P). Note, however, that the unmeasured variable A is being instantiated.
When applied to the goal at hand the above induction scheme produces
the following two nontautological subgoals.
Subgoal *1/2
(IMPLIES (NOT (CONSP X))
(EQUAL (MC-FLATTEN X A)
(APP (LEAVES X) A))).
But simplification reduces this to T, using the :definitions APP, LEAVES
and MC-FLATTEN, the :executable-counterpart of CONSP, primitive type
reasoning and the :rewrite rules CAR-CONS and CDR-CONS.
Subgoal *1/1
(IMPLIES (AND (CONSP X)
(EQUAL (MC-FLATTEN (CAR X)
(MC-FLATTEN (CDR X) A))
(APP (LEAVES (CAR X))
(MC-FLATTEN (CDR X) A)))
(EQUAL (MC-FLATTEN (CDR X) A)
(APP (LEAVES (CDR X)) A)))
(EQUAL (MC-FLATTEN X A)
(APP (LEAVES X) A))).
But simplification reduces this to T, using the :definitions LEAVES
and MC-FLATTEN, primitive type reasoning and the :rewrite rule ASSOCIATIVITY-
OF-APP.
That completes the proof of *1.
Q.E.D.
Summary
Form: ( DEFTHM MC-FLATTEN-IS-LEAVES-GENERALIZED ...)
Rules: ((:DEFINITION APP)
(:DEFINITION LEAVES)
(:DEFINITION MC-FLATTEN)
(:EXECUTABLE-COUNTERPART CONSP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION LEAVES)
(:INDUCTION MC-FLATTEN)
(:REWRITE ASSOCIATIVITY-OF-APP)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
MC-FLATTEN-IS-LEAVES-GENERALIZED
ACL2 >>(DEFTHM PROPERP-LEAVES (PROPERP (LEAVES X)))
This event is redundant. See :DOC redundant-events.
Summary
Form: ( DEFTHM PROPERP-LEAVES ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT
ACL2 >>(DEFTHM MC-FLATTEN-IS-LEAVES
(EQUAL (MC-FLATTEN X NIL) (LEAVES X)))
ACL2 Warning [Subsume] in ( DEFTHM MC-FLATTEN-IS-LEAVES ...): The
previously added rule MC-FLATTEN-IS-LEAVES-GENERALIZED subsumes the
newly proposed :REWRITE rule MC-FLATTEN-IS-LEAVES, in the sense that
the old rule rewrites a more general target. Because the new rule
will be tried first, it may nonetheless find application.
By the simple :rewrite rule MC-FLATTEN-IS-LEAVES-GENERALIZED we reduce
the conjecture to
Goal'
(EQUAL (APP (LEAVES X) NIL) (LEAVES X)).
But simplification reduces this to T, using primitive type reasoning
and the :rewrite rules APP-RIGHT-IDENTITY and PROPERP-LEAVES.
Q.E.D.
Summary
Form: ( DEFTHM MC-FLATTEN-IS-LEAVES ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE APP-RIGHT-IDENTITY)
(:REWRITE MC-FLATTEN-IS-LEAVES-GENERALIZED)
(:REWRITE PROPERP-LEAVES))
Warnings: Subsume
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
MC-FLATTEN-IS-LEAVES
* Step 3: That completes the admissibility check. Each form read
was an embedded event form and was admissible. We now retract back
to the initial world and try to include the book. This may expose
local incompatibilities.
[SGC for 25 FIXNUM pages..(8363 writable)..(T=1).GC finished]
Summary
Form: ( INCLUDE-BOOK "how-to-prove-thms" ...)
Rules: NIL
Warnings: None
Time: 0.07 seconds (prove: 0.00, print: 0.00, other: 0.07)
ACL2 Warning [Guards] in (CERTIFY-BOOK "how-to-prove-thms" ...): You
have told certify-book to produce a compiled file for
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp".
However, the functions DUP, APP, MEMP, REV, REV1, PROPERP, MAPNIL,
SWAPTREE, ZIPLISTS, LOOKUP, FOUNDP, SUBP, INT, MEM, LONESOMEP, COLLECT-
LONESOMEP, LEAVES, LONESOMES, TREECOPY, SETEQP, LIST-OF-ATOMSP, NUMP,
ADD, MULT, RAISE, FACT, FACT1 and MC-FLATTEN have not had their guards
verified. A compiled file will be produced anyway, but all bets are
off if you load it into raw Common Lisp and try to run the functions
in it. See :DOC verify-guards.
* Step 4: Write the certificate for
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp"
in "/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.cert".
The final check sum alist is
(("/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp"
"how-to-prove-thms" "how-to-prove-thms"
((:SKIPPED-PROOFSP) (:AXIOMSP))
. 190369092)).
* Step 5: Compile the functions defined in
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp".
As noted above, 28 functions have not had their guards verified. A
compiled file will be produced but you are advised not to use it in
raw Common Lisp. See :DOC guard for a general discussion of the issues.
Compiling /export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp.
End of Pass 1.
;; Note: Tail-recursive call of MEMP was replaced by iteration.
;; Note: Tail-recursive call of REV1 was replaced by iteration.
;; Note: Tail-recursive call of PROPERP was replaced by iteration.
;; Note: Tail-recursive call of LOOKUP was replaced by iteration.
;; Note: Tail-recursive call of FOUNDP was replaced by iteration.
;; Note: Tail-recursive call of SUBP was replaced by iteration.
;; Note: Tail-recursive call of INT was replaced by iteration.
;; Note: Tail-recursive call of MEM was replaced by iteration.
;; Note: Tail-recursive call of COLLECT-LONESOMEP was replaced by iteration.
Warning: LEAVES has a duplicate definition in this file
;; Note: Tail-recursive call of LIST-OF-ATOMSP was replaced by iteration.
;; Note: Tail-recursive call of NUMP was replaced by iteration.
;; Note: Tail-recursive call of FACT1 was replaced by iteration.
;; Note: Tail-recursive call of MC-FLATTEN was replaced by iteration.
End of Pass 2.
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.o.
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.o"
Loading /export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.o
start address -T 0x90292e0 Finished loading /export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.o
Summary
Form: (CERTIFY-BOOK "how-to-prove-thms" ...)
Rules: NIL
Warnings: Guards, Non-rec, Free and Subsume
Time: 0.63 seconds (prove: 0.28, print: 0.16, other: 0.19)
"/export/v/filer3/v0q005/text/marktoberdorf-04/how-to-prove-thms.lisp"
ACL2 !>