~/Dropbox/talks/key-workshop-july-2015/demos$ acl2-7.1
Welcome to Clozure Common Lisp Version 1.11-dev-r16378M-trunk  (DarwinX8664)!

 ACL2 Version 7.1 built May 6, 2015  18:48:38.
 Copyright (C) 2015, Regents of the University of Texas
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the LICENSE file distributed with ACL2.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).

 Includes support for hash cons, memoization, and applicative hash
 tables.

 See the documentation topic note-7-1 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

Customizing with "/Users/kaufmann/acl2-customization.lsp".

ACL2 Version 7.1.  Level 1.  Cbd "/Users/kaufmann/".
System books directory "/Users/kaufmann/acl2/v7-1/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !><state>
ACL2 !>Bye.

ACL2 Version 7.1.  Level 1.  Cbd 
"/Users/kaufmann/Dropbox/talks/key-workshop-july-2015/demos/".
System books directory "/Users/kaufmann/acl2/v7-1/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(defun mem (a lst)
       ; Return t if a is a member of the list, lst, else
       ; nil.  This definition is typical in style for
       ; list processing.  The termination proof
       ; obligation, important for soundness, is
       ; discharged automatically.
	 (cond ((atom lst)
		nil)
	       ((equal a (car lst))
		t)
	       (t
		(mem a (cdr lst)))))

The admission of MEM is trivial, using the relation
O< (which is known to be well-founded on the domain
recognized by O-P) and the measure (ACL2-COUNT LST).
We observe that the type of MEM is described by the
theorem (OR (EQUAL (MEM A LST) T) (EQUAL (MEM A LST) NIL)).

Summary
Form:  ( DEFUN MEM ...)
Rules: NIL
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 MEM
ACL2 !>(defun del (a lst)
       ; This function deletes the first occurrence of a
       ; (if any) in the list, lst.
	 (cond ((atom lst)
		nil)
	       ((equal a (car lst))
		(cdr lst))
	       (t
		(cons (car lst)
		      (del a (cdr lst))))))

The admission of DEL is trivial, using the relation
O< (which is known to be well-founded on the domain
recognized by O-P) and the measure (ACL2-COUNT LST).
We could deduce no constraints on the type of DEL.

Summary
Form:  ( DEFUN DEL ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 DEL
ACL2 !>(defun perm (lst1 lst2)
       ; Given two lists, return t if lst1 is a
       ; permutation of lst2.
	 (cond ((atom lst1)
		(atom lst2))
	       ((mem (car lst1) lst2)
		(perm (cdr lst1)
		      (del (car lst1) lst2)))
	       (t
		nil)))

The admission of PERM is trivial, using the relation
O< (which is known to be well-founded on the domain
recognized by O-P) and the measure (ACL2-COUNT LST1).
We observe that the type of PERM is described by the
theorem (OR (EQUAL (PERM LST1 LST2) T) (EQUAL (PERM LST1 LST2) NIL)).

Summary
Form:  ( DEFUN PERM ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
 PERM
ACL2 !>(defthm perm-transitive ; OUR GOAL for this demo
	 (implies (and (perm x y) (perm y z))
		  (perm x z)))

ACL2 Warning [Free] in ( DEFTHM PERM-TRANSITIVE ...):
A :REWRITE rule generated from PERM-TRANSITIVE contains
the free variable Y.  This variable will be chosen by
searching for an instance of (PERM X Y) in the context
of the term being rewritten.  This is generally a severe
restriction on the applicability of a :REWRITE rule.
See :DOC free-variables.


*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (PERM X Z),
but modified to accommodate (PERM X Y).  These suggestions
were produced using the :induction rule PERM.  If we
let (:P X Y Z) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ATOM X))
                   (NOT (MEM (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (AND (NOT (ATOM X))
                   (MEM (CAR X) Z)
                   (:P (CDR X)
                       (DEL (CAR X) Y)
                       (DEL (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (ATOM X) (:P X Y Z))).
This induction is justified by the same argument used
to admit PERM.  Note, however, that the unmeasured variables
Y and Z are being instantiated.  When applied to the
goal at hand the above induction scheme produces five
nontautological subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/5''
Subgoal *1/5'''
Subgoal *1/5'4'

([ A key checkpoint while proving *1 (descended from
Goal):

Subgoal *1/5''
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Z))
              (MEM (CAR X) Y)
              (PERM (CDR X) (DEL (CAR X) Y)))
         (NOT (PERM Y Z)))

*1.1 (Subgoal *1/5'4') is pushed for proof by induction.

])
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'
Subgoal *1/3'5'

([ A key checkpoint while proving *1 (descended from
Goal):

Subgoal *1/3''
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Z)
              (NOT (PERM (DEL (CAR X) Y) (DEL (CAR X) Z)))
              (MEM (CAR X) Y)
              (PERM (CDR X) (DEL (CAR X) Y))
              (PERM Y Z))
         (PERM (CDR X) (DEL (CAR X) Z)))

*1.2 (Subgoal *1/3'5') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.2, which is

(IMPLIES (AND (MEM X1 Z)
              (NOT (PERM DL0 DL))
              (MEM X1 Y)
              (PERM X2 DL0)
              (PERM Y Z))
         (PERM X2 DL)).
Subgoal *1.2/5
Subgoal *1.2/5'
Subgoal *1.2/5''
Subgoal *1.2/5'''
Subgoal *1.2/5'4'

*1.2.1 (Subgoal *1.2/5'4') is pushed for proof by induction.
Subgoal *1.2/4
Subgoal *1.2/4'
Subgoal *1.2/3
Subgoal *1.2/3'
Subgoal *1.2/2
Subgoal *1.2/2'
Subgoal *1.2/2''
Subgoal *1.2/2'''
Subgoal *1.2/2'4'
Subgoal *1.2/2'5'

*1.2.2 (Subgoal *1.2/2'5') is pushed for proof by induction.
Subgoal *1.2/1
Subgoal *1.2/1'
Subgoal *1.2/1''
Subgoal *1.2/1'''
Subgoal *1.2/1'4'

*1.2.3 (Subgoal *1.2/1'4') is pushed for proof by induction.

So we now return to *1.2.3, which is

(IMPLIES (AND (MEM X1 Z) (MEM X1 Y))
         (NOT (PERM Y Z))).
Subgoal *1.2.3/5
Subgoal *1.2.3/5'
Subgoal *1.2.3/5''
Subgoal *1.2.3/4
Subgoal *1.2.3/4'
Subgoal *1.2.3/3
Subgoal *1.2.3/3'
Subgoal *1.2.3/3''
Subgoal *1.2.3/3'''
Subgoal *1.2.3/3'4'
Subgoal *1.2.3/3'5'

*1.2.3.1 (Subgoal *1.2.3/3'5') is pushed for proof by
induction.
Subgoal *1.2.3/2
Subgoal *1.2.3/2'

Splitter note (see :DOC splitter) for Subgoal *1.2.3/2'
(2 subgoals).
  if-intro: ((:DEFINITION MEM))

Subgoal *1.2.3/2.2
Subgoal *1.2.3/2.2'
Subgoal *1.2.3/2.2''
Subgoal *1.2.3/2.2'''
Subgoal *1.2.3/2.2'4'

*1.2.3.2 (Subgoal *1.2.3/2.2'4') is pushed for proof
by induction.
Subgoal *1.2.3/2.1
Subgoal *1.2.3/2.1'
Subgoal *1.2.3/2.1''
Subgoal *1.2.3/2.1'''

*1.2.3.3 (Subgoal *1.2.3/2.1''') is pushed for proof
by induction.
Subgoal *1.2.3/1
Subgoal *1.2.3/1'

So we now return to *1.2.3.3, which is

(IMPLIES (AND (MEM Y1 Z)
              (NOT (MEM X1 DL))
              (MEM X1 Z)
              (MEM X1 Y2))
         (NOT (PERM Y2 DL))).

But the formula above is subsumed by *1.2.3.2, which
we'll try to prove later.  We therefore regard *1.2.3.3
as proved (pending the proof of the more general *1.2.3.2).

We next consider *1.2.3.2, which is

(IMPLIES (AND (NOT (MEM Y1 DL)) (MEM Y1 Z))
         (NOT (PERM Y2 DL))).
Subgoal *1.2.3.2/4
Subgoal *1.2.3.2/4'
Subgoal *1.2.3.2/3
Subgoal *1.2.3.2/3'
Subgoal *1.2.3.2/2
Subgoal *1.2.3.2/2'
Subgoal *1.2.3.2/2''
Subgoal *1.2.3.2/2'''
Subgoal *1.2.3.2/2'4'
Subgoal *1.2.3.2/2'5'

*1.2.3.2.1 (Subgoal *1.2.3.2/2'5') is pushed for proof
by induction.
Subgoal *1.2.3.2/1
Subgoal *1.2.3.2/1'
Subgoal *1.2.3.2/1''
Subgoal *1.2.3.2/1'''
Subgoal *1.2.3.2/1'4'

A goal of NIL, Subgoal *1.2.3.2/1'4', has been generated!
Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM PERM-TRANSITIVE ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEM)
        (:INDUCTION PERM)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION MEM))
Warnings:  Free
Time:  0.06 seconds (prove: 0.05, print: 0.01, other: 0.00)
Prover steps counted:  17384

---
The key checkpoint goals, below, may help you to debug
this failure.  See :DOC failure and see :DOC set-checkpoint-
summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(IMPLIES (AND (PERM X Y) (PERM Y Z))
         (PERM X Z))

*** Key checkpoints under a top-level induction ***
[NOTE: A goal of NIL was generated.  See :DOC nil-goal.]

Subgoal *1/5''
(IMPLIES (AND (CONSP X)
              (NOT (MEM (CAR X) Z))
              (MEM (CAR X) Y)
              (PERM (CDR X) (DEL (CAR X) Y)))
         (NOT (PERM Y Z)))

Subgoal *1/3''
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Z)
              (NOT (PERM (DEL (CAR X) Y) (DEL (CAR X) Z)))
              (MEM (CAR X) Y)
              (PERM (CDR X) (DEL (CAR X) Y))
              (PERM Y Z))
         (PERM (CDR X) (DEL (CAR X) Z)))

ACL2 Error in ( DEFTHM PERM-TRANSITIVE ...):  See :DOC
failure.

******** FAILED ********
ACL2 !>(defthm not-perm-if-different-members
	 ;; lemma for perm-transitive
	 (implies (and (not (mem a z))
		       (mem a y))
		  (equal (perm y z) nil)))

ACL2 Warning [Free] in ( DEFTHM NOT-PERM-IF-DIFFERENT-MEMBERS
...):  A :REWRITE rule generated from NOT-PERM-IF-DIFFERENT-MEMBERS
contains the free variable A.  This variable will be
chosen by searching for an instance of (NOT (MEM A Z))
in the context of the term being rewritten.  This is
generally a severe restriction on the applicability
of a :REWRITE rule.  See :DOC free-variables.

Goal'

([ A key checkpoint:

Goal'
(IMPLIES (AND (NOT (MEM A Z)) (MEM A Y))
         (NOT (PERM Y Z)))

*1 (Goal') is pushed for proof by induction.

])

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (PERM Y Z),
but modified to accommodate (MEM A Y).  These suggestions
were produced using the :induction rules MEM and PERM.
If we let (:P A Y Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ATOM Y))
                   (NOT (MEM (CAR Y) Z)))
              (:P A Y Z))
     (IMPLIES (AND (NOT (ATOM Y))
                   (MEM (CAR Y) Z)
                   (:P A (CDR Y) (DEL (CAR Y) Z)))
              (:P A Y Z))
     (IMPLIES (ATOM Y) (:P A Y Z))).
This induction is justified by the same argument used
to admit PERM.  Note, however, that the unmeasured variable
Z is being instantiated.  When applied to the goal at
hand the above induction scheme produces five nontautological
subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/2''
Subgoal *1/2'''
Subgoal *1/2'4'
Subgoal *1/2'5'

([ A key checkpoint while proving *1 (descended from
Goal'):

Subgoal *1/2''
(IMPLIES (AND (CONSP Y)
              (MEM (CAR Y) Z)
              (MEM A (DEL (CAR Y) Z))
              (NOT (MEM A Z))
              (MEM A (CDR Y)))
         (NOT (PERM (CDR Y) (DEL (CAR Y) Z))))

*1.1 (Subgoal *1/2'5') is pushed for proof by induction.

])
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(IMPLIES (AND (MEM Y1 Z)
              (MEM A DL)
              (NOT (MEM A Z))
              (MEM A Y2))
         (NOT (PERM Y2 DL))).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/5''
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/3''
Subgoal *1.1/3'''
Subgoal *1.1/3'4'
Subgoal *1.1/3'5'

*1.1.1 (Subgoal *1.1/3'5') is pushed for proof by induction.
Subgoal *1.1/2
Subgoal *1.1/2'

Splitter note (see :DOC splitter) for Subgoal *1.1/2'
(2 subgoals).
  if-intro: ((:DEFINITION MEM))

Subgoal *1.1/2.2
Subgoal *1.1/2.2'
Subgoal *1.1/2.2''
Subgoal *1.1/2.2'''
Subgoal *1.1/2.2'4'

*1.1.2 (Subgoal *1.1/2.2'4') is pushed for proof by
induction.
Subgoal *1.1/2.1
Subgoal *1.1/2.1'
Subgoal *1.1/2.1''
Subgoal *1.1/2.1'''

*1.1.3 (Subgoal *1.1/2.1''') is pushed for proof by
induction.
Subgoal *1.1/1
Subgoal *1.1/1'

So we now return to *1.1.3, which is

(IMPLIES (AND (MEM Y3 DL)
              (NOT (MEM A DL0))
              (MEM Y1 Z)
              (MEM A DL)
              (NOT (MEM A Z))
              (MEM A Y4))
         (NOT (PERM Y4 DL0))).

But the formula above is subsumed by *1.1.2, which we'll
try to prove later.  We therefore regard *1.1.3 as proved
(pending the proof of the more general *1.1.2).

We next consider *1.1.2, which is

(IMPLIES (AND (NOT (MEM Y3 DL0))
              (MEM Y1 Z)
              (MEM Y3 DL)
              (NOT (MEM Y3 Z)))
         (NOT (PERM Y4 DL0))).
Subgoal *1.1.2/4
Subgoal *1.1.2/4'
Subgoal *1.1.2/3
Subgoal *1.1.2/3'
Subgoal *1.1.2/2
Subgoal *1.1.2/2'
Subgoal *1.1.2/2''
Subgoal *1.1.2/2'''
Subgoal *1.1.2/2'4'
Subgoal *1.1.2/2'5'

*1.1.2.1 (Subgoal *1.1.2/2'5') is pushed for proof by
induction.
Subgoal *1.1.2/1
Subgoal *1.1.2/1'
Subgoal *1.1.2/1''
Subgoal *1.1.2/1'''
Subgoal *1.1.2/1'4'

*1.1.2.2 (Subgoal *1.1.2/1'4') is pushed for proof by
induction.

So we now return to *1.1.2.2, which is

(IMPLIES (AND (MEM Y1 Z) (MEM Y3 DL))
         (MEM Y3 Z)).
Subgoal *1.1.2.2/4
Subgoal *1.1.2.2/4'
Subgoal *1.1.2.2/3
Subgoal *1.1.2.2/3'
Subgoal *1.1.2.2/3''
Subgoal *1.1.2.2/3'''
Subgoal *1.1.2.2/3'4'
Subgoal *1.1.2.2/3'5'

*1.1.2.2.1 (Subgoal *1.1.2.2/3'5') is pushed for proof
by induction.
Subgoal *1.1.2.2/2
Subgoal *1.1.2.2/2'
Subgoal *1.1.2.2/1
Subgoal *1.1.2.2/1'

So we now return to *1.1.2.2.1, which is

(IMPLIES (AND (NOT (EQUAL Y3 Z1))
              (NOT (MEM Z1 Z2))
              (MEM Y3 DL))
         (MEM Y3 Z2)).
Subgoal *1.1.2.2.1/4
Subgoal *1.1.2.2.1/4'
Subgoal *1.1.2.2.1/3
Subgoal *1.1.2.2.1/3'
Subgoal *1.1.2.2.1/2
Subgoal *1.1.2.2.1/2'
Subgoal *1.1.2.2.1/1
Subgoal *1.1.2.2.1/1'
Subgoal *1.1.2.2.1/1''
Subgoal *1.1.2.2.1/1'''

*1.1.2.2.1.1 (Subgoal *1.1.2.2.1/1''') is pushed for
proof by induction.

So we now return to *1.1.2.2.1.1, which is

(IMPLIES (NOT (EQUAL Y3 Z1))
         (NOT (MEM Y3 DL))).
Subgoal *1.1.2.2.1.1/3
Subgoal *1.1.2.2.1.1/3'
Subgoal *1.1.2.2.1.1/2
Subgoal *1.1.2.2.1.1/2'
Subgoal *1.1.2.2.1.1/2''
Subgoal *1.1.2.2.1.1/2'''
Subgoal *1.1.2.2.1.1/2'4'
Subgoal *1.1.2.2.1.1/2'5'

A goal of NIL, Subgoal *1.1.2.2.1.1/2'5', has been generated!
Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM NOT-PERM-IF-DIFFERENT-MEMBERS ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEM)
        (:INDUCTION PERM)
        (:TYPE-PRESCRIPTION MEM))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION MEM))
Warnings:  Free
Time:  0.06 seconds (prove: 0.05, print: 0.01, other: 0.00)
Prover steps counted:  12720

---
The key checkpoint goals, below, may help you to debug
this failure.  See :DOC failure and see :DOC set-checkpoint-
summary-limit.
---

*** Key checkpoint at the top level: ***

Goal'
(IMPLIES (AND (NOT (MEM A Z)) (MEM A Y))
         (NOT (PERM Y Z)))

*** Key checkpoint under a top-level induction ***
[NOTE: A goal of NIL was generated.  See :DOC nil-goal.]

Subgoal *1/2''
(IMPLIES (AND (CONSP Y)
              (MEM (CAR Y) Z)
              (MEM A (DEL (CAR Y) Z))
              (NOT (MEM A Z))
              (MEM A (CDR Y)))
         (NOT (PERM (CDR Y) (DEL (CAR Y) Z))))

ACL2 Error in ( DEFTHM NOT-PERM-IF-DIFFERENT-MEMBERS
...):  See :DOC failure.

******** FAILED ********
ACL2 !>(defthm mem-del-implies-mem
	 ;; lemma for not-perm-if-different-members
	 (implies (not (mem a z))
		  (equal (mem a (del b z))
			 nil)))
Goal'

([ A key checkpoint:

Goal'
(IMPLIES (NOT (MEM A Z))
         (NOT (MEM A (DEL B Z))))

*1 (Goal') is pushed for proof by induction.

])

Perhaps we can prove *1 by induction.  Two induction
schemes are suggested by this conjecture.  These merge
into one derived induction scheme.  

We will induct according to a scheme suggested by (DEL B Z),
but modified to accommodate (MEM A Z).  These suggestions
were produced using the :induction rules DEL and MEM.
If we let (:P A B Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ATOM Z))
                   (NOT (EQUAL B (CAR Z)))
                   (:P A B (CDR Z)))
              (:P A B Z))
     (IMPLIES (AND (NOT (ATOM Z)) (EQUAL B (CAR Z)))
              (:P A B Z))
     (IMPLIES (ATOM Z) (:P A B Z))).
This induction is justified by the same argument used
to admit DEL.  When applied to the goal at hand the
above induction scheme produces four nontautological
subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM MEM-DEL-IMPLIES-MEM ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION DEL)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DEL)
        (:INDUCTION MEM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:TYPE-PRESCRIPTION MEM))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  724
 MEM-DEL-IMPLIES-MEM
ACL2 !>(defthm not-perm-if-different-members
	 ;; lemma for perm-transitive
	 (implies (and (not (mem a z))
		       (mem a y))
		  (equal (perm y z) nil)))

ACL2 Warning [Free] in ( DEFTHM NOT-PERM-IF-DIFFERENT-MEMBERS
...):  A :REWRITE rule generated from NOT-PERM-IF-DIFFERENT-MEMBERS
contains the free variable A.  This variable will be
chosen by searching for an instance of (NOT (MEM A Z))
in the context of the term being rewritten.  This is
generally a severe restriction on the applicability
of a :REWRITE rule.  See :DOC free-variables.

Goal'

([ A key checkpoint:

Goal'
(IMPLIES (AND (NOT (MEM A Z)) (MEM A Y))
         (NOT (PERM Y Z)))

*1 (Goal') is pushed for proof by induction.

])

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (PERM Y Z),
but modified to accommodate (MEM A Y).  These suggestions
were produced using the :induction rules MEM and PERM.
If we let (:P A Y Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ATOM Y))
                   (NOT (MEM (CAR Y) Z)))
              (:P A Y Z))
     (IMPLIES (AND (NOT (ATOM Y))
                   (MEM (CAR Y) Z)
                   (:P A (CDR Y) (DEL (CAR Y) Z)))
              (:P A Y Z))
     (IMPLIES (ATOM Y) (:P A Y Z))).
This induction is justified by the same argument used
to admit PERM.  Note, however, that the unmeasured variable
Z is being instantiated.  When applied to the goal at
hand the above induction scheme produces five nontautological
subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal' is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM NOT-PERM-IF-DIFFERENT-MEMBERS ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEM)
        (:INDUCTION PERM)
        (:REWRITE MEM-DEL-IMPLIES-MEM)
        (:TYPE-PRESCRIPTION MEM))
Warnings:  Free
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1263
 NOT-PERM-IF-DIFFERENT-MEMBERS
ACL2 !>(defthm perm-transitive ; OUR GOAL for this demo
	 (implies (and (perm x y) (perm y z))
		  (perm x z)))

ACL2 Warning [Free] in ( DEFTHM PERM-TRANSITIVE ...):
A :REWRITE rule generated from PERM-TRANSITIVE contains
the free variable Y.  This variable will be chosen by
searching for an instance of (PERM X Y) in the context
of the term being rewritten.  This is generally a severe
restriction on the applicability of a :REWRITE rule.
See :DOC free-variables.


*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (PERM X Z),
but modified to accommodate (PERM X Y).  These suggestions
were produced using the :induction rule PERM.  If we
let (:P X Y Z) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ATOM X))
                   (NOT (MEM (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (AND (NOT (ATOM X))
                   (MEM (CAR X) Z)
                   (:P (CDR X)
                       (DEL (CAR X) Y)
                       (DEL (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (ATOM X) (:P X Y Z))).
This induction is justified by the same argument used
to admit PERM.  Note, however, that the unmeasured variables
Y and Z are being instantiated.  When applied to the
goal at hand the above induction scheme produces five
nontautological subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/3'''
Subgoal *1/3'4'
Subgoal *1/3'5'

([ A key checkpoint while proving *1 (descended from
Goal):

Subgoal *1/3''
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Z)
              (NOT (PERM (DEL (CAR X) Y) (DEL (CAR X) Z)))
              (MEM (CAR X) Y)
              (PERM (CDR X) (DEL (CAR X) Y))
              (PERM Y Z))
         (PERM (CDR X) (DEL (CAR X) Z)))

*1.1 (Subgoal *1/3'5') is pushed for proof by induction.

])
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(IMPLIES (AND (MEM X1 Z)
              (NOT (PERM DL0 DL))
              (MEM X1 Y)
              (PERM X2 DL0)
              (PERM Y Z))
         (PERM X2 DL)).
Subgoal *1.1/5
Subgoal *1.1/5'
Subgoal *1.1/5''
Subgoal *1.1/5'''
Subgoal *1.1/5'4'
Subgoal *1.1/5'5'

*1.1.1 (Subgoal *1.1/5'5') is pushed for proof by induction.
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
Subgoal *1.1/2'5'

*1.1.2 (Subgoal *1.1/2'5') is pushed for proof by induction.
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''
Subgoal *1.1/1'4'

*1.1.3 (Subgoal *1.1/1'4') is pushed for proof by induction.

So we now return to *1.1.3, which is

(IMPLIES (AND (MEM X1 Z) (MEM X1 Y))
         (NOT (PERM Y Z))).
Subgoal *1.1.3/5
Subgoal *1.1.3/5'
Subgoal *1.1.3/4
Subgoal *1.1.3/4'
Subgoal *1.1.3/3
Subgoal *1.1.3/3'
Subgoal *1.1.3/3''
Subgoal *1.1.3/3'''
Subgoal *1.1.3/3'4'
Subgoal *1.1.3/3'5'

*1.1.3.1 (Subgoal *1.1.3/3'5') is pushed for proof by
induction.
Subgoal *1.1.3/2
Subgoal *1.1.3/2'

Splitter note (see :DOC splitter) for Subgoal *1.1.3/2'
(2 subgoals).
  if-intro: ((:DEFINITION MEM))

Subgoal *1.1.3/2.2
Subgoal *1.1.3/2.2'
Subgoal *1.1.3/2.2''
Subgoal *1.1.3/2.2'''
Subgoal *1.1.3/2.2'4'

*1.1.3.2 (Subgoal *1.1.3/2.2'4') is pushed for proof
by induction.
Subgoal *1.1.3/2.1
Subgoal *1.1.3/1
Subgoal *1.1.3/1'

So we now return to *1.1.3.2, which is

(IMPLIES (AND (NOT (MEM Y1 DL)) (MEM Y1 Z))
         (NOT (PERM Y2 DL))).
Subgoal *1.1.3.2/4
Subgoal *1.1.3.2/4'
Subgoal *1.1.3.2/3
Subgoal *1.1.3.2/3'
Subgoal *1.1.3.2/2
Subgoal *1.1.3.2/2'
Subgoal *1.1.3.2/1
Subgoal *1.1.3.2/1'
Subgoal *1.1.3.2/1''
Subgoal *1.1.3.2/1'''
Subgoal *1.1.3.2/1'4'

A goal of NIL, Subgoal *1.1.3.2/1'4', has been generated!
Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM PERM-TRANSITIVE ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION MEM)
        (:INDUCTION PERM)
        (:REWRITE MEM-DEL-IMPLIES-MEM)
        (:REWRITE NOT-PERM-IF-DIFFERENT-MEMBERS)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION MEM))
Warnings:  Free
Time:  0.05 seconds (prove: 0.04, print: 0.01, other: 0.00)
Prover steps counted:  15054

---
The key checkpoint goals, below, may help you to debug
this failure.  See :DOC failure and see :DOC set-checkpoint-
summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(IMPLIES (AND (PERM X Y) (PERM Y Z))
         (PERM X Z))

*** Key checkpoint under a top-level induction ***
[NOTE: A goal of NIL was generated.  See :DOC nil-goal.]

Subgoal *1/3''
(IMPLIES (AND (CONSP X)
              (MEM (CAR X) Z)
              (NOT (PERM (DEL (CAR X) Y) (DEL (CAR X) Z)))
              (MEM (CAR X) Y)
              (PERM (CDR X) (DEL (CAR X) Y))
              (PERM Y Z))
         (PERM (CDR X) (DEL (CAR X) Z)))

ACL2 Error in ( DEFTHM PERM-TRANSITIVE ...):  See :DOC
failure.

******** FAILED ********
ACL2 !>(defthm perm-del-del ; lemma for perm-transitive
	 (implies (perm y z)
		  (perm (del a y) (del a z))))

*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (DEL A Y),
but modified to accommodate (PERM Y Z).  These suggestions
were produced using the :induction rules DEL and PERM.
If we let (:P A Y Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ATOM Y))
                   (NOT (EQUAL A (CAR Y)))
                   (:P A (CDR Y) (DEL (CAR Y) Z)))
              (:P A Y Z))
     (IMPLIES (AND (NOT (ATOM Y)) (EQUAL A (CAR Y)))
              (:P A Y Z))
     (IMPLIES (ATOM Y) (:P A Y Z))).
This induction is justified by the same argument used
to admit DEL.  Note, however, that the unmeasured variable
Z is being instantiated.  When applied to the goal at
hand the above induction scheme produces four nontautological
subgoals.
Subgoal *1/4
Subgoal *1/4'

Splitter note (see :DOC splitter) for Subgoal *1/4'
(2 subgoals).
  if-intro: ((:DEFINITION PERM))

Subgoal *1/4.2
Subgoal *1/4.2'
Subgoal *1/4.2''
Subgoal *1/4.2'''

([ A key checkpoint while proving *1 (descended from
Goal):

Subgoal *1/4.2
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL A (CAR Y)))
              (PERM (DEL A (CDR Y))
                    (DEL A (DEL (CAR Y) Z)))
              (MEM (CAR Y) Z)
              (PERM (CDR Y) (DEL (CAR Y) Z)))
         (MEM (CAR Y) (DEL A Z)))

*1.1 (Subgoal *1/4.2''') is pushed for proof by induction.

])
Subgoal *1/4.1
Subgoal *1/4.1'
Subgoal *1/4.1''
Subgoal *1/4.1'''

([ A key checkpoint while proving *1 (descended from
Goal):

Subgoal *1/4.1
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL A (CAR Y)))
              (PERM (DEL A (CDR Y))
                    (DEL A (DEL (CAR Y) Z)))
              (MEM (CAR Y) Z)
              (PERM (CDR Y) (DEL (CAR Y) Z)))
         (PERM (DEL A (CDR Y))
               (DEL (CAR Y) (DEL A Z))))

*1.2 (Subgoal *1/4.1''') is pushed for proof by induction.

])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.2, which is

(IMPLIES (AND (NOT (EQUAL A Y1))
              (PERM DL (DEL A DL0))
              (MEM Y1 Z)
              (PERM Y2 DL0))
         (PERM DL (DEL Y1 (DEL A Z)))).
Subgoal *1.2/4
Subgoal *1.2/4'
Subgoal *1.2/4''
Subgoal *1.2/4'''
Subgoal *1.2/4'4'
Subgoal *1.2/4'5'
Subgoal *1.2/4'6'

*1.2.1 (Subgoal *1.2/4'6') is pushed for proof by induction.
Subgoal *1.2/3
Subgoal *1.2/3'
Subgoal *1.2/3''
Subgoal *1.2/3'''
Subgoal *1.2/3'4'
Subgoal *1.2/3'5'
Subgoal *1.2/3'6'
Subgoal *1.2/3'7'

*1.2.2 (Subgoal *1.2/3'7') is pushed for proof by induction.
Subgoal *1.2/2
Subgoal *1.2/2'
Subgoal *1.2/2''
Subgoal *1.2/2'''
Subgoal *1.2/2'4'
Subgoal *1.2/2'5'
Subgoal *1.2/2'6'
Subgoal *1.2/2'7'

*1.2.3 (Subgoal *1.2/2'7') is pushed for proof by induction.
Subgoal *1.2/1
Subgoal *1.2/1'
Subgoal *1.2/1''
Subgoal *1.2/1'''

*1.2.4 (Subgoal *1.2/1''') is pushed for proof by induction.

So we now return to *1.2.4, which is

(IMPLIES (AND (NOT (EQUAL A Y1))
              (NOT (CONSP (DEL A DL0)))
              (MEM Y1 Z)
              (PERM Y2 DL0))
         (NOT (CONSP (DEL Y1 (DEL A Z))))).
Subgoal *1.2.4/4
Subgoal *1.2.4/4'
Subgoal *1.2.4/3
Subgoal *1.2.4/3'
Subgoal *1.2.4/2
Subgoal *1.2.4/2'
Subgoal *1.2.4/2''
Subgoal *1.2.4/2'''
Subgoal *1.2.4/2'4'
Subgoal *1.2.4/2'5'

*1.2.4.1 (Subgoal *1.2.4/2'5') is pushed for proof by
induction.
Subgoal *1.2.4/1
Subgoal *1.2.4/1'
Subgoal *1.2.4/1''
Subgoal *1.2.4/1'''
Subgoal *1.2.4/1'4'

*1.2.4.2 (Subgoal *1.2.4/1'4') is pushed for proof by
induction.

So we now return to *1.2.4.2, which is

(IMPLIES (AND (NOT (EQUAL A Y1)) (MEM Y1 Z))
         (NOT (CONSP (DEL Y1 (DEL A Z))))).
Subgoal *1.2.4.2/4
Subgoal *1.2.4.2/4'

Splitter note (see :DOC splitter) for Subgoal *1.2.4.2/4'
(3 subgoals).
  if-intro: ((:DEFINITION DEL) (:DEFINITION MEM))

Subgoal *1.2.4.2/4.3
Subgoal *1.2.4.2/4.3'
Subgoal *1.2.4.2/4.3''
Subgoal *1.2.4.2/4.3'''
Subgoal *1.2.4.2/4.3'4'

*1.2.4.2.1 (Subgoal *1.2.4.2/4.3'4') is pushed for proof
by induction.
Subgoal *1.2.4.2/4.2
Subgoal *1.2.4.2/4.2'
Subgoal *1.2.4.2/4.2''
Subgoal *1.2.4.2/4.2'''
Subgoal *1.2.4.2/4.2'4'

*1.2.4.2.2 (Subgoal *1.2.4.2/4.2'4') is pushed for proof
by induction.
Subgoal *1.2.4.2/4.1
Subgoal *1.2.4.2/4.1'
Subgoal *1.2.4.2/4.1''
Subgoal *1.2.4.2/4.1'''

*1.2.4.2.3 (Subgoal *1.2.4.2/4.1''') is pushed for proof
by induction.
Subgoal *1.2.4.2/3
Subgoal *1.2.4.2/3'
Subgoal *1.2.4.2/3''
Subgoal *1.2.4.2/3'''
Subgoal *1.2.4.2/3'4'
Subgoal *1.2.4.2/3'5'

*1.2.4.2.4 (Subgoal *1.2.4.2/3'5') is pushed for proof
by induction.
Subgoal *1.2.4.2/2
Subgoal *1.2.4.2/2'
Subgoal *1.2.4.2/2''
Subgoal *1.2.4.2/2'''
Subgoal *1.2.4.2/2'4'

*1.2.4.2.5 (Subgoal *1.2.4.2/2'4') is pushed for proof
by induction.
Subgoal *1.2.4.2/1
Subgoal *1.2.4.2/1'

So we now return to *1.2.4.2.5, which is

(IMPLIES (AND (NOT (EQUAL Z1 Y1)) (MEM Y1 Z2))
         (NOT (CONSP (DEL Y1 Z2)))).
Subgoal *1.2.4.2.5/4
Subgoal *1.2.4.2.5/4'
Subgoal *1.2.4.2.5/4''
Subgoal *1.2.4.2.5/4'''
Subgoal *1.2.4.2.5/4'4'

*1.2.4.2.5.1 (Subgoal *1.2.4.2.5/4'4') is pushed for
proof by induction.
Subgoal *1.2.4.2.5/3
Subgoal *1.2.4.2.5/3'
Subgoal *1.2.4.2.5/2
Subgoal *1.2.4.2.5/2'
Subgoal *1.2.4.2.5/2''
Subgoal *1.2.4.2.5/2'''
Subgoal *1.2.4.2.5/2'4'
Subgoal *1.2.4.2.5/2'5'

A goal of NIL, Subgoal *1.2.4.2.5/2'5', has been generated!
Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM PERM-DEL-DEL ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION DEL)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART PERM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DEL)
        (:INDUCTION MEM)
        (:INDUCTION PERM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE NOT-PERM-IF-DIFFERENT-MEMBERS)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION DEL)
             (:DEFINITION MEM)
             (:DEFINITION PERM))
Time:  0.08 seconds (prove: 0.07, print: 0.01, other: 0.00)
Prover steps counted:  27430

---
The key checkpoint goals, below, may help you to debug
this failure.  See :DOC failure and see :DOC set-checkpoint-
summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(IMPLIES (PERM Y Z)
         (PERM (DEL A Y) (DEL A Z)))

*** Key checkpoints under a top-level induction ***
[NOTE: A goal of NIL was generated.  See :DOC nil-goal.]

Subgoal *1/4.2
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL A (CAR Y)))
              (PERM (DEL A (CDR Y))
                    (DEL A (DEL (CAR Y) Z)))
              (MEM (CAR Y) Z)
              (PERM (CDR Y) (DEL (CAR Y) Z)))
         (MEM (CAR Y) (DEL A Z)))

Subgoal *1/4.1
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL A (CAR Y)))
              (PERM (DEL A (CDR Y))
                    (DEL A (DEL (CAR Y) Z)))
              (MEM (CAR Y) Z)
              (PERM (CDR Y) (DEL (CAR Y) Z)))
         (PERM (DEL A (CDR Y))
               (DEL (CAR Y) (DEL A Z))))

ACL2 Error in ( DEFTHM PERM-DEL-DEL ...):  See :DOC
failure.

******** FAILED ********
ACL2 !>(defthm mem-del
	 ;; lemma for perm-del-del
	 (implies (not (equal a b))
		  (equal (mem b (del a z))
			 (mem b z))))

*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Two induction
schemes are suggested by this conjecture.  These merge
into one derived induction scheme.  

We will induct according to a scheme suggested by (MEM B Z),
but modified to accommodate (DEL A Z).  These suggestions
were produced using the :induction rules DEL and MEM.
If we let (:P A B Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ATOM Z))
                   (NOT (EQUAL B (CAR Z)))
                   (:P A B (CDR Z)))
              (:P A B Z))
     (IMPLIES (AND (NOT (ATOM Z)) (EQUAL B (CAR Z)))
              (:P A B Z))
     (IMPLIES (ATOM Z) (:P A B Z))).
This induction is justified by the same argument used
to admit MEM.  When applied to the goal at hand the
above induction scheme produces three nontautological
subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM MEM-DEL ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION DEL)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DEL)
        (:INDUCTION MEM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  837
 MEM-DEL
ACL2 !>(defthm perm-del-del
	 ;; lemma for perm-transitive
	 (implies (perm y z)
		  (perm (del a y) (del a z))))

*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (DEL A Y),
but modified to accommodate (PERM Y Z).  These suggestions
were produced using the :induction rules DEL and PERM.
If we let (:P A Y Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ATOM Y))
                   (NOT (EQUAL A (CAR Y)))
                   (:P A (CDR Y) (DEL (CAR Y) Z)))
              (:P A Y Z))
     (IMPLIES (AND (NOT (ATOM Y)) (EQUAL A (CAR Y)))
              (:P A Y Z))
     (IMPLIES (ATOM Y) (:P A Y Z))).
This induction is justified by the same argument used
to admit DEL.  Note, however, that the unmeasured variable
Z is being instantiated.  When applied to the goal at
hand the above induction scheme produces four nontautological
subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/4''
Subgoal *1/4'''
Subgoal *1/4'4'
Subgoal *1/4'5'

([ A key checkpoint while proving *1 (descended from
Goal):

Subgoal *1/4''
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL A (CAR Y)))
              (PERM (DEL A (CDR Y))
                    (DEL A (DEL (CAR Y) Z)))
              (MEM (CAR Y) Z)
              (PERM (CDR Y) (DEL (CAR Y) Z)))
         (PERM (DEL A (CDR Y))
               (DEL (CAR Y) (DEL A Z))))

*1.1 (Subgoal *1/4'5') is pushed for proof by induction.

])
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

So we now return to *1.1, which is

(IMPLIES (AND (NOT (EQUAL A Y1))
              (PERM DL (DEL A DL0))
              (MEM Y1 Z)
              (PERM Y2 DL0))
         (PERM DL (DEL Y1 (DEL A Z)))).
Subgoal *1.1/4
Subgoal *1.1/4'
Subgoal *1.1/4''
Subgoal *1.1/4'''
Subgoal *1.1/4'4'
Subgoal *1.1/4'5'
Subgoal *1.1/4'6'

*1.1.1 (Subgoal *1.1/4'6') is pushed for proof by induction.
Subgoal *1.1/3
Subgoal *1.1/3'
Subgoal *1.1/3''
Subgoal *1.1/3'''
Subgoal *1.1/3'4'
Subgoal *1.1/3'5'
Subgoal *1.1/3'6'
Subgoal *1.1/3'7'

*1.1.2 (Subgoal *1.1/3'7') is pushed for proof by induction.
Subgoal *1.1/2
Subgoal *1.1/2'
Subgoal *1.1/2''
Subgoal *1.1/2'''
Subgoal *1.1/2'4'
Subgoal *1.1/2'5'
Subgoal *1.1/2'6'
Subgoal *1.1/2'7'

*1.1.3 (Subgoal *1.1/2'7') is pushed for proof by induction.
Subgoal *1.1/1
Subgoal *1.1/1'
Subgoal *1.1/1''
Subgoal *1.1/1'''

*1.1.4 (Subgoal *1.1/1''') is pushed for proof by induction.

So we now return to *1.1.4, which is

(IMPLIES (AND (NOT (EQUAL A Y1))
              (NOT (CONSP (DEL A DL0)))
              (MEM Y1 Z)
              (PERM Y2 DL0))
         (NOT (CONSP (DEL Y1 (DEL A Z))))).
Subgoal *1.1.4/4
Subgoal *1.1.4/4'
Subgoal *1.1.4/3
Subgoal *1.1.4/3'
Subgoal *1.1.4/2
Subgoal *1.1.4/2'
Subgoal *1.1.4/2''
Subgoal *1.1.4/2'''
Subgoal *1.1.4/2'4'
Subgoal *1.1.4/2'5'

*1.1.4.1 (Subgoal *1.1.4/2'5') is pushed for proof by
induction.
Subgoal *1.1.4/1
Subgoal *1.1.4/1'
Subgoal *1.1.4/1''
Subgoal *1.1.4/1'''
Subgoal *1.1.4/1'4'

*1.1.4.2 (Subgoal *1.1.4/1'4') is pushed for proof by
induction.

So we now return to *1.1.4.2, which is

(IMPLIES (AND (NOT (EQUAL A Y1)) (MEM Y1 Z))
         (NOT (CONSP (DEL Y1 (DEL A Z))))).
Subgoal *1.1.4.2/4
Subgoal *1.1.4.2/4'

Splitter note (see :DOC splitter) for Subgoal *1.1.4.2/4'
(3 subgoals).
  if-intro: ((:DEFINITION DEL) (:DEFINITION MEM))

Subgoal *1.1.4.2/4.3
Subgoal *1.1.4.2/4.3'
Subgoal *1.1.4.2/4.3''
Subgoal *1.1.4.2/4.3'''
Subgoal *1.1.4.2/4.3'4'

*1.1.4.2.1 (Subgoal *1.1.4.2/4.3'4') is pushed for proof
by induction.
Subgoal *1.1.4.2/4.2
Subgoal *1.1.4.2/4.2'
Subgoal *1.1.4.2/4.2''
Subgoal *1.1.4.2/4.2'''
Subgoal *1.1.4.2/4.2'4'

*1.1.4.2.2 (Subgoal *1.1.4.2/4.2'4') is pushed for proof
by induction.
Subgoal *1.1.4.2/4.1
Subgoal *1.1.4.2/4.1'
Subgoal *1.1.4.2/4.1''
Subgoal *1.1.4.2/4.1'''

*1.1.4.2.3 (Subgoal *1.1.4.2/4.1''') is pushed for proof
by induction.
Subgoal *1.1.4.2/3
Subgoal *1.1.4.2/3'
Subgoal *1.1.4.2/3''
Subgoal *1.1.4.2/3'''
Subgoal *1.1.4.2/3'4'
Subgoal *1.1.4.2/3'5'

*1.1.4.2.4 (Subgoal *1.1.4.2/3'5') is pushed for proof
by induction.
Subgoal *1.1.4.2/2
Subgoal *1.1.4.2/2'
Subgoal *1.1.4.2/2''
Subgoal *1.1.4.2/2'''
Subgoal *1.1.4.2/2'4'

*1.1.4.2.5 (Subgoal *1.1.4.2/2'4') is pushed for proof
by induction.
Subgoal *1.1.4.2/1
Subgoal *1.1.4.2/1'

So we now return to *1.1.4.2.5, which is

(IMPLIES (AND (NOT (EQUAL Z1 Y1)) (MEM Y1 Z2))
         (NOT (CONSP (DEL Y1 Z2)))).
Subgoal *1.1.4.2.5/4
Subgoal *1.1.4.2.5/4'
Subgoal *1.1.4.2.5/4''
Subgoal *1.1.4.2.5/4'''
Subgoal *1.1.4.2.5/4'4'

*1.1.4.2.5.1 (Subgoal *1.1.4.2.5/4'4') is pushed for
proof by induction.
Subgoal *1.1.4.2.5/3
Subgoal *1.1.4.2.5/3'
Subgoal *1.1.4.2.5/2
Subgoal *1.1.4.2.5/2'
Subgoal *1.1.4.2.5/2''
Subgoal *1.1.4.2.5/2'''
Subgoal *1.1.4.2.5/2'4'
Subgoal *1.1.4.2.5/2'5'

A goal of NIL, Subgoal *1.1.4.2.5/2'5', has been generated!
Obviously, the proof attempt has failed.

Summary
Form:  ( DEFTHM PERM-DEL-DEL ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION DEL)
        (:DEFINITION MEM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:ELIM CAR-CDR-ELIM)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART PERM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DEL)
        (:INDUCTION MEM)
        (:INDUCTION PERM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE MEM-DEL)
        (:REWRITE NOT-PERM-IF-DIFFERENT-MEMBERS)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION DEL) (:DEFINITION MEM))
Time:  0.08 seconds (prove: 0.07, print: 0.01, other: 0.00)
Prover steps counted:  26139

---
The key checkpoint goals, below, may help you to debug
this failure.  See :DOC failure and see :DOC set-checkpoint-
summary-limit.
---

*** Key checkpoint at the top level: ***

Goal
(IMPLIES (PERM Y Z)
         (PERM (DEL A Y) (DEL A Z)))

*** Key checkpoint under a top-level induction ***
[NOTE: A goal of NIL was generated.  See :DOC nil-goal.]

Subgoal *1/4''
(IMPLIES (AND (CONSP Y)
              (NOT (EQUAL A (CAR Y)))
              (PERM (DEL A (CDR Y))
                    (DEL A (DEL (CAR Y) Z)))
              (MEM (CAR Y) Z)
              (PERM (CDR Y) (DEL (CAR Y) Z)))
         (PERM (DEL A (CDR Y))
               (DEL (CAR Y) (DEL A Z))))

ACL2 Error in ( DEFTHM PERM-DEL-DEL ...):  See :DOC
failure.

******** FAILED ********
ACL2 !>(defthm del-del
	 ;; lemma for perm-del-del (NOTE: DOESN'T LOOP!)
	 (equal (del a (del b x))
		(del b (del a x))))

*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Two induction
schemes are suggested by this conjecture.  These merge
into one derived induction scheme.  

We will induct according to a scheme suggested by (DEL A X),
but modified to accommodate (DEL B X).  These suggestions
were produced using the :induction rule DEL.  If we
let (:P A B X) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ATOM X))
                   (NOT (EQUAL A (CAR X)))
                   (:P A B (CDR X)))
              (:P A B X))
     (IMPLIES (AND (NOT (ATOM X)) (EQUAL A (CAR X)))
              (:P A B X))
     (IMPLIES (ATOM X) (:P A B X))).
This induction is justified by the same argument used
to admit DEL.  When applied to the goal at hand the
above induction scheme produces three nontautological
subgoals.
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/3''
Subgoal *1/2
Subgoal *1/2'

Splitter note (see :DOC splitter) for Subgoal *1/2'
(2 subgoals).
  if-intro: ((:DEFINITION DEL))

Subgoal *1/2.2
Subgoal *1/2.1
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

Summary
Form:  ( DEFTHM DEL-DEL ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION DEL)
        (:DEFINITION NOT)
        (:EXECUTABLE-COUNTERPART CONSP)
        (:EXECUTABLE-COUNTERPART EQUAL)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DEL)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS))
Splitter rules (see :DOC splitter):
  if-intro: ((:DEFINITION DEL))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1148
 DEL-DEL
ACL2 !>(defthm perm-del-del
	 ;; lemma for perm-transitive
	 (implies (perm y z)
		  (perm (del a y) (del a z))))

*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (DEL A Y),
but modified to accommodate (PERM Y Z).  These suggestions
were produced using the :induction rules DEL and PERM.
If we let (:P A Y Z) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (AND (NOT (ATOM Y))
                   (NOT (EQUAL A (CAR Y)))
                   (:P A (CDR Y) (DEL (CAR Y) Z)))
              (:P A Y Z))
     (IMPLIES (AND (NOT (ATOM Y)) (EQUAL A (CAR Y)))
              (:P A Y Z))
     (IMPLIES (ATOM Y) (:P A Y Z))).
This induction is justified by the same argument used
to admit DEL.  Note, however, that the unmeasured variable
Z is being instantiated.  When applied to the goal at
hand the above induction scheme produces four nontautological
subgoals.
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

The storage of PERM-DEL-DEL depends upon the :type-
prescription rule PERM.

Summary
Form:  ( DEFTHM PERM-DEL-DEL ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION DEL)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:EXECUTABLE-COUNTERPART PERM)
        (:FAKE-RUNE-FOR-TYPE-SET NIL)
        (:INDUCTION DEL)
        (:INDUCTION PERM)
        (:REWRITE CAR-CONS)
        (:REWRITE CDR-CONS)
        (:REWRITE DEL-DEL)
        (:REWRITE MEM-DEL)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1374
 PERM-DEL-DEL
ACL2 !>(defthm perm-transitive
	 (implies (and (perm x y) (perm y z))
		  (perm x z)))

ACL2 Warning [Free] in ( DEFTHM PERM-TRANSITIVE ...):
A :REWRITE rule generated from PERM-TRANSITIVE contains
the free variable Y.  This variable will be chosen by
searching for an instance of (PERM X Y) in the context
of the term being rewritten.  This is generally a severe
restriction on the applicability of a :REWRITE rule.
See :DOC free-variables.


*1 (the initial Goal, a key checkpoint) is pushed for
proof by induction.

Perhaps we can prove *1 by induction.  Three induction
schemes are suggested by this conjecture.  These merge
into two derived induction schemes.  However, one of
these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (PERM X Z),
but modified to accommodate (PERM X Y).  These suggestions
were produced using the :induction rule PERM.  If we
let (:P X Y Z) denote *1 above then the induction scheme
we'll use is
(AND (IMPLIES (AND (NOT (ATOM X))
                   (NOT (MEM (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (AND (NOT (ATOM X))
                   (MEM (CAR X) Z)
                   (:P (CDR X)
                       (DEL (CAR X) Y)
                       (DEL (CAR X) Z)))
              (:P X Y Z))
     (IMPLIES (ATOM X) (:P X Y Z))).
This induction is justified by the same argument used
to admit PERM.  Note, however, that the unmeasured variables
Y and Z are being instantiated.  When applied to the
goal at hand the above induction scheme produces five
nontautological subgoals.
Subgoal *1/5
Subgoal *1/5'
Subgoal *1/4
Subgoal *1/4'
Subgoal *1/3
Subgoal *1/3'
Subgoal *1/2
Subgoal *1/2'
Subgoal *1/1
Subgoal *1/1'

*1 is COMPLETED!
Thus key checkpoint Goal is COMPLETED!

Q.E.D.

The storage of PERM-TRANSITIVE depends upon the :type-
prescription rule PERM.

Summary
Form:  ( DEFTHM PERM-TRANSITIVE ...)
Rules: ((:DEFINITION ATOM)
        (:DEFINITION NOT)
        (:DEFINITION PERM)
        (:INDUCTION PERM)
        (:REWRITE NOT-PERM-IF-DIFFERENT-MEMBERS)
        (:REWRITE PERM-DEL-DEL)
        (:TYPE-PRESCRIPTION MEM)
        (:TYPE-PRESCRIPTION PERM))
Warnings:  Free
Time:  0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
Prover steps counted:  1324
 PERM-TRANSITIVE
ACL2 !>(quit)

~/Dropbox/talks/key-workshop-july-2015/demos$