Import acl2_7.4dfsg.orig.tar.gz

[dgit import orig acl2_7.4dfsg.orig.tar.gz]

11 files changed, 3136 insertions, 0 deletions

diff --git a/books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp b/books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp
new file mode 100644
index 0000000..3aab407
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp
@@ -0,0 +1,249 @@
+;;; ackermann.lisp
+;;; Admissibility of an iterative version of Ackermann function.
+;;; Created: 06-06-2000 Last Revised: 19-09-00
+;;;============================================================================
+
+;;; To certify this book:
+
+#|
+(in-package "ACL2")
+(certify-book "ackermann")
+|#
+
+(in-package "ACL2")
+
+(include-book "../../defmul")
+(set-well-founded-relation e0-ord-<)
+
+;;;****************************************************************************
+;;; USING MULTISETS RELATIONS TO PROVE TERMINATION OF AN ITERATIVE
+;;; VERSION OF ACKERMANN'S FUNCTION
+;;;****************************************************************************
+
+;;; ===========================================================================
+;;; 1. Admission of an iterative version of Ackermann's function
+;;; ===========================================================================
+
+;;; This is the Ackermann function, classical definition:
+;;; ·····················································
+
+(defun ack (m n)
+  (declare (xargs :measure (cons (+ (nfix m) 1) (nfix n))
+		  :guard (and (integerp m) (>= m 0)
+			      (integerp n) (>= n 0))
+		  :verify-guards nil))
+  (cond ((zp m) (+ n 1))
+	((zp n) (ack (- m 1) 1))
+	(t (ack (- m 1) (ack m (- n 1))))))
+
+(defthm ack-non-negative-integer
+  (implies (and (integerp n) (>= n 0))
+	   (and (integerp (ack m n))
+		(>= (ack m n) 0))))
+
+(verify-guards ack)
+
+;;; Our goal is to define an iterative version of ack:
+;;; ··················································
+
+; (defun ack-it-aux (s z)
+;   (declare (xargs :mode :program))
+;   (if (endp s)
+;       z
+;       (let ((head (first s))
+;             (tail (rest s)))
+;         (cond ((zp head) (ack-it-aux tail (+ z 1)))
+;               ((zp z) (ack-it-aux (cons (- head 1) tail) 1))
+;               (t (ack-it-aux (cons head (cons (- head 1) tail))
+;                              (- z 1)))))))
+
+; (defun ack-it (m n)
+;   (declare (xargs :mode :program))
+;   (ack-it-aux (list m) n))
+
+;;; And prove that ack-it is equal to ack
+
+;;; We will replay the proof of Dershowitz & Manna in "Proving
+;;; termination with multiset orderings"
+
+;;; ---------------------------------------------------------------------------
+;;; 1.1 A well-founded relation rel-ack
+;;; ---------------------------------------------------------------------------
+
+;;; The measures:
+(defun mp-ack (p)
+  (declare (xargs :verify-guards t))
+  (and (consp p)
+       ;; slight mod (use of natp) for v2-8 ordinals changes
+       (natp (car p))
+       (natp (cdr p))))
+
+;;; The relation:
+(defun rel-ack (p1 p2)
+  (declare (xargs :guard (and (mp-ack p1) (mp-ack p2))))
+  (cond ((< (car p1) (car p2)) t)
+	((= (car p1) (car p2)) (< (cdr p1) (cdr p2)))))
+
+;;; The embedding:
+(defun fn-ack (p)
+  (declare (xargs :guard (mp-ack p)))
+  ;; modified for v2-8 ordinals changes
+  (make-ord (1+ (car p)) 1 (cdr p)))
+
+;;; The well-foundedness-theorem:
+; modified for v2-8 ordinals changes
+(defthm rel-ack-well-founded
+  (and (implies (mp-ack x)
+		(o-p (fn-ack x)))
+       (implies (and (mp-ack x)
+		     (mp-ack y)
+		     (rel-ack x y))
+		(o< (fn-ack x) (fn-ack y))))
+  :rule-classes :well-founded-relation)
+
+
+;;; ---------------------------------------------------------------------------
+;;; 1.2 Extension of rel-ack to mul-rel-ack (well founded).
+;;;----------------------------------------------------------------------------
+
+; (defmul-components rel-ack)
+; => The list of components is:
+;     (REL-ACK REL-ACK-WELL-FOUNDED MP-ACK FN-ACK X Y)
+
+(defmul (REL-ACK REL-ACK-WELL-FOUNDED MP-ACK FN-ACK X Y)
+  :verify-guards t)
+
+;;;----------------------------------------------------------------------------
+;;; 1.3 Definition of a measure in order to accept ack-it-aux.
+;;;----------------------------------------------------------------------------
+
+(defun get-pairs-add1-0 (s)
+  (declare (xargs :guard (true-listp s)))
+  (if (atom s)
+      nil
+      (cons (cons (+ (nfix (car s)) 1) 0)
+	    (get-pairs-add1-0 (cdr s)))))
+
+(defun measure-ack-it-aux (s z)
+  (declare (xargs :guard (true-listp s)))
+  (if (endp s)
+      nil
+      (cons (cons (nfix (car s)) (nfix z))
+	    (get-pairs-add1-0 (cdr s)))))
+
+;;;----------------------------------------------------------------------------
+;;; 1.4 Definition of ack-it-aux.
+;;;----------------------------------------------------------------------------
+
+;;; Some lemmas needed to the admission of ack-it-aux
+;;; ·················································
+
+;;; 1)
+
+(in-theory (enable natp)) ; modified for v2-8 ordinals changes
+
+(encapsulate
+ ()
+
+ (local (in-theory (disable nfix)))
+
+ (local
+  (defthm mp-ack-true-listp-get-pairs-add1-0
+    (mp-ack-true-listp (get-pairs-add1-0 l))))
+
+ (defthm measure-ack-it-aux-mp-ack-true-lisp
+   (mp-ack-true-listp (measure-ack-it-aux s z))))
+
+;;; 2)
+
+(in-theory (disable multiset-diff))
+
+(encapsulate
+ ()
+
+ (local (in-theory (disable nfix zp)))
+
+ (defthm measure-ack-it-aux-mp-decreases-1
+   (implies (zp y)
+	    (mul-rel-ack (measure-ack-it-aux l (+ 1 z))
+			 (measure-ack-it-aux (cons y l) z)))
+   :hints (("Subgoal 2" :in-theory (disable multiset-diff))
+	   ("Subgoal 2.2" :in-theory (enable multiset-diff))
+	   ("Subgoal 2.1" :in-theory (enable multiset-diff)))))
+
+;;; 3)
+
+(defthm measure-ack-it-aux-mp-decreases-2
+  (implies (and (not (zp y)) (zp z))
+	   (mul-rel-ack (measure-ack-it-aux (cons (+ -1 y) l)
+					    1)
+			(measure-ack-it-aux (cons y l) z)))
+  :hints (("Goal" :in-theory (disable multiset-diff))))
+
+;;; 4)
+
+(defthm measure-ack-it-aux-mp-decreases-3
+  (implies
+   (and (not (zp y)) (not (zp z)))
+   (mul-rel-ack (measure-ack-it-aux (list* y (+ -1 y) l) (+ -1 z))
+		(measure-ack-it-aux (cons y l) z)))
+  :hints (("Goal" :in-theory (disable multiset-diff))
+	  ("Subgoal 1" :in-theory (enable multiset-diff))))
+
+
+;;; At last, admission of ack-it-aux and definition of ack-it
+;;; ·························································
+
+(defun nn-integer-true-listp (s)
+  (declare (xargs :guard t))
+  (if (atom s)
+      (equal s nil)
+      (and (integerp (car s)) (>= (car s) 0)
+	   (nn-integer-true-listp (cdr s)))))
+
+(defun ack-it-aux (s z)
+  (declare (xargs
+	    :guard (and (nn-integer-true-listp s) (integerp z) (>= z 0))
+	    :measure (measure-ack-it-aux s z)
+	    :well-founded-relation mul-rel-ack
+	    :hints (("Goal" :in-theory
+		     (disable measure-ack-it-aux mul-rel-ack zp)))))
+  (if (endp s)
+      z
+      (let ((head (first s))
+	    (tail (rest s)))
+	(cond ((zp head) (ack-it-aux tail (+ z 1)))
+	      ((zp z) (ack-it-aux (cons (- head 1) tail) 1))
+	      (t (ack-it-aux (cons head (cons (- head 1) tail)) (- z 1)))))))
+
+(defun ack-it (m n)
+  (declare (xargs
+	    :guard (and (integerp m) (>= m 0)
+			(integerp n) (>= n 0))))
+  (ack-it-aux (list m) n))
+
+
+;;; ============================================================================
+;;; 2. Main property of ack-it: ack-it is equal to ack
+;;; ============================================================================
+
+
+(defun ack-stack (s z)
+  (declare (xargs
+	    :guard (and (nn-integer-true-listp s) (integerp z) (>= z 0))))
+  (if (endp s)
+      z
+      (ack-stack (cdr s) (ack (car s) z))))
+
+(encapsulate
+ ()
+
+ (local (defthm ack-stack-cons-expand
+	  (equal (ack-stack (cons s1 s) z)
+		 (ack-stack s (ack s1 z)))))
+
+ (defthm ack-it-aux-ack-stack
+   (equal (ack-it-aux s z) (ack-stack s z))))
+
+(defthm ack-it-equal-ack
+  (equal (ack-it m n) (ack m n)))
diff --git a/books/workshops/2000/ruiz/multiset/examples/mccarthy-91/mccarthy-91.lisp b/books/workshops/2000/ruiz/multiset/examples/mccarthy-91/mccarthy-91.lisp
new file mode 100644
index 0000000..b4e163f
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/mccarthy-91/mccarthy-91.lisp
@@ -0,0 +1,261 @@
+;;; mccarthy-91.lisp
+;;; Admissibility of an iterative version of McCarthy's 91 function.
+;;; Created: 6-6-2000 Last revised: 2-8-00
+;;;============================================================================
+
+;;; To certify this book:
+
+#|
+(in-package "ACL2")
+(certify-book "mccarthy-91")
+|#
+
+(in-package "ACL2")
+
+(include-book "../../defmul")
+;(include-book "../../../../../../ordinals/e0-ordinal")
+
+(set-verify-guards-eagerness 2)
+
+
+;;;****************************************************************************
+;;; USING MULTISETS RELATIONS TO PROVE TERMINATION OF McCARTHY'S 91 FUNCTION
+;;;****************************************************************************
+
+
+;;; ===========================================================================
+;;; 1. Admission of an iterative version of McCarthy 91 function.
+;;; ===========================================================================
+
+;;; Instead of defining the following definition of McCarthy's 91 function:
+
+; (defun mc (x)
+;   (declare (xargs :mode :program))
+;   (if (> x 100)
+;       (- x 10)
+;       (mc (mc (+ x 11)))))
+
+;;; Our goal is to define in ACL2 the following iterative version:
+
+; (defun mc-aux (n z)
+;   (declare (xargs :measure ...
+; 		    :well-founded-relation ...))
+;   (cond ((or (zp n) (not (integerp z))) z)
+; 	((> z 100) (mc-aux (- n 1) (- z 10)))
+; 	(t (mc-aux (+ n 1) (+ z 11)))))
+
+; (defun mc-it (x)
+;   (mc-aux 1 x))
+
+;;; We will replay the proof of Dershowitz & Manna in "Proving
+;;; termination with multiset orderings"
+
+;;; ---------------------------------------------------------------------------
+;;; 1.1 A well-founded relation rel-mc
+;;; ---------------------------------------------------------------------------
+
+;;; The measures:
+(defun integerp-<=-111 (x)
+  (and (integerp x) (<= x 111)))
+
+;;; REMARK : There is a mistake in the proof by D&M, because they say
+;;; that the domain is 0 <= x < 111.
+
+;;; The relation:
+(defun rel-mc (x y)
+  (and (integerp-<=-111 x)
+       (integerp-<=-111 y)
+       (< y x)))
+
+;;; The embedding:
+(defun fn-rel-mc (x)
+  (if (integerp-<=-111 x)
+      (- 111 x)
+      0))
+
+;;; The well-foundedness theorem:
+; modified for v2-8 ordinals changes
+(defthm rel-mc-well-founded
+  (and (o-p (fn-rel-mc x))
+       (implies (rel-mc x y)
+		(o< (fn-rel-mc x) (fn-rel-mc y))))
+  :rule-classes :well-founded-relation)
+
+;;; REMARK: One could think that integerp-<=-111 is the MP property of the
+;;; well-founded relation, instead of T. But there is a subtle difference: our
+;;; measure (our multisets) can contain elements greater than 111, although
+;;; those elements are not comparable.
+
+;;; ---------------------------------------------------------------------------
+;;; 1.2 Extension of rel-mc to mul-rel-mc (well founded).
+;;;----------------------------------------------------------------------------
+
+;;; (defmul-components rel-mc)
+; => The list of components is:
+;     (REL-MC REL-MC-WELL-FOUNDED T FN-REL-MC X Y)
+
+(defmul (REL-MC REL-MC-WELL-FOUNDED T FN-REL-MC X Y) :verify-guards t)
+
+;;;----------------------------------------------------------------------------
+;;; 1.3 Definition of a measure in order to accept mc-aux.
+;;;----------------------------------------------------------------------------
+
+(defun f91 (x)
+  (cond ((not (integerp x)) x)
+	((> x 100) (- x 10))
+	(t 91)))
+
+(defun measure-mc-aux (n z)
+  (declare (xargs :guard (and (integerp n) (>= n 0))))
+  (if (zp n)
+      nil
+      (cons z (measure-mc-aux (- n 1) (f91 z)))))
+
+;;;----------------------------------------------------------------------------
+;;; 1.4 Definition of "mc-aux".
+;;;----------------------------------------------------------------------------
+
+;;; Fundamental rewrite rule for our proof strategy:
+;;; The rule measure-mc-aux-expand expands measure-mc-aux where the
+;;; expansion heuristics of the system fail. This is important for two
+;;; reasons. First, measure-mc-aux definition is expanded whenever it
+;;; can be deduced that n>0, and the multiset obtained explicitly
+;;; present the first (and second sometimes) elements and the same tail,
+;;; allowing the meta rule of multiset.lisp to rewrite. Second, the IF
+;;; in the rule performs almost the same case distinction as in the hand
+;;; proof.
+
+(defthm measure-mc-aux-expand
+  (implies (and (not (zp n)) (integerp z))
+	   (equal (measure-mc-aux n z)
+		  (cons z (measure-mc-aux (- n 1)
+					  (if (> z 100) (- z 10) 91))))))
+
+;;; The next theorem comes from the "equalities" book
+;;; ("../distribution/books/arithmetic/equalities.lisp"). It's the only event
+;;; from this book needed in the admission of "mc-aux".
+
+(defthm fold-consts-in-+
+  (implies (and (syntaxp (quotep x))
+		(syntaxp (quotep y)))
+	   (equal (+ x (+ y z))
+		  (+ (+ x y) z))))
+
+(in-theory (disable multiset-diff))
+
+;;; At last:
+
+(defun mc-aux (n z)
+  (declare (xargs
+	    :guard (and (integerp n) (>= n 0))
+	    :measure (measure-mc-aux n z)
+	    :well-founded-relation mul-rel-mc))
+  (cond ((or (zp n) (not (integerp z))) z)
+	((> z 100) (mc-aux (- n 1) (- z 10)))
+	(t (mc-aux (+ n 1) (+ z 11)))))
+
+(defun mc-it (x)
+  (mc-aux 1 x))
+
+
+;;; ============================================================================
+;;; 2. Properties of mc-it
+;;; ============================================================================
+
+
+;;; ----------------------------------------------------------------------------
+;;; 2.1 mc-it is equal to f91
+;;; ----------------------------------------------------------------------------
+
+
+(defun iter-f91 (n x)
+  (declare (xargs :guard (and (integerp n) (>= n 0))))
+  (if (zp n)
+      x
+      (iter-f91 (- n 1) (f91 x))))
+
+;;; Fundamental rewrite rule for our proof strategy:
+
+(defthm iter-f91-expand
+  (implies (and (not (zp n)) (integerp z))
+	   (equal (iter-f91 n z)
+		  (iter-f91 (- n 1)
+			    (if (> z 100) (- z 10) 91)))))
+
+(defthm iter-f91-mc-aux
+  (equal (mc-aux n z) (iter-f91 n z))
+  :hints (("Goal" :induct (mc-aux n z))))
+
+(defthm mc-it-equals-f91-for-non-integers
+  (implies (not (integerp x))
+	   (equal (iter-f91 n x) x)))
+
+(defthm equal-mc-it-and-f91
+  (equal (mc-it x) (f91 x)))
+
+
+;;; ----------------------------------------------------------------------------
+;;; 2.2 mc-it verifies the recursion scheme of mc
+;;; ----------------------------------------------------------------------------
+
+(defthm mc-it-recursive-schema
+  (equal (mc-it x)
+	 (cond ((not (integerp x)) x)
+	       ((> x 100) (- x 10))
+	       (t (mc-it (mc-it (+ x 11))))))
+  :rule-classes nil)
+
+
+;;; ----------------------------------------------------------------------------
+;;; 2.3 Every function satisfying the recursion scheme of mc is equal to f91
+;;; ----------------------------------------------------------------------------
+
+
+
+;;; A general function M satisfying the above recursive equation:
+
+(encapsulate
+ ((M (x) t))
+
+ (local (defun M (x) (mc-it x)))
+
+ (defthm M-it-recursive-schema
+   (equal (M x)
+	  (cond ((not (integerp x)) x)
+		((> x 100) (- x 10))
+		(t (M (M (+ x 11))))))
+   :rule-classes :definition))
+
+(defun iter-M (n x)
+  (declare (xargs :guard (and (integerp n) (>= n 0))))
+  (if (zp n)
+      x
+      (iter-M (- n 1) (M x))))
+
+(defthm M-expand
+  (implies (and (not (zp n)) (integerp z))
+	   (equal (iter-M n z)
+		  (iter-M (- n 1)
+			  (if (> z 100) (- z 10) (M (M (+ z 11))))))))
+
+(defthm iter-M-equals-mc-aux
+  (equal (iter-M n z) (mc-aux n z))
+  :hints (("Goal" :in-theory (disable iter-f91-mc-aux))))
+
+;;; Then M is equal to f91
+
+(encapsulate
+ ()
+
+ (local
+  (defthm iter-M-1-M
+    (equal (M x) (iter-M 1 x))
+    :hints (("Goal" :in-theory (disable iter-M-equals-mc-aux)
+	     :expand (iter-M 1 x)))))
+
+ (defthm M-equal-f91
+   (equal (M x) (f91 x))))
+
+
+
+
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/abstract-proofs.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/abstract-proofs.lisp
new file mode 100644
index 0000000..d5421b1
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/abstract-proofs.lisp
@@ -0,0 +1,268 @@
+;;; abstract-proofs.lisp
+;;; Definition and properties of abstract proofs.
+;;; Created: 10-6-99 Last Revision: 05-10-00
+;;; =============================================================================
+
+(in-package "ACL2")
+
+(include-book "../../../../../../data-structures/structures")
+(local (include-book "../../../../../../ordinals/e0-ordinal"))
+
+;;; *******************************************
+;;; ABSTRACT PROOFS: DEFINITIONS AND PROPERTIES
+;;; *******************************************
+
+;;; ============================================================================
+;;; 1. Proof steps
+;;; ============================================================================
+
+;;; We see here proofs from a very general point of view. Proofs are
+;;; lists of r-steps, and r-steps are structures with four fields:
+;;; elt1, elt2, direct and operator (every step "connect" elt1 and elt2
+;;; in the direction given by direct, and by application of operator).
+
+;;; Definition and properties about manipulation of proofs and its form
+;;; are given here.
+
+;;; The following is the definition of an abstract reduction step:
+
+(defstructure r-step
+   direct
+   operator
+   elt1
+   elt2
+   (:options (:conc-name nil)
+	     (:do-not :tag)))
+
+;;; REMARK: An abstract proof will be defined as a list of r-steps. Note
+;;; that, in this book, we do not require that the operator is applicable
+;;; to one of the elements returning the other. This will be required
+;;; for each particular reduction relation. We are only concerned with the
+;;; "shape" of proofs.
+
+
+;;; ============================================================================
+;;; 2. Useful definitions
+;;; ============================================================================
+
+;;; The last element of a non-empty list
+
+(defmacro last-elt (l)
+  `(car (last ,l)))
+
+;;; First and last elements of a proof (including empty proofs)
+
+(defun first-of-proof (x p)
+   (if (endp p) x (elt1 (car p))))
+
+(defun last-of-proof (x p)
+   (if (endp p) x (elt2 (last-elt p))))
+
+;;; Steps-up: A chain of inverse steps
+
+(defun steps-up (p)
+   (if (endp p)
+       t
+     (and
+      (not (direct (car p)))
+      (steps-up (cdr p)))))
+
+;;; Steps-down: A chain of direct steps
+
+(defun steps-down (p)
+   (if (endp p)
+       t
+     (and
+      (direct (car p))
+      (steps-down (cdr p)))))
+
+;;; Steps-valley: down and up
+
+(defun steps-valley (p)
+   (cond ((endp p) t)
+	 ((direct (car p)) (steps-valley (cdr p)))
+	 (t (steps-up (cdr p)))))
+
+
+;;; Steps-mountain: up and down
+
+(defun steps-mountain (p)
+   (cond ((endp p) t)
+	 ((direct (car p)) (steps-down (cdr p)))
+	 (t (steps-mountain (cdr p)))))
+
+
+;;; A local peak
+
+(defun local-peak-p (p)
+   (and (consp p)
+	(consp (cdr p))
+	(atom (cddr p))
+	(not (direct (car p)))
+	(direct (cadr p))))
+
+
+;;; Inverse step
+
+(defun inverse-r-step (st)
+   (make-r-step
+    :direct (not (direct st))
+    :elt1 (elt2 st)
+    :elt2 (elt1 st)
+    :operator (operator st)))
+
+;;; The piece of proof just before the first local-peak
+
+(defun proof-before-peak (p)
+  (cond ((or (atom p) (atom (cdr p))) p)
+	((and (not (direct (car p))) (direct (cadr p))) nil)
+	(t (cons (car p) (proof-before-peak (cdr p))))))
+
+;;; The piece of proof just after the first local peak
+
+(defun proof-after-peak (p)
+  (cond ((atom p) p)
+	((atom (cdr p)) (cdr p))
+	((and (not (direct (car p))) (direct (cadr p)))
+	 (cddr p))
+	(t (proof-after-peak (cdr p)))))
+
+;;; The first peak of a proof
+
+(defun local-peak (p)
+  (cond ((atom p) p)
+	((atom (cdr p)) (cdr p))
+	((and (not (direct (car p))) (direct (cadr p)))
+	 (list (car p) (cadr p)))
+	(t (local-peak (cdr p)))))
+
+;;; The top element of a peak
+
+(defun peak-element (p)
+   (elt1 (cadr (local-peak p))))
+
+;;; The down part of a valley
+
+(defun proof-before-valley (p)
+  (cond ((atom p) p)
+	((direct (car p)) (cons (car p)
+				(proof-before-valley (cdr p))))
+	(t nil)))
+
+;;; Inverse proof
+
+(defun inverse-proof (p)
+   (if (atom p)
+       p
+     (append (inverse-proof (cdr p))
+	     (list (inverse-r-step (car p))))))
+
+;;; The up part of a valley
+
+(defun proof-after-valley (p)
+  (cond ((atom p) p)
+	((direct (car p)) (proof-after-valley (cdr p)))
+	(t p)))
+
+;;; The list of elements involved in a proof
+
+(defun proof-measure (p)
+  (if (endp p)
+      nil
+    (cons (elt1 (car p)) (proof-measure (cdr p)))))
+
+
+;;; ============================================================================
+;;; 3. Useful properties
+;;; ============================================================================
+
+(defthm steps-down-append
+  (equal (steps-down (append p1 p2))
+	 (and (steps-down p1) (steps-down p2))))
+
+(defthm steps-up-append
+  (equal (steps-up (append p1 p2))
+	 (and (steps-up p1) (steps-up p2))))
+
+
+(defthm steps-valley-append
+  (implies (and (steps-down p1)
+		(steps-up p2))
+	   (steps-valley (append p1 p2))))
+
+
+(defthm steps-mountain-append
+  (implies (and (steps-up p1)
+		(steps-down p2))
+	   (steps-mountain (append p1 p2))))
+
+
+(defthm steps-up-inverse-proof
+  (equal
+   (steps-up (inverse-proof p))
+   (steps-down p)))
+
+
+(defthm steps-down-inverse-proof
+  (equal
+   (steps-down (inverse-proof p))
+   (steps-up p)))
+
+
+(defthm proof-measure-append
+  (equal (proof-measure (append p1 p2))
+	 (append (proof-measure p1)
+		 (proof-measure p2))))
+
+
+(defthm steps-down-proof-before-valley
+  (steps-down (proof-before-valley p)))
+
+
+(defthm steps-up-proof-before-valley
+  (implies (steps-valley p)
+	   (steps-up (proof-after-valley p))))
+
+
+(defthm proof-valley-append
+  (equal
+   (append (proof-before-valley p)
+	   (proof-after-valley p))
+   p)
+  :rule-classes nil)
+
+(defthm first-element-of-proof-before-valley
+  (implies (consp (proof-before-valley p))
+	   (equal (elt1 (car (proof-before-valley p)))
+		  (elt1 (car p)))))
+
+(defthm last-element-of-proof-after-valley
+   (implies (consp (proof-after-valley p))
+ 	   (equal (elt2 (last-elt (proof-after-valley p)))
+ 		  (elt2 (last-elt p)))))
+
+
+(defthm steps-valley-append-steps-up
+  (implies (and (steps-up p2)
+		(steps-valley p1))
+	   (steps-valley (append p1 p2))))
+
+(defthm steps-dowm-append-steps-valley
+  (implies (and (steps-down p1)
+		(steps-valley p2))
+	   (steps-valley (append p1 p2))))
+
+(defthm steps-up-steps-valley
+  (implies (steps-up p)
+	   (steps-valley p)))
+
+(defthm steps-down-steps-valley
+  (implies (steps-down p)
+	   (steps-valley p)))
+
+(defthm steps-valley-inverse-proof
+  (implies (steps-valley p)
+	   (steps-valley (inverse-proof p))))
+
+
+
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.acl2 b/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.acl2
new file mode 100644
index 0000000..f7ca171
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.acl2
@@ -0,0 +1,20 @@
+(value :q)
+
+(lp)
+
+(defconst *abstract-proofs-exports*
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step
+    first-of-proof last-of-proof steps-up steps-down steps-valley
+    proof-before-valley proof-after-valley inverse-r-step inverse-proof
+    local-peak-p proof-measure proof-before-peak proof-after-peak
+    local-peak peak-element))
+
+(defconst *cnf-package-exports*
+  (union-eq *acl2-exports*
+	    (union-eq
+	     *common-lisp-symbols-from-main-lisp-package*
+	     *abstract-proofs-exports*)))
+
+(defpkg "CNF" *cnf-package-exports*)
+
+(certify-book "confluence-v0" ? t)
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp
new file mode 100644
index 0000000..dfc7899
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp
@@ -0,0 +1,417 @@
+;;; confluence-v0.lisp
+;;; Church-Rosser and normalizing abstract reductions.
+;;; Definition, properties and decidability
+;;; *** We prove here the same properties than
+;;; *** confluence.lisp, but we extend here our language to talk about
+;;; *** reducibility, by means of the function (reducible x)
+;;; Created: 10-6-99 Last Revision: 06-10-2000
+;;; =======================================================
+
+;;; To certify this book:
+#|
+(in-package "ACL2")
+
+
+(defconst *abstract-proofs-exports*
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step
+    first-of-proof last-of-proof steps-up steps-down steps-valley
+    proof-before-valley proof-after-valley inverse-r-step inverse-proof
+    local-peak-p proof-measure proof-before-peak proof-after-peak
+    local-peak peak-element))
+
+(defconst *cnf-package-exports*
+  (union-eq *acl2-exports*
+	    (union-eq
+	     *common-lisp-symbols-from-main-lisp-package*
+	     *abstract-proofs-exports*)))
+
+(defpkg "CNF" *cnf-package-exports*)
+
+(certify-book "confluence-v0" 3)
+|#
+
+;;;
+(in-package "CNF")
+(include-book "abstract-proofs")
+
+;;; ********************************************************************
+;;; A FORMALIZATION OF NORMALIZING AND CHURCH-ROSSER ABSTRACT REDUCTIONS
+;;; ********************************************************************
+
+;;; ********* IMPORTANT REMARK:
+
+;;; We formalize here normalizing and Church-Rosser reduction relations,
+;;; and show decidability of its equivalence closure. We do the same
+;;; thing in confluence.lisp. But unlike there, we extend our language
+;;; by a function called reducible, supposed to return a legal operator
+;;; for every input, whenever it exists.
+;;; The main advantage of this presentation is clarity. The main
+;;; disadvantage comes from a theoretical point of view. The results in
+;;; confluence.lisp are stronger since we can show decidability without
+;;; having an algorithm to check reducibility. That is the reason why we
+;;; chose the presentation in confluence.lisp. But from a practical
+;;; point of view there is no such distinction: we need anyway a function
+;;; proof-irreducible, returning a proof connecting every element to an
+;;; equivalent normal form. It's hard to think in one case in which we
+;;; have such function and we do not have the reducibility test (for
+;;; example, if we think in a noetherian reduction, to define
+;;; proof-irreducible, we need a reducibility test, as we will show in
+;;; local-confluence.lisp)
+
+;;; ============================================================================
+;;; 1. Definition of a normalizing and (CR) abstract reduction
+;;; ============================================================================
+
+(encapsulate
+ ((legal (x u) boolean)
+  (reduce-one-step (x u) element)
+  (reducible (x) boolean)
+  (transform-to-valley (x) valley-proof)
+  (proof-irreducible (x) proof))
+
+ (local (defun legal (x u) (declare (ignore x u)) nil))
+ (local (defun reduce-one-step (x u) (+ x u)))
+ (local (defun reducible (x) (declare (ignore x)) nil))
+
+ (defthm legal-reducible-1
+   (implies (reducible x) (legal x (reducible x))))
+
+ (defthm legal-reducible-2
+   (implies (not (reducible x)) (not (legal x u))))
+
+ (defun proof-step-p (s)
+   (let ((elt1 (elt1 s)) (elt2 (elt2 s))
+	 (operator (operator s)) (direct (direct s)))
+     (and (r-step-p s)
+	  (implies direct (and (legal elt1  operator)
+			       (equal (reduce-one-step elt1 operator)
+				      elt2)))
+	  (implies (not direct) (and (legal elt2 operator)
+				     (equal (reduce-one-step elt2 operator)
+					    elt1))))))
+
+ (defun equiv-p (x y p)
+   (if (endp p)
+       (equal x y)
+       (and (proof-step-p (car p))
+	    (equal x (elt1 (car p)))
+	    (equiv-p (elt2 (car p)) y (cdr p)))))
+
+ (local (defun transform-to-valley (x) (declare (ignore x)) nil))
+
+ (defthm Chuch-Rosser-property
+   (let ((valley (transform-to-valley p)))
+     (implies (equiv-p x y p)
+	      (and (steps-valley valley)
+		   (equiv-p x y valley)))))
+
+ (local (defun proof-irreducible (x) (declare (ignore x)) nil))
+
+ (defthm normalizing
+   (let* ((p-x-y (proof-irreducible x))
+	  (y (last-of-proof x p-x-y)))
+     (and (equiv-p x y p-x-y)
+	  (not (reducible y))))))
+
+;;; ----------------------------------------------------------------------------
+;;; 1.1 Useful rules
+;;; ----------------------------------------------------------------------------
+
+;;; Two useful rewrite rules about normalizing
+
+(local
+ (defthm normalizing-not-consp-proof-irreducible
+   (implies (not (consp (proof-irreducible x)))
+	    (not (reducible x)))
+   :hints (("Goal" :use (:instance normalizing)))))
+
+(local
+ (defthm normalizing-consp-proof-irreducible
+   (let ((p-x-y (proof-irreducible x)))
+     (implies (consp p-x-y)
+	      (and (equiv-p x (elt2 (last-elt p-x-y)) p-x-y)
+		   (not (reducible (elt2 (last-elt p-x-y)))))))
+   :hints (("Goal" :use (:instance normalizing)))))
+
+;;; Since equiv-p is "infected", we have to specify the induction scheme.
+;;; Suggested by M. Kaufman
+
+(local
+ (defun induct-equiv-p (x p) (declare (ignore x))
+   (if (endp p)
+       t
+     (induct-equiv-p (elt2 (car p)) (cdr p)))))
+
+(local
+ (defthm equiv-p-induct t
+   :rule-classes
+   ((:induction :pattern (equiv-p x y p)
+	       :condition t
+	       :scheme (induct-equiv-p x p)))))
+
+;;; The first and the last element of a proof
+
+(local
+ (defthm first-element-of-equivalence
+   (implies (and (equiv-p x y p) (consp p))
+	    (equal (elt1 (car p)) x))))
+
+(local
+ (defthm last-elt-of-equivalence
+   (implies (and (equiv-p x y p) (consp p))
+	    (equal (elt2 (last-elt p)) y))))
+
+
+;;; ---------------------------------------------------------------------------
+;;; 1.2 equiv-p is an equivalence relation (the least containing the reduction)
+;;; ---------------------------------------------------------------------------
+
+;;; To be confident of the definition of equiv-p we show that equiv-p is
+;;; the least equivalence relation containing the reduction steps.
+
+;;; REMARK: To say it properly, we show that the relation
+;;; "exists p such that (equiv-p x y p)" is an equivalence relation.
+
+;;; An useful rule to deal with concatenation of proofs
+(local
+ (defthm proof-append
+   (implies (equal z (last-of-proof x p1))
+	    (equal (equiv-p x y (append p1 p2))
+		   (and (equiv-p x z p1)
+			(equiv-p z y p2))))))
+
+;;; The properties of equivalence relations are met by equiv-p
+
+(defthm equiv-p-reflexive
+  (equiv-p x x nil))
+
+(defthm equiv-p-symmetric
+  (implies (equiv-p x y p)
+	   (equiv-p y x (inverse-proof p))))
+
+(defthm equiv-p-transitive
+  (implies (and (equiv-p x y p1)
+		(equiv-p y z p2))
+	   (equiv-p x z (append p1 p2)))
+  :rule-classes nil)
+
+;;; REMARK: We have an "algebra" of proofs:
+;;;   - append for the concatenation of proofs
+;;;   - inverse-proof is already defined in abstract-proofs.lisp
+;;;   - nil is the identity.
+
+;;; Obviously, the reduction relaton is contained in equiv-p
+
+(defthm equiv-p-containd-reduction
+  (implies (legal x op)
+	   (equiv-p x (reduce-one-step x op)
+		   (list
+		    (make-r-step
+		     :elt1 x
+		     :elt2 (reduce-one-step x op)
+		     :direct t
+		     :operator op)))))
+
+
+;;; Let us assume that we have a relation eqv of equivalence, containing
+;;; the reduction steps. Let us show that it contains equiv-p
+
+
+(local
+ (encapsulate
+  ((eqv (t1 t2) boolean))
+
+  (local (defun eqv (t1 t2) (declare (ignore t1 t2)) t))
+
+  (defthm eqv-contains-reduction
+    (implies (legal x op)
+             (eqv x (reduce-one-step x op))))
+
+  (defthm eqv-reflexive
+    (eqv x x))
+
+  (defthm eqv-symmetric
+    (implies (eqv x y) (eqv y x)))
+
+  (defthm eqv-transitive
+    (implies (and (eqv x y) (eqv y z))
+            (eqv x z)))))
+
+
+(local
+ (defthm equiv-p-the-least-equivalence-containing-reduction
+   (implies (equiv-p x y p)
+            (eqv x y))
+   :hints (("Subgoal *1/3" :use
+	    (:instance eqv-transitive (y (elt2 (car p)))
+		       (z y))
+	    :in-theory (disable eqv-transitive)))))
+
+
+
+;;; ----------------------------------------------------------------------------
+;;; 1.3 There are no equivalent and distinct normal forms
+;;; ----------------------------------------------------------------------------
+
+;;; Two lemmas
+
+(local
+  (defthm reducible-steps-up
+    (implies (and  (consp p) (steps-up p)
+		   (not (reducible y)))
+ 	    (not (equiv-p x y p)))))
+
+
+(local
+ (defthm two-ireducible-connected-by-a-valley-are-equal
+   (implies (and (steps-valley p)
+ 		 (equiv-p x y p)
+ 		 (not (reducible x))
+ 		 (not (reducible y)))
+ 	    (equal x y))
+   :rule-classes nil))
+
+;;; And the theorem
+
+(local
+  (defthm if-confluent--two-ireducible-connected-are-equal
+    (implies (and (equiv-p x y p)
+		  (not (reducible x))
+		  (not (reducible y)))
+ 	    (equal x y))
+    :rule-classes nil
+    :hints (("Goal" :use (:instance
+ 			  two-ireducible-connected-by-a-valley-are-equal
+ 			  (p (transform-to-valley p)))))))
+
+
+;;; ============================================================================
+;;; 2. Decidability of Church-Rosser and normalizing redutions
+;;; ============================================================================
+
+;;; ----------------------------------------------------------------------------
+;;; 2.1 Normal forms, definition and fundamental properties.
+;;; ----------------------------------------------------------------------------
+
+(defun normal-form (x)
+  (last-of-proof x (proof-irreducible x)))
+
+(local
+ (defthm irreducible-normal-form
+   (not (reducible (normal-form x)))))
+
+(local
+ (defthm proof-irreducible-proof
+   (equiv-p x (normal-form x) (proof-irreducible x))))
+
+(local
+ (defthm proof-irreducible-atom-normal-form
+   (implies (atom (proof-irreducible x))
+	    (equal (normal-form x) x))))
+
+(local
+ (defthm proof-irreducible-consp-normal-form
+   (implies (consp (proof-irreducible x))
+	    (equal (elt2 (last-elt (proof-irreducible x))) (normal-form x)))))
+
+
+;;; We can disable normal-form (its fundamental properties are rewrite
+;;; rules).
+(local (in-theory (disable normal-form)))
+
+;;; ----------------------------------------------------------------------------
+;;; 2.2  A decision algorithm for [<-reduce-one-step->]*
+;;; ----------------------------------------------------------------------------
+
+
+(defun provably-equivalent (x y)
+  (equal (normal-form x) (normal-form y)))
+
+;;; ············································································
+;;; 2.2.1 Completeness
+;;; ············································································
+
+;;; A proof between normal forms
+(local
+ (defun make-proof-between-normal-forms (x y p)
+   (append (inverse-proof (proof-irreducible x))
+	   p
+	   (proof-irreducible y))))
+
+;;;; Some needed lemmas
+
+(local
+ (defthm consp-inverse-proof
+   (iff (consp (inverse-proof p))
+	(consp p))))
+
+(local
+ (defthm last-elt-append
+   (implies (consp p2)
+	    (equal (last-elt (append p1 p2)) (last-elt p2)))))
+(local
+ (defthm last-elt-inverse-proof
+   (implies (consp p)
+	    (equal (last-elt (inverse-proof p))
+		   (inverse-r-step (car p))))))
+
+(local
+ (defthm first-element-of-proof-irreducible
+   (implies (consp (proof-irreducible x))
+	    (equal (elt1 (car (proof-irreducible x))) x))
+   :hints (("Goal" :use ((:instance
+			  first-element-of-equivalence
+			  (y (normal-form x)) (p (proof-irreducible
+						   x))))))))
+;;; The main lemma for completeness: the proof constructed is a proof
+;;; indeed.
+(local
+ (defthm make-proof-between-normal-forms-indeed
+   (implies (equiv-p x y p)
+	    (equiv-p (normal-form x)
+		     (normal-form y)
+		     (make-proof-between-normal-forms x y p)))))
+
+(local (in-theory (disable make-proof-between-normal-forms)))
+
+;;; COMPLETENESS
+
+(defthm provably-equivalent-complete
+  (implies (equiv-p x y p)
+	   (provably-equivalent x y))
+  :hints (("Goal" :use ((:instance
+			 if-confluent--two-ireducible-connected-are-equal
+			 (x (normal-form x))
+			 (y (normal-form y))
+			 (p (make-proof-between-normal-forms x y p)))))))
+
+
+;;; ············································································
+;;; 2.2.1 Soundness
+;;; ············································································
+
+;;; A proof between x and y (if their normal forms are equal)
+
+(defun make-proof-common-n-f (x y)
+   (append (proof-irreducible x) (inverse-proof (proof-irreducible y))))
+
+;;; SOUNDNESS
+
+(defthm provably-equivalent-sound
+  (implies (provably-equivalent x y)
+	   (equiv-p x y (make-proof-common-n-f x y)))
+  :hints (("Goal" :use (:instance
+			       equiv-p-symmetric
+			       (x y)
+			       (y (normal-form y))
+			       (p (proof-irreducible y))))))
+
+;;; REMARK: :use is needed due to a weird behaviour that sometimes of
+;;; ACL2 has with equalities in hypotesis.
+
+
+
+
+
+
+
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/confluence.acl2 b/books/workshops/2000/ruiz/multiset/examples/newman/confluence.acl2
new file mode 100644
index 0000000..ff8827c
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/confluence.acl2
@@ -0,0 +1,19 @@
+(value :q)
+(lp)
+
+(defconst *abstract-proofs-exports* 
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step 
+	     first-of-proof last-of-proof steps-up steps-down steps-valley 
+	     proof-before-valley proof-after-valley inverse-r-step inverse-proof 
+	     local-peak-p proof-measure proof-before-peak proof-after-peak 
+	     local-peak peak-element))
+
+(defconst *cnf-package-exports* 
+  (union-eq *acl2-exports* 
+	    (union-eq 
+	     *common-lisp-symbols-from-main-lisp-package* 
+	     *abstract-proofs-exports*)))
+
+(defpkg "CNF" *cnf-package-exports*)
+
+(certify-book "confluence" ? t)
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp
new file mode 100644
index 0000000..f1940ac
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp
@@ -0,0 +1,395 @@
+;;; confluence.lisp
+;;; Church-Rosser and normalizing abstract reductions.
+;;; Created: 06-10-2000 Last Revision: 06-10-2000
+;;; =============================================================================
+
+;;; To certify this book:
+#|
+(in-package "ACL2")
+
+
+(defconst *abstract-proofs-exports*
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step
+    first-of-proof last-of-proof steps-up steps-down steps-valley
+    proof-before-valley proof-after-valley inverse-r-step inverse-proof
+    local-peak-p proof-measure proof-before-peak proof-after-peak
+    local-peak peak-element))
+
+(defconst *cnf-package-exports*
+  (union-eq *acl2-exports*
+	    (union-eq
+	     *common-lisp-symbols-from-main-lisp-package*
+	     *abstract-proofs-exports*)))
+
+(defpkg "CNF" *cnf-package-exports*)
+
+(certify-book "confluence" 3)
+|#
+
+(in-package "CNF")
+
+(include-book "abstract-proofs")
+
+;;; ********************************************************************
+;;; A FORMALIZATION OF NORMALIZING AND CHURCH-ROSSER ABSTRACT REDUCTIONS
+;;; ********************************************************************
+
+;;; ********* IMPORTANT REMARK:
+;;; See the comments in the book confluence-v0.lisp
+
+;;; ============================================================================
+;;; 1. Definition of a normalizing and (CR) abstract reduction
+;;; ============================================================================
+
+(encapsulate
+ ((legal (x u) boolean)
+  (reduce-one-step (x u) element)
+  (transform-to-valley (x) valley-proof)
+  (proof-irreducible (x) proof))
+
+ (local (defun legal (x u) (declare (ignore x u)) nil))
+ (local (defun reduce-one-step (x u) (+ x u)))
+
+ (defun proof-step-p (s)
+   (let ((elt1 (elt1 s)) (elt2 (elt2 s))
+	 (operator (operator s)) (direct (direct s)))
+     (and (r-step-p s)
+	  (implies direct (and (legal elt1  operator)
+			       (equal (reduce-one-step elt1 operator)
+				      elt2)))
+	  (implies (not direct) (and (legal elt2 operator)
+				     (equal (reduce-one-step elt2 operator)
+					    elt1))))))
+
+ (defun equiv-p (x y p)
+   (if (endp p)
+       (equal x y)
+       (and (proof-step-p (car p))
+	    (equal x (elt1 (car p)))
+	    (equiv-p (elt2 (car p)) y (cdr p)))))
+
+ (local (defun transform-to-valley (x) (declare (ignore x)) nil))
+
+ (defthm Chuch-Rosser-property
+   (let ((valley (transform-to-valley p)))
+     (implies (equiv-p x y p)
+	      (and (steps-valley valley)
+		   (equiv-p x y valley)))))
+
+ (local (defun proof-irreducible (x) (declare (ignore x)) nil))
+
+ (defthm normalizing
+   (let* ((p-x-y (proof-irreducible x))
+	  (y (last-of-proof x p-x-y)))
+     (and (equiv-p x y p-x-y)
+	  (not (legal y op))))))
+
+
+;;; ----------------------------------------------------------------------------
+;;; 1.1 Useful rules
+;;; ----------------------------------------------------------------------------
+
+;;; Two useful rewrite rules about normalizing
+
+(local
+ (defthm normalizing-not-consp-proof-irreducible
+   (implies (not (consp (proof-irreducible x)))
+	    (not (legal x op)))
+   :hints (("Goal" :use (:instance normalizing)))))
+
+(local
+ (defthm normalizing-consp-proof-irreducible
+   (let ((p-x-y (proof-irreducible x)))
+     (implies (consp p-x-y)
+	      (and (equiv-p x (elt2 (last-elt p-x-y)) p-x-y)
+		   (not (legal (elt2 (last-elt p-x-y)) op)))))
+   :hints (("Goal" :use (:instance normalizing)))))
+
+
+;;; Since equiv-p is "infected" (see subversive-recursions in the ACL2
+;;; manual), we have to specify the induction scheme by means of a rule.
+
+;;; Suggested by M. Kaufman
+
+(local
+ (defun induct-equiv-p (x p) (declare (ignore x))
+   (if (endp p)
+       t
+       (induct-equiv-p (elt2 (car p)) (cdr p)))))
+
+(local
+ (defthm equiv-p-induct t
+   :rule-classes
+   ((:induction :pattern (equiv-p x y p)
+		:condition t
+		:scheme (induct-equiv-p x p)))))
+
+;;; The first and the last element of a proof
+
+(local
+ (defthm first-element-of-equivalence
+   (implies (and (equiv-p x y p) (consp p))
+	    (equal (elt1 (car p)) x))))
+
+(local
+ (defthm last-elt-of-equivalence
+   (implies (and (equiv-p x y p) (consp p))
+	    (equal (elt2 (last-elt p)) y))))
+
+
+;;; ---------------------------------------------------------------------------
+;;; 1.2 equiv-p is an equivalence relation (the least containing the reduction)
+;;; ---------------------------------------------------------------------------
+
+;;; To be confident of the definition of equiv-p we show that equiv-p is
+;;; the least equivalence relation containing reduction steps.
+
+;;; REMARK: To say it properly, we show that for the relation
+;;; "exists p such that (equiv-p x y p)".
+
+;;; An useful rule to deal with concatenation of proofs
+(local
+ (defthm proof-append
+   (implies (equal z (last-of-proof x p1))
+	    (equal (equiv-p x y (append p1 p2))
+		   (and (equiv-p x z p1)
+			(equiv-p z y p2))))))
+
+;;; The properties of equivalence relations are met by equiv-p
+
+(defthm equiv-p-reflexive
+  (equiv-p x x nil))
+
+(defthm equiv-p-symmetric
+  (implies (equiv-p x y p)
+	   (equiv-p y x (inverse-proof p))))
+
+(defthm equiv-p-transitive
+  (implies (and (equiv-p x y p1)
+		(equiv-p y z p2))
+	   (equiv-p x z (append p1 p2)))
+  :rule-classes nil)
+
+;;; REMARK: We have an "algebra" of proofs:
+;;;   - append for the concatenation of proofs
+;;;   - inverse-proof is already defined in abstract-proofs.lisp
+;;;   - nil is the identity.
+
+;;; Obviously, the reduction relaton is contained in equiv-p
+
+(defthm equiv-p-contains-reduction
+  (implies (legal x op)
+	   (equiv-p x (reduce-one-step x op)
+		   (list
+		    (make-r-step
+		     :elt1 x
+		     :elt2 (reduce-one-step x op)
+		     :direct t
+		     :operator op)))))
+
+
+;;; Let us assume that we have a relation eqv of equivalence, containing
+;;; the reduction steps, and let us show that it contains equiv-p
+
+(encapsulate
+ ((eqv (t1 t2) boolean))
+
+ (local (defun eqv (t1 t2) (declare (ignore t1 t2)) t))
+
+ (defthm eqv-contains-reduction
+   (implies (legal x op)
+	    (eqv x (reduce-one-step x op))))
+
+ (defthm eqv-reflexive
+   (eqv x x))
+
+ (defthm eqv-symmetric
+   (implies (eqv x y) (eqv y x)))
+
+ (defthm eqv-transitive
+   (implies (and (eqv x y) (eqv y z))
+            (eqv x z))))
+
+(defthm equiv-p-the-least-equivalence-containing-reduction
+  (implies (equiv-p x y p)
+	   (eqv x y))
+  :hints (("Subgoal *1/3" :use
+	   (:instance eqv-transitive (y (elt2 (car p)))
+		      (z y))
+           :in-theory (disable eqv-transitive))))
+
+
+;;; ----------------------------------------------------------------------------
+;;; 1.3 There are no equivalent and distinct normal forms
+;;; ----------------------------------------------------------------------------
+
+;;; Two lemmas
+
+(local
+  (defthm reducible-steps-up
+    (implies (and  (consp p) (steps-up p)
+		   (not (legal y (operator (last-elt p)))))
+ 	    (not (equiv-p x y p)))))
+
+
+(local
+ (defthm two-ireducible-connected-by-a-valley-are-equal
+   (implies (and (steps-valley p)
+		 (equiv-p x y p)
+		 (not (legal x (operator (first p))))
+		 (not (legal y (operator (last-elt p)))))
+	    (equal x y))
+   :rule-classes nil))
+
+;;; And the theorem
+
+(local
+ (defthm if-CR--two-ireducible-connected-are-equal
+   (implies (and (equiv-p x y p)
+		 (not (legal x (operator (first (transform-to-valley p)))))
+		 (not (legal y (operator (last-elt (transform-to-valley p))))))
+	    (equal x y))
+   :rule-classes nil
+   :hints (("Goal" :use (:instance
+			  two-ireducible-connected-by-a-valley-are-equal
+			  (p (transform-to-valley p)))))))
+
+;;; REMARK: although this lemma is weaker than the statement "every two
+;;; equivalent normal forms are equal" (we cannot state this with our
+;;; current language, see confluence-v0.lisp), it is a tool to show
+;;; equality of every two particular elements known to be equivalent and
+;;; irreducible.
+
+;;; ============================================================================
+;;; 2. Decidability of Church-Rosser and normalizing redutions
+;;; ============================================================================
+
+
+;;; ----------------------------------------------------------------------------
+;;; 2.1 Normal forms, definition and fundamental properties.
+;;; ----------------------------------------------------------------------------
+
+
+(defun normal-form (x) (last-of-proof x (proof-irreducible x)))
+
+
+(local
+ (defthm irreducible-normal-form (not (legal (normal-form x) op))))
+
+(local
+ (defthm equivalent-proof
+   (equiv-p x (normal-form x) (proof-irreducible x))))
+
+(local
+ (defthm proof-irreducible-atom-normal-form
+   (implies (atom (proof-irreducible x))
+	    (equal (normal-form x) x))))
+
+(local
+ (defthm proof-irreducible-consp-normal-form
+   (implies (consp (proof-irreducible x))
+	    (equal (elt2 (last-elt (proof-irreducible x))) (normal-form x)))))
+
+
+;;; We can disable normal-form (its fundamental properties are now
+;;; rewrite rules):
+
+(local (in-theory (disable normal-form)))
+
+
+;;; ----------------------------------------------------------------------------
+;;; 2.2  A decision algorithm for [<-reduce-one-step->]*
+;;; ----------------------------------------------------------------------------
+
+
+(defun r-equiv (x y)
+  (equal (normal-form x) (normal-form y)))
+
+;;; ············································································
+;;; 2.2.1 Completeness
+;;; ············································································
+
+;;; A proof between normal forms
+(local
+ (defun make-proof-between-normal-forms (x y p)
+   (append (inverse-proof (proof-irreducible x))
+	   p
+	   (proof-irreducible y))))
+
+;;;; Some needed lemmas
+
+(local
+ (defthm consp-inverse-proof
+   (iff (consp (inverse-proof p))
+	(consp p))))
+
+(local
+ (defthm last-elt-append
+   (implies (consp p2)
+	    (equal (last-elt (append p1 p2)) (last-elt p2)))))
+(local
+ (defthm last-elt-inverse-proof
+   (implies (consp p)
+	    (equal (last-elt (inverse-proof p))
+		   (inverse-r-step (car p))))))
+
+(local
+ (defthm first-element-of-proof-irreducible
+   (implies (consp (proof-irreducible x))
+	    (equal (elt1 (car (proof-irreducible x))) x))
+   :hints (("Goal" :use ((:instance
+			  first-element-of-equivalence
+			  (y (normal-form x)) (p (proof-irreducible
+						   x))))))))
+;;; The main lemma for completeness: the proof constructed is a proof
+;;; indeed.
+(local
+ (defthm make-proof-between-normal-forms-indeed
+   (implies (equiv-p x y p)
+	    (equiv-p (normal-form x)
+		     (normal-form y)
+		     (make-proof-between-normal-forms x y p)))))
+
+(local (in-theory (disable make-proof-between-normal-forms)))
+
+;;; COMPLETENESS
+
+(defthm r-equiv-complete
+  (implies (equiv-p x y p)
+	   (r-equiv x y))
+  :hints (("Goal" :use ((:instance
+			 if-CR--two-ireducible-connected-are-equal
+			 (x (normal-form x))
+			 (y (normal-form y))
+			 (p (make-proof-between-normal-forms x y p)))))))
+
+
+;;; ············································································
+;;; 2.2.1 Soundness
+;;; ············································································
+
+;;; A proof between x and y (if their normal forms are equal)
+
+(defun make-proof-common-n-f (x y)
+   (append (proof-irreducible x) (inverse-proof (proof-irreducible y))))
+
+;;; SOUNDNESS
+
+(defthm r-equiv-sound
+  (implies (r-equiv x y)
+	   (equiv-p x y (make-proof-common-n-f x y)))
+  :hints (("Goal" :use (:instance
+			       equiv-p-symmetric
+			       (x y)
+			       (y (normal-form y))
+			       (p (proof-irreducible y))))))
+
+;;; REMARK: :use is needed due to a weird behaviour that sometimes
+;;; ACL2 has with equalities in hypotesis.
+
+
+
+
+
+
+
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.acl2 b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.acl2
new file mode 100644
index 0000000..ac7f28a
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.acl2
@@ -0,0 +1,23 @@
+(value :q)
+(lp)
+
+(defconst *abstract-proofs-exports* 
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step 
+	     first-of-proof last-of-proof steps-up steps-down steps-valley 
+	     proof-before-valley proof-after-valley inverse-r-step inverse-proof 
+	     local-peak-p proof-measure proof-before-peak proof-after-peak 
+	     local-peak peak-element))
+
+(defconst *cnf-package-exports* 
+  (union-eq *acl2-exports* 
+	    (union-eq 
+	     *common-lisp-symbols-from-main-lisp-package* 
+	     *abstract-proofs-exports*)))
+
+(defpkg "CNF" *cnf-package-exports*)
+
+(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*))
+
+(defpkg "LCNF" (cons 'multiset-diff *cnf-package-exports*))
+
+(certify-book "local-confluence" ? t)
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp
new file mode 100644
index 0000000..9ca2fd1
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp
@@ -0,0 +1,471 @@
+;;; local-confluence.lisp
+;;; Convergent reduction relations have a decidable equivalence closure
+;;; Created: 1-11-99 Last modified: 11-10-00
+;;; =============================================================================
+
+
+;;; To certify this book:
+#|
+(in-package "ACL2")
+
+(defconst *abstract-proofs-exports*
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step
+    first-of-proof last-of-proof steps-up steps-down steps-valley
+    proof-before-valley proof-after-valley inverse-r-step inverse-proof
+    local-peak-p proof-measure proof-before-peak proof-after-peak
+    local-peak peak-element))
+
+(defconst *cnf-package-exports*
+  (union-eq *acl2-exports*
+	    (union-eq
+	     *common-lisp-symbols-from-main-lisp-package*
+	     *abstract-proofs-exports*)))
+
+(defpkg "CNF" *cnf-package-exports*)
+
+(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*))
+
+(defpkg "LCNF" (cons 'multiset-diff *cnf-package-exports*))
+
+(certify-book "local-confluence" 5)
+|#
+
+;;;
+(in-package "LCNF")
+
+(local (include-book "confluence"))
+
+(include-book "newman")
+
+
+;;; ****************************************************************************
+;;; LOCALLY CONFLUENT AND TERMINATING REDUCTION RELATIONS HAVE A
+;;; DECIDABLE EQUIVALENCE CLOSURE
+;;; ****************************************************************************
+
+
+;;; We prove that every noetherian, locally confluent reduction relation
+;;; has decidable equivalence closure. This is a good example of how
+;;; functional instantiation can be useful. This result can be easily
+;;; proved by functional instantiation of the results in the books
+;;; previously developed. Using confluence.lisp, we need to show that
+;;; the reduction relation is normalizing and has the Church-Rosser
+;;; property. And the Church-Rosser property can be proved by using
+;;; Newman's lemma, proved in newman.lisp. The normalizing property is
+;;; an easy consequence of noetherianity.
+
+;;; ============================================================================
+;;; 1. A Tool for functional instantation
+;;; ============================================================================
+
+;;; In this file we have to extensively use functional
+;;; instantiation of results previously proved. The functional
+;;; instantiations we have to carry out are always of the same kind:
+;;; the functional substitution relates functions with the same symbol
+;;; name but in different package and the same happen with individual
+;;; variables.  We define the following functions in :program
+;;; mode to provide a tool to make this kind of functional-instance
+;;; hints convenient.
+
+(local
+ (defun pkg-functional-instance-pairs (lemma-name symbols)
+   (declare (xargs :mode :program))
+   (if (endp symbols)
+       nil
+     (cons (list (acl2::intern-in-package-of-symbol
+		 (string (car symbols)) lemma-name)
+		 (car symbols))
+	   (pkg-functional-instance-pairs lemma-name (cdr symbols))))))
+
+(local
+ (defun pkg-functional-instance
+   (id lemma-name variable-symbols function-symbols)
+   (declare (xargs :mode :program))
+   (if (equal id (acl2::parse-clause-id "Goal"))
+       (list :use (list* :functional-instance
+			 (list* :instance
+				lemma-name
+				(pkg-functional-instance-pairs
+				 lemma-name variable-symbols))
+			 (pkg-functional-instance-pairs
+			  lemma-name function-symbols)))
+     nil)))
+
+
+;;; The function pkg-functional-instance computes a hint (see
+;;; computed-hints in the ACL2 manual) and is called
+;;; in the following way:
+
+;;; (pkg-functional-instance id lemma-name variable-symbols
+;;;                          function-symbols)
+
+;;; where:
+
+;;; id:               is always the variable acl2::id
+;;; lemma-name:       the name of the lemma to be instantiated
+;;;                   (including the package).
+;;; variable-symbols: the list of symbol names of variables to be
+;;;                   instantiated.
+;;; function-symbols: the list of symbol names of functions to be
+;;;                   instantiated.
+
+;;; The computed hint is the functional instantiation of the lemma-name,
+;;; relating each variable name and function name (of the package where
+;;; the lemma has been proved) to the same symbol name in the current
+;;; package.
+
+
+;;; ============================================================================
+;;; 2. Formalizing the hypothesis of the theorem
+;;; ============================================================================
+
+;;; REMARK: This section is exactly the same as in newman.lisp:
+;;; formalization of noetherianity and local confluence. Nevertheless,
+;;; since we have to compute normal forms and the function
+;;; proof-irreducible, we have to assume the existence of a reducibility
+;;; test given by a function reducible with the following properties for
+;;; every element x:
+;;; 1) When reducible returns non-nil, it returns a legal operator for x.
+;;; 2) When reducible returns nil, there are no legal operators for x.
+;;; See newman.lisp and confluence-v0.lisp for more details.
+
+
+;;; A noetherian partial order rel (used to justify noetherianity of the
+;;; reduction relation defined later)
+;;; .....................................................................
+
+(encapsulate
+ ((rel (x y) booleanp)
+  (fn (x) e0-ordinalp))
+
+
+ (local (defun rel (x y) (declare (ignore x y)) nil))
+ (local (defun fn (x) (declare (ignore x)) 1))
+
+ (defthm rel-well-founded-relation-on-mp
+   ;; modified for v2-8 ordinals changes
+   (and
+    (o-p (fn x))
+    (implies (rel x y)
+	     (o< (fn x) (fn y))))
+   :rule-classes (:well-founded-relation
+		  :rewrite))
+
+ (defthm rel-transitive
+   (implies (and (rel x y) (rel y z))
+	    (rel x z))))
+
+(in-theory (disable rel-transitive))
+
+
+;;; A noetherian and locally confluent reduction relation
+;;; ·····················································
+
+
+(encapsulate
+ ((legal (x u) boolean)
+  (reduce-one-step (x u) element)
+  (reducible (x) boolean)
+  (transform-local-peak (x) proof))
+
+ (local (defun legal (x u) (declare (ignore x u)) nil))
+ (local (defun reduce-one-step (x u) (+ x u)))
+ (local (defun reducible (x) (declare (ignore x)) nil))
+ (local (defun transform-local-peak (x) (declare (ignore x)) nil))
+
+
+ (defthm legal-reducible-1
+   (implies (reducible x) (legal x (reducible x))))
+
+ (defthm legal-reducible-2
+   (implies (not (reducible x)) (not (legal x u))))
+
+ (defun proof-step-p (s)
+   (let ((elt1 (elt1 s)) (elt2 (elt2 s))
+	 (operator (operator s)) (direct (direct s)))
+     (and (r-step-p s)
+	  (implies direct (and (legal elt1  operator)
+			       (equal (reduce-one-step elt1 operator)
+				    elt2)))
+	  (implies (not direct) (and (legal elt2 operator)
+				   (equal (reduce-one-step elt2 operator)
+					  elt1))))))
+
+ (defun equiv-p (x y p)
+   (if (endp p)
+       (equal x y)
+     (and (proof-step-p (car p))
+	  (equal x (elt1 (car p)))
+	  (equiv-p (elt2 (car p)) y (cdr p)))))
+
+; The following was added by Matt Kaufmann after ACL2 Version 3.4 because of
+; a soundness bug fix; see ``subversive'' in :doc note-3-5.
+ (defthm equiv-p-type
+   (booleanp (equiv-p x y p))
+   :rule-classes :type-prescription)
+
+ (defthm local-confluence
+   (let ((valley (transform-local-peak p)))
+     (implies (and (equiv-p x y p) (local-peak-p p))
+              (and (steps-valley valley)
+		   (equiv-p x y valley)))))
+
+ (defthm noetherian
+   (implies (legal x u) (rel (reduce-one-step x u) x))))
+
+
+;;; ============================================================================
+;;; 2. Theorem: The reduction relation has the Church-Rosser property
+;;; ============================================================================
+
+
+
+;;; REMARK: We show that it is possible to define a function
+;;; transform-to-valley with the propertiy of transforming every proof
+;;; ina an equivalent valley proof. This is done in newman.lisp, so
+;;; now we can functionally instantiate the main results proved there.
+;;; See newman.lisp for details.
+
+;;; Well-founded multiset extension of rel
+;;; ······································
+
+;(acl2::defmul-components rel)
+;The list of components is:
+; (REL REL-WELL-FOUNDED-RELATION-ON-MP T FN X Y)
+(local
+ (acl2::defmul (REL REL-WELL-FOUNDED-RELATION-ON-MP T FN X Y)))
+
+
+;;; Auxiliary functions in the definition of transform-to-valley
+;;; ···························································
+
+(local
+ (defun exists-local-peak (p)
+   (cond ((or (atom p) (atom (cdr p))) nil)
+	 ((and
+	   (not (direct (car p)))
+	   (direct (cadr p)))
+	  (and (proof-step-p (car p))
+	       (proof-step-p (cadr p))
+	       (equal (elt2 (car p)) (elt1 (cadr p)))))
+	 (t (exists-local-peak (cdr p))))))
+
+(local
+ (defun replace-local-peak (p)
+   (cond ((or (atom p) (atom (cdr p))) nil)
+	 ((and (not (direct (car p))) (direct (cadr p)))
+	  (append (transform-local-peak (list (car p) (cadr p)))
+		  (cddr p)))
+	 (t (cons (car p) (replace-local-peak (cdr p)))))))
+
+
+;;; transform-to-valley terminates
+;;; ······························
+
+;;; By functional instantiation of the same result in newman.lisp
+
+(local
+ (defthm transform-to-valley-admission
+   (implies (exists-local-peak p)
+	    (mul-rel (proof-measure (replace-local-peak p))
+		     (proof-measure p)))
+
+   :rule-classes nil
+   :hints ((pkg-functional-instance
+	    acl2::id
+	    'nwm::transform-to-valley-admission
+	    '(p) '(fn legal forall-exists-rel-bigger reduce-one-step
+		      proof-step-p equiv-p rel mul-rel
+		      exists-local-peak replace-local-peak
+		      transform-local-peak exists-rel-bigger))
+	   ("Subgoal 10" :in-theory (enable rel-transitive)))))
+
+
+
+;;; Definition of transform-to-valley
+;;; ·································
+
+(local
+ (defun transform-to-valley (p)
+   (declare (xargs :measure (proof-measure p)
+		   :well-founded-relation mul-rel
+		   :hints (("Goal" :use
+			    (:instance transform-to-valley-admission)))))
+
+  (if (not (exists-local-peak p))
+      p
+    (transform-to-valley (replace-local-peak p)))))
+
+
+;;; Properties of transform-to-valley: the Church-Rosser property
+;;; ·····························································
+
+;;; By functional instantiation of the same results in newman.lisp
+
+
+(local
+ (defthm equiv-p-x-y-transform-to-valley
+   (implies (equiv-p x y p)
+	    (equiv-p x y (transform-to-valley p)))
+   :hints ((pkg-functional-instance
+	    acl2::id
+	    'nwm::equiv-p-x-y-transform-to-valley
+	    '(p x y)
+	    '(fn transform-to-valley reduce-one-step legal
+		 proof-step-p equiv-p rel exists-local-peak
+		 replace-local-peak transform-local-peak)))))
+
+(local
+ (defthm valley-transform-to-valley
+   (implies (equiv-p x y p)
+	    (steps-valley (transform-to-valley p)))
+   :hints ((pkg-functional-instance
+	    acl2::id
+	    'nwm::valley-transform-to-valley
+	    '(p x y)
+	    '(fn transform-to-valley reduce-one-step legal
+		 proof-step-p equiv-p rel exists-local-peak
+		 replace-local-peak transform-local-peak)))))
+
+
+
+;;; ============================================================================
+;;; 3. Theorem: The reduction relation is normalizing
+;;; ============================================================================
+
+;;; To instantiate the results in confluence.lisp, we have to define a
+;;; function proof-irreducible and prove the properties assumed there as
+;;; axioms.
+
+;;; Definition of proof-irreducible
+;;; ·······························
+
+;;; REMARK: Iteratively apply reduction steps until an irreducible
+;;; element is found. This function termination can be justified by the
+;;; well-founded relation rel. That is, the normal-form computation
+;;; terminates because the reduction relation is assumed to be
+;;; noetherian.
+
+(defun proof-irreducible (x)  (declare (xargs :measure x
+					       :well-founded-relation rel))
+  (let ((red (reducible x)))
+    (if (not red)
+	nil
+      (cons (make-r-step
+	      :direct t :elt1 x :elt2 (reduce-one-step x red)
+	      :operator red)
+	    (proof-irreducible (reduce-one-step x red))))))
+
+
+;;; Properties of proof-irreducible (normalizing property)
+;;; ······················································
+
+;;; REMARK: These are the assumed proerties of proof-irreducible in
+;;; confluence.lisp, in rewriting rule form:
+
+(local
+ (defthm normalizing-1
+   (let ((y (elt2 (last-elt (proof-irreducible x)))))
+     (implies (consp (proof-irreducible x))
+	      (and (equiv-p x y (proof-irreducible x))
+		   (not (legal y op)))))))
+(local
+ (defthm normalizing-2
+   (implies
+    (not (consp (proof-irreducible x)))
+    (not (legal x op)))))
+
+;;; ============================================================================
+;;; 4. Theorem: The equivalence closure is decidable
+;;; ============================================================================
+
+
+;;; ----------------------------------------------------------------------------
+;;; 4.1 Definition of a decison procedure for <--*--reduce-one-step--*-->
+;;; ----------------------------------------------------------------------------
+
+(defun normal-form (x)
+  (declare (xargs :measure x
+		  :well-founded-relation rel))
+  (let ((red (reducible x)))
+    (if (not red)
+	x
+      (normal-form (reduce-one-step x red)))))
+
+(defun r-equivalent (x y)
+  (equal (normal-form x) (normal-form y)))
+
+
+;;; REMARK: Note that this is not exactly the same definition of the
+;;; decision procedure given in confluence.lisp. The point is that in
+;;; confluence.lisp the normal-form computation is through the proof
+;;; given by proof-irreducible. In order to functionally instantiate the
+;;; result of confluence.lisp, we show that it is the same function.
+
+
+;;; This is the same function as r-equiv in confluence.lisp
+;;; ·······················································
+
+;;; REMARK: normal-form-aux is analogue NWM::normal-form, but
+;;; normal-form is more eficcient. The same for r-equiv.
+
+(local
+ (defun normal-form-aux (x) (last-of-proof x (proof-irreducible x))))
+
+(local
+ (defthm normal-form-aux-normal-form
+   (equal (normal-form x)
+	  (normal-form-aux x))))
+
+(local
+ (defun r-equiv (x y)
+   (equal (normal-form-aux x) (normal-form-aux y))))
+
+
+
+;;; ----------------------------------------------------------------------------
+;;; 4.2 Soundness and completeness
+;;; ----------------------------------------------------------------------------
+
+;;; Completeness
+;;; ············
+
+;;; By functional instantiation of the same results in confluence.lisp
+
+(defthm r-equivalent-complete
+  (implies (equiv-p x y p)
+	   (r-equivalent x y))
+
+  :rule-classes nil
+  :hints ((pkg-functional-instance
+	   acl2::id
+	   'cnf::r-equiv-complete
+	   '(p x y)
+	   '(legal proof-step-p r-equiv
+	    equiv-p reduce-one-step proof-irreducible
+	    transform-to-valley normal-form))))
+
+
+
+;;; Soundness
+;;; ·········
+
+;;; By functional instantiation of the same results in confluence.lisp
+
+;;; Skolem function
+(defun make-proof-common-n-f (x y)
+   (append (proof-irreducible x) (inverse-proof (proof-irreducible y))))
+
+
+(defthm r-equivalent-sound
+  (implies (r-equivalent x y)
+	   (equiv-p x y (make-proof-common-n-f x y)))
+
+  :hints ((pkg-functional-instance
+	   acl2::id
+	   'cnf::r-equiv-sound
+	   '(x y)
+	   '(legal make-proof-common-n-f proof-step-p
+		   r-equiv  equiv-p
+		   reduce-one-step proof-irreducible transform-to-valley
+		   normal-form))))
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/newman.acl2 b/books/workshops/2000/ruiz/multiset/examples/newman/newman.acl2
new file mode 100644
index 0000000..83e8337
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/newman.acl2
@@ -0,0 +1,19 @@
+(value :q)
+(lp)
+
+(defconst *abstract-proofs-exports* 
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step 
+	     first-of-proof last-of-proof steps-up steps-down steps-valley 
+	     proof-before-valley proof-after-valley inverse-r-step inverse-proof 
+	     local-peak-p proof-measure proof-before-peak proof-after-peak 
+	     local-peak peak-element))
+
+(defconst *cnf-package-exports* 
+  (union-eq *acl2-exports* 
+	    (union-eq 
+	     *common-lisp-symbols-from-main-lisp-package* 
+	     *abstract-proofs-exports*)))
+
+(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*))
+
+(certify-book "newman" ? t)
diff --git a/books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp b/books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp
new file mode 100644
index 0000000..c6406f1
--- /dev/null
+++ b/books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp
@@ -0,0 +1,994 @@
+;;; newman.lisp
+;;; A mechanical proof of Newman's lemma for abstract reduction relations
+;;; Created: 6-8-99 Last revison: 11-10-00
+;;; =============================================================================
+
+;;; To certify this book:
+#|
+(in-package "ACL2")
+
+(defconst *abstract-proofs-exports*
+  '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step
+    first-of-proof last-of-proof steps-up steps-down steps-valley
+    proof-before-valley proof-after-valley inverse-r-step inverse-proof
+    local-peak-p proof-measure proof-before-peak proof-after-peak
+    local-peak peak-element))
+
+(defconst *cnf-package-exports*
+  (union-eq *acl2-exports*
+	    (union-eq
+	     *common-lisp-symbols-from-main-lisp-package*
+	     *abstract-proofs-exports*)))
+
+(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*))
+
+(certify-book "newman" 3)
+|#
+
+
+(in-package "NWM")
+
+(include-book "../../defmul")
+(local (include-book "../../../../../../ordinals/ordinals-without-arithmetic"))
+
+(include-book "abstract-proofs")
+
+;;; *******************************************************************
+;;; A MECHANICAL PROOF OF NEWMAN'S LEMMA:
+;;; For terminating relations, local confluence implies
+;;; confluence [see "Term Rewriting and all that..." (Baader & Nipkow),
+;;; chapter 2, pp. 28-29]
+;;; *******************************************************************
+
+;;; ============================================================================
+;;; 1. Formalizing the statement of the theorem
+;;; ============================================================================
+
+
+;;; ----------------------------------------------------------------------------
+;;; 1.1 A noetherian partial order
+;;; ----------------------------------------------------------------------------
+
+
+;;; A general noetherian partial order rel is defined.
+;;; It will be used to justify noetherianity of the reduction relation,
+;;; based on the following meta-theorem:
+;;; "A reduction is noetherian iff it is contained in a noetherian
+;;;  partial order"
+
+;;; REMARK: Transitivity is required, but this is not a real
+;;; restriction, since a reduction is noetherian iff its included in a
+;;; transitive and noetherian relation.  We need it because transitive
+;;; closure, in general, is not decidable even if the relation is
+;;; decidable, so we cannot define the transitive closure of a relation.
+
+
+(encapsulate
+ ((rel (x y) booleanp)
+  (fn (x) e0-ordinalp))
+
+ (local (defun rel (x y) (declare (ignore x y)) nil))
+ (local (defun fn (x) (declare (ignore x)) 1))
+
+ (defthm rel-well-founded-relation-on-mp
+   ;; modified for v2-8 ordinals changes
+   (and
+    (o-p (fn x))
+    (implies (rel x y)
+	     (o< (fn x) (fn y))))
+   :rule-classes (:well-founded-relation
+		  :rewrite))
+
+ (defthm rel-transitive
+   (implies (and (rel x y) (rel y z))
+ 	    (rel x z))
+   :rule-classes nil))
+
+
+;;; A theorem: irreflexivity of rel
+
+(local
+ (defthm rel-irreflexive
+   (not (rel x x))
+   :hints (("Goal"
+	    :use ((:instance rel-well-founded-relation-on-mp
+			     (y x)))))))
+
+;;; REMARK: e0-ord-irreflexive (in multiset.lisp) is needed
+
+;;; ----------------------------------------------------------------------------
+;;; 1.2 A noetherian locally confluent relation
+;;; ----------------------------------------------------------------------------
+
+;;; A general reduction is given by two functions: reduction-one-step
+;;; and legal. Noetherianity is justified by inclusion in the previously
+;;; defined well-founded relation on rel. Local confluence is defined by
+;;; the existence of a function transform-local-peak, assumed to
+;;; transform every local peak to an equivalent valley proof.
+
+(encapsulate
+ ((legal (x u) boolean)
+  (reduce-one-step (x u) element)
+  (transform-local-peak (x) proof))
+
+ (local (defun legal (x u) (declare (ignore x u)) nil))
+ (local (defun reduce-one-step (x u) (+ x u)))
+ (local (defun transform-local-peak (x) (declare (ignore x)) nil))
+
+
+ (defun proof-step-p (s)
+   (let ((elt1 (elt1 s)) (elt2 (elt2 s))
+	 (operator (operator s)) (direct (direct s)))
+     (and (r-step-p s)
+	  (implies direct (and (legal elt1  operator)
+			       (equal (reduce-one-step elt1 operator)
+				    elt2)))
+	  (implies (not direct) (and (legal elt2 operator)
+				   (equal (reduce-one-step elt2 operator)
+					  elt1))))))
+
+ (defun equiv-p (x y p)
+   (if (endp p)
+       (equal x y)
+     (and (proof-step-p (car p))
+	  (equal x (elt1 (car p)))
+	  (equiv-p (elt2 (car p)) y (cdr p)))))
+
+ (defthm local-confluence
+   (let ((valley (transform-local-peak p)))
+     (implies (and (equiv-p x y p) (local-peak-p p))
+              (and (steps-valley valley)
+		   (equiv-p x y valley)))))
+
+ (defthm noetherian
+   (implies (legal x u) (rel (reduce-one-step x u) x))))
+
+;;; ----------------------------------------------------------------------------
+;;; 1.3 Our goal
+;;; ----------------------------------------------------------------------------
+
+;;; REMARK: We will prove that the reduction relation has the
+;;; Church-Rosser property, instead of showing confluence (which is
+;;; equivalent).
+
+;;; Our definition of the Church-Rosser property (see confluence.lisp) is:
+;;; (defthm Chuch-Rosser-property
+;;;   (let ((valley (transform-to-valley p)))
+;;;     (implies (equiv-p x y p)
+;;;	      (and (steps-valley valley)
+;;;		   (equiv-p x y valley)))))
+;;; So our goal is to define transform-to-valley with these properties.
+
+
+;;; ----------------------------------------------------------------------------
+;;; 1.4 Some useful stuff
+;;; ----------------------------------------------------------------------------
+
+
+;;; Since equiv-p is "infected" (see subversive-recursions in the ACL2
+;;; manual), we have to specify the induction scheme.  Suggested by
+;;; M. Kaufman
+
+(local
+ (defun induct-equiv-p (x p) (declare (ignore x))
+   (if (endp p)
+       t
+     (induct-equiv-p (elt2 (car p)) (cdr p)))))
+
+(local
+ (defthm equiv-p-induct t
+   :rule-classes
+   ((:induction :pattern (equiv-p x y p)
+        	:condition t
+	        :scheme (induct-equiv-p x p)))))
+
+
+;;; Proof-p: sometimes it will be useful to talk about proofs without
+;;; mentioning equiv-p
+
+(local
+ (defun proof-p (p)
+   (if (atom p)
+       t
+     (and (proof-step-p (car p))
+	 (if (atom (cdr p))
+	     t
+	   (and (equal (elt2 (car p)) (elt1 (cadr p)))
+		(proof-p (cdr p))))))))
+
+;;;; Relation between proof-p y equiv-p
+
+(local
+ (defthm equiv-p-proof-p
+   (implies (equiv-p x y p)
+	    (proof-p p))))
+
+;;; A rule without free variables (almost) expressing local conf.
+
+(local
+ (defthm local-confluence-w-f-v
+   (implies (and (proof-p p) (local-peak-p p))
+	    (and (steps-valley (transform-local-peak p))
+		 (proof-p (transform-local-peak p))))
+    :hints (("Goal" :use (:instance local-confluence
+				    (x (elt1 (car p)))
+				    (y (elt2 (last-elt p))))
+	     :in-theory (disable local-confluence)))))
+
+;;; ============================================================================
+;;; 2. Towards the definition of transform-to-valley
+;;; ============================================================================
+
+
+(defun exists-local-peak (p)
+  (cond ((or (atom p) (atom (cdr p))) nil)
+	((and
+	  (not (direct (car p)))
+	  (direct (cadr p)))
+	  (and (proof-step-p (car p))
+	       (proof-step-p (cadr p))
+	       (equal (elt2 (car p)) (elt1 (cadr p)))))
+	(t (exists-local-peak (cdr p)))))
+
+(defun replace-local-peak (p)
+  (cond ((or (atom p) (atom (cdr p))) nil)
+	((and (not (direct (car p))) (direct (cadr p)))
+	 (append (transform-local-peak (list (car p) (cadr p)))
+		 (cddr p)))
+	(t (cons (car p) (replace-local-peak (cdr p))))))
+
+
+;;; The idea is to define a function like this (i.e. to replace local peaks
+;;; iteratively until there are no local peaks left)
+
+;(defun transform-to-valley (p)
+;  (if (not (exists-local-peak p))
+;      p
+;    (transform-to-valley (replace-local-peak p))))
+
+
+;;; As expected, this function is not admitted without help from the
+;;; user (the length of the proof (replace-local-peak p) may be greater
+;;; than the length of p). So the hard part of the theorem is to provide
+;;; that help as a suitable set of rules and hints, to get the admission
+;;; of transform-to-valley.
+
+
+;;; ============================================================================
+;;; 3. Admission of transform-to-valley
+;;; ============================================================================
+
+;;; ----------------------------------------------------------------------------
+;;; 3.1 A multiset measure
+;;; ----------------------------------------------------------------------------
+
+
+;;; We will lead the prover to the admission of the theorem by means of
+;;; a multiset measure. The idea is to assign to every proof the
+;;; multiset of elements involved in it. These multisets are compared
+;;; w.r.t. the well-founded multiset relation induced by rel (mul-rel)
+
+;;; We define the well-founded extension of rel to multisets.
+;;; See defmul.lisp
+
+
+; (acl2::defmul-components rel)
+;The list of components is:
+; (REL REL-WELL-FOUNDED-RELATION-ON-MP T FN X Y)
+
+(acl2::defmul (REL REL-WELL-FOUNDED-RELATION-ON-MP T FN X Y)
+	      :verify-guards t)
+
+;;; This defmul call define the well-founded multiset relation mul-rel,
+;;; induced by the well-founded relation rel.
+
+;;; So our admission hint will be (see the definition of proof-measure
+;;; in abstract-proofs.lisp).
+
+;(defun transform-to-valley (p)
+;  (declare (xargs :measure (proof-measure p)
+;		   :well-founded-relation mul-rel))
+;  (if (not (exists-local-peak p))
+;      p
+;    (transform-to-valley (replace-local-peak p))))
+
+
+
+;;; ----------------------------------------------------------------------------
+;;; 3.2 The proof of the main lemma for admission of transform-to-valley
+;;; ----------------------------------------------------------------------------
+
+;;; In order to admit transform-to-valley, our main goal is:
+
+;;; (defthm transform-to-valley-admission
+;;;   (implies (exists-local-peak p)
+;;; 	   (mul-rel (proof-measure (replace-local-peak p))
+;;; 		    (proof-measure p)))
+;;;   :rule-classes nil)
+
+;;; This conjecture generates the following two goals:
+
+;;; Subgoal 2
+;;; (IMPLIES (EXISTS-LOCAL-PEAK P)
+;;;          (CONSP (MULTISET-DIFF (PROOF-MEASURE P)
+;;;                                (PROOF-MEASURE (REPLACE-LOCAL-PEAK P))))).
+;;; Subgoal 1
+;;; (IMPLIES (EXISTS-LOCAL-PEAK P)
+;;;          (FORALL-EXISTS-REL-BIGGER
+;;;               (MULTISET-DIFF (PROOF-MEASURE (REPLACE-LOCAL-PEAK P))
+;;;                              (PROOF-MEASURE P))
+;;;               (MULTISET-DIFF (PROOF-MEASURE P)
+;;;                              (PROOF-MEASURE (REPLACE-LOCAL-PEAK P))))).
+
+;;; In the sequel, we build a collection of rules to prove these two goals.
+
+;;; ············································································
+;;; 3.2.1 Removing initial and final common parts
+;;; ············································································
+
+
+(local
+ (defthm proof-peak-append
+   (implies (exists-local-peak p)
+	    (equal
+	     (append (proof-before-peak p)
+		     (append (local-peak p)
+			     (proof-after-peak p)))
+	     p))
+   :rule-classes (:elim :rewrite)))
+
+;;; REMARK: This decomposition only makes sense when (exists-local-peak
+;;; p). The elim rule is for avoiding :use.
+
+
+;;; We use a rewrite rule to decompose proof-measure of proofs with
+;;; local peaks. This rule implements a rewriting rule strategy: every
+;;; proof with a local peak can be divided into three pieces (w.r.t. its
+;;; complexity)
+
+(local
+ (defthm proof-measure-with-local-peak
+   (implies (exists-local-peak p)
+	    (equal (proof-measure p)
+		   (append (proof-measure (proof-before-peak p))
+			   (proof-measure (local-peak p))
+			   (proof-measure (proof-after-peak p)))))))
+
+
+(local (in-theory (disable proof-peak-append)))
+
+;;; The following rule helps to express the proof-measure of
+;;; (replace-local-peak p) in a similar way than the previous rule does
+;;; with the proof-measure of p.
+
+(local
+ (defthm replace-local-peak-another-definition
+   (implies (exists-local-peak p)
+	    (equal (replace-local-peak p)
+		   (append (proof-before-peak p)
+			   (append (transform-local-peak (local-peak p))
+				   (proof-after-peak p)))))))
+
+
+;;; The above rules rewrite the proof measures of p and
+;;; (replace-local-peak p) in a way such that the initial and final
+;;; common parts are explicit. In this way the rules
+;;; multiset-diff-append-1 and multiset-diff-append-2 rewrite the
+;;; expression, simplifying the common parts (see multiset.lisp and
+;;; defmul.lisp to see also the role of the congruence rules generated
+;;; by the above defmul call). The simplified goals now are:
+
+;;; Subgoal 2'
+;;; (IMPLIES
+;;;  (EXISTS-LOCAL-PEAK P)
+;;;  (CONSP
+;;;      (MULTISET-DIFF (PROOF-MEASURE (LOCAL-PEAK P))
+;;;                     (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))))).
+
+;;; Subgoal 1'
+;;; (IMPLIES
+;;;  (EXISTS-LOCAL-PEAK P)
+;;;  (FORALL-EXISTS-REL-BIGGER
+;;;      (MULTISET-DIFF (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))
+;;;                     (PROOF-MEASURE (LOCAL-PEAK P)))
+;;;      (MULTISET-DIFF (PROOF-MEASURE (LOCAL-PEAK P))
+;;;                     (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))))).
+
+
+
+;;; ············································································
+;;; 3.2.2 Removing the first element of the local peak
+;;; ············································································
+
+;;; First, let's prove that the local peak and the transformed are
+;;; proofs with the same endpoints, so their proof measures have the
+;;; same first element. This will be useful in 3.2.3 where we will look
+;;; for an explicit reference to the peak-element of the local peak.
+
+(local
+ (defthm local-peak-equiv-p
+   (implies (exists-local-peak p)
+	    (equiv-p (elt1 (car (local-peak p)))
+		     (elt2 (cadr (local-peak p)))
+		     (local-peak p)))))
+
+(local
+ (defthm transform-local-peak-equiv-p
+   (implies (exists-local-peak p)
+	    (equiv-p (elt1 (car (local-peak p)))
+		     (elt2 (cadr (local-peak p)))
+		     (transform-local-peak (local-peak p))))))
+
+
+;;; Using the above, now we will see that we can simplify further the
+;;; multiset difference of the measures of the complexity of the proofs,
+;;; removing the first element. This is not so easy as one can think at
+;;; first sight, since there is a subtle point: the transformed proof
+;;; can be empty.
+
+
+(local
+ (defthm consp-proof-measure
+   (equal (consp (proof-measure p))
+	  (consp p))))
+
+(local
+ (defthm car-equiv-p-proof-measure
+   (implies (and (equiv-p x y p)
+		 (consp p))
+	    (equal (car (proof-measure p)) x))))
+
+;;; The main lemma of this sub-subsection. Note how we distinguish two
+;;; cases: proofs empty or not.
+
+(local
+ (defthm multiset-diff-proof-measure
+   (implies (and (equiv-p x y p1)
+		 (equiv-p x z p2))
+	    (equal (multiset-diff
+		    (proof-measure p1)
+		    (proof-measure p2))
+		   (if (consp p1)
+		       (if (consp p2)
+			   (multiset-diff (cdr (proof-measure p1))
+					  (cdr (proof-measure p2)))
+			 (proof-measure p1))
+		     nil)))
+   :rule-classes nil))
+
+(local
+ (defthm consp-local-peak
+   (implies (exists-local-peak p)
+	    (consp (local-peak p)))
+   :rule-classes :type-prescription))
+
+;;; And now the two rules needed for the intended simplification
+
+(local
+ (defthm multiset-diff-proof-measure-local-peak-transform-1
+   (implies (exists-local-peak p)
+	    (equal
+	     (multiset-diff (proof-measure (transform-local-peak (local-peak p)))
+			    (proof-measure (local-peak p)))
+	     (if (consp (transform-local-peak (local-peak p)))
+		 (multiset-diff
+		  (cdr (proof-measure (transform-local-peak (local-peak p))))
+		  (cdr (proof-measure (local-peak p))))
+		 nil)))
+   :hints (("Goal" :use
+	    (:instance multiset-diff-proof-measure
+		       (x (elt1 (car (local-peak p))))
+		       (y (elt2 (cadr (local-peak p))))
+		       (z (elt2 (cadr (local-peak p))))
+		       (p1 (transform-local-peak (local-peak p)))
+		       (p2 (local-peak p)))))))
+
+
+(local
+ (defthm multiset-diff-proof-measure-local-peak-transform-2
+   (implies (exists-local-peak p)
+	    (equal
+	     (multiset-diff
+	      (proof-measure (local-peak p))
+	      (proof-measure (transform-local-peak (local-peak p))))
+	    (if (consp (transform-local-peak (local-peak p)))
+		(multiset-diff
+		 (cdr (proof-measure (local-peak p)))
+		 (cdr (proof-measure (transform-local-peak (local-peak p)))))
+	      (proof-measure (local-peak p)))))
+   :hints (("Goal" :use
+	    (:instance multiset-diff-proof-measure
+		       (x (elt1 (car (local-peak p))))
+		       (y (elt2 (cadr (local-peak p))))
+		       (z (elt2 (cadr (local-peak p))))
+		       (p2 (transform-local-peak (local-peak p)))
+		       (p1 (local-peak p)))))))
+
+;;; REMARK: it could seem that in the lemma multiset-diff-proof-measure
+;;; variables x, y and z are not needed and that proof-p could be used
+;;; instead of equiv-p. But we think that in that case, to deal with the
+;;; empty proof would be somewhat unnatural.
+
+
+;;; With the rules we have at this moment, our unresolved goals are
+;;; simplified to:
+
+;;; Subgoal 2.2
+;;; (IMPLIES
+;;;   (AND (EXISTS-LOCAL-PEAK P)
+;;;        (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))
+;;;   (CONSP (MULTISET-DIFF
+;;;               (CDR (PROOF-MEASURE (LOCAL-PEAK P)))
+;;;               (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))).
+
+;;; Subgoal 1.2
+;;; (IMPLIES
+;;;  (AND (EXISTS-LOCAL-PEAK P)
+;;;       (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))
+;;;  (FORALL-EXISTS-REL-BIGGER
+;;;    (MULTISET-DIFF (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))
+;;;                   (CDR (PROOF-MEASURE (LOCAL-PEAK P))))
+;;;    (MULTISET-DIFF
+;;;         (CDR (PROOF-MEASURE (LOCAL-PEAK P)))
+;;;         (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))).
+
+
+;;; ············································································
+;;; 3.2.3 An explicit reference to the peak-element
+;;; ············································································
+
+;;; Definition and properties of peak-element
+;;; ·········································
+
+;;; See the definition in abstract-proofs.lisp
+
+(local
+ (defthm peak-element-member-proof-measure-local-peak
+   (implies (exists-local-peak p)
+	    (member (peak-element p) (proof-measure (local-peak p))))))
+
+(local
+ (defthm peak-element-rel-1
+   (implies (exists-local-peak p)
+	    (rel (elt1 (car (local-peak p)))
+		 (peak-element p)))))
+
+(local
+ (defthm peak-element-rel-2
+   (implies (exists-local-peak p)
+	    (rel (elt2 (cadr (local-peak p)))
+		 (peak-element p)))))
+
+(local
+ (defthm cdr-proof-measure-local-peak
+   (implies (exists-local-peak p)
+	    (equal (cdr (proof-measure (local-peak p)))
+		   (list (peak-element p))))))
+
+(local (in-theory (disable peak-element)))
+
+
+;;; Now our unresolved goals reduces to (note the explicit reference to
+;;; the peak element):
+
+;;; Subgoal 2.2
+;;; (IMPLIES
+;;;   (AND (EXISTS-LOCAL-PEAK P)
+;;;        (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))
+;;;   (CONSP (MULTISET-DIFF
+;;;               (LIST (PEAK-ELEMENT P))
+;;;               (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))).
+
+;;; Subgoal 1.2
+;;; (IMPLIES
+;;;  (AND (EXISTS-LOCAL-PEAK P)
+;;;       (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))
+;;;  (FORALL-EXISTS-REL-BIGGER
+;;;      (ACL2::REMOVE-ONE
+;;;            (PEAK-ELEMENT P)
+;;;            (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))))
+;;;      (MULTISET-DIFF
+;;;           (LIST (PEAK-ELEMENT P))
+;;;           (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))).
+
+
+;;; ············································································
+;;; 3.2.4 The peak element is bigger than any element of
+;;; (transform-local-peak (local-peak p))
+;;; ············································································
+
+;;; Definition of being bigger (w.r.t rel) than every element of a list
+;;; ···································································
+
+(local
+ (defun rel-bigger-than-list (x l)
+   (if (atom l)
+       t
+     (and (rel (car l) x) (rel-bigger-than-list x (cdr l))))))
+
+
+;;; Conditions assuring that an element m is rel-bigger-than-list than
+;;; the elements of the proof-measure of a proof, when the proof is,
+;;; respectively, steps-up or steps-down:
+;;; ···································································
+
+;;; A previous lemma: transitivity of rel is needed here
+
+(local
+ (defthm transitive-reduction
+   (implies (and
+             (legal e1 op)
+             (rel e1 m))
+            (rel (reduce-one-step e1 op) m))
+   :hints (("Goal"
+            :use (:instance rel-transitive
+                            (x (reduce-one-step e1 op)) (y e1) (z m))))))
+
+;;; And the two lemmas
+
+(local
+ (defthm steps-down-proof-measure-w-f-v
+   (implies (and (proof-p p) (steps-down p))
+            (iff (rel-bigger-than-list m (proof-measure p))
+                 (if (consp p)
+                     (rel (elt1 (car p)) m)
+                   t)))))
+
+(local
+ (defthm steps-up-proof-measure-w-f-v
+   (implies (and (proof-p p) (steps-up p)
+                 (if (consp p) (rel (elt2 (last-elt p)) m) t))
+            (rel-bigger-than-list m (proof-measure p)))))
+
+;;; REMARKS:
+;;; 1) The reverse implication in the steps-up case is not true as in
+;;; the steps-down case. The reason is that the proof measure does not
+;;; contain the final endpoint.
+
+;;; 2) The form of the rule allows one to distinguish between p empty or
+;;; non-empty.
+
+
+;;; In order to apply the two lemmas above we try to split
+;;; (transform-local-peak (local-peak p)) in two proofs: the proof
+;;; before the valley (steps-up) and the proof after the valley
+;;; (steps-down). The following lemmas are needed for that purpose.
+;;; ····································································
+
+;;; If p is a proof, so they are the proofs after and before the
+;;; valley.
+
+(local
+ (defthm proof-p-two-pieces-of-a-valley
+   (implies (proof-p p)
+            (and (proof-p (proof-before-valley p))
+                 (proof-p (proof-after-valley p))))))
+
+;;; rel-bigger-than-list when the list is splitted in two pieces
+
+(local
+ (defthm rel-bigger-than-list-append
+   (equal
+    (rel-bigger-than-list x (append l1 l2))
+    (and (rel-bigger-than-list x l1)
+         (rel-bigger-than-list x l2)))))
+
+
+
+;;; REMARK: In abstract-proofs.lisp it is also shown that
+;;; (proof-before-valley p) is steps-up and that when p is a valley then
+;;; (proof-after-valley p) is steps-down. And also the lemma
+;;; proof-valley-append splits the proof in these two pieces.
+
+
+;;; The transformed proof is a valley
+;;; ·································
+
+(local
+ (defthm local-peak-local-peak-p
+   (implies (exists-local-peak p)
+            (local-peak-p (local-peak p)))))
+
+
+(local
+ (defthm exists-local-peak-implies-proof-p-trasform-local-peak
+   (implies (exists-local-peak p)
+	    (proof-p (local-peak p)))))
+
+(local
+ (defthm transform-local-peak-steps-valley
+   (implies (exists-local-peak p)
+	    (steps-valley (transform-local-peak (local-peak p))))))
+
+;;; We show a simplified expression of the endpoints of
+;;; (transform-local-peak (local-peak p)) In this way, the lemmas
+;;; peak-element-rel-1 and peak-element-rel-2 can be used to reveal the
+;;; hypothesis of steps-down-proof-measure-w-f-v and
+;;; steps-up-proof-measure-w-f-v (and then prove that the peak-element
+;;; is bigger than every element of the complexities of the
+;;; proof-after-valley and the proof-before-valley, respectively.
+;;; ····································································
+
+
+
+(local
+ (encapsulate
+  ()
+  (local
+   (defthm endpoints-of-a-proof
+     (implies (and (equiv-p x y p) (consp p))
+	      (and (equal (elt1 (car p)) x)
+		   (equal (elt2 (last-elt p)) y)))))
+
+  (defthm endpoints-of-transform-of-a-local-peak
+    (implies (and (exists-local-peak p)
+		  (consp (transform-local-peak (local-peak p))))
+	     (and (equal (elt1 (car (transform-local-peak (local-peak p))))
+			 (elt1 (car (local-peak p))))
+		  (equal (elt2 (last-elt (transform-local-peak (local-peak p))))
+			 (elt2 (cadr (local-peak p))))))
+    :hints (("Goal" :use (:instance endpoints-of-a-proof
+				    (x (elt1 (car (local-peak p))))
+				    (y (elt2 (cadr (local-peak p))))
+				    (p (transform-local-peak (local-peak p)))))))))
+
+
+;;; Some technical lemmas
+;;; ·····················
+
+(local
+ (defthm consp-proof-after-proof-instance
+   (let ((q (transform-local-peak (local-peak p))))
+     (implies (consp (proof-after-valley q))
+              (consp q)))))
+
+(local
+ (defthm consp-proof-before-proof-instance
+   (let ((q (transform-local-peak (local-peak p))))
+     (implies (consp (proof-before-valley q))
+              (consp q)))))
+
+
+;;; And finally, the intended lemma
+;;; ·······························
+
+(local
+ (defthm valley-rel-bigger-peak-lemma
+   (implies (exists-local-peak p)
+            (rel-bigger-than-list
+             (peak-element p)
+             (proof-measure (transform-local-peak (local-peak p)))))
+   :hints (("Goal" :use (:instance acl2::proof-valley-append
+                                   (acl2::p
+                                    (transform-local-peak (local-peak p))))))))
+
+
+;;; ············································································
+;;; 3.2.5 Using valley-rel-bigger-peak-lemma to simplify the goals
+;;; ············································································
+
+;;; The two unresolved goals, as stated at the end of 3.2.3, can be
+;;; simplified to t by using the previously proved
+;;; valley-rel-bigger-peak-lemma.  This is lemma can be used for two
+;;; purposes:
+
+;;; 1: Using multiset-diff-member (see multiset.lisp) and the
+;;; following lemma (stating that the peak-element is not a member of
+;;; the proof-meassure of the transformed proof),
+;;; the calls to multiset-diff in the goals now disappear.
+;;; ···································································
+
+(local
+ (encapsulate
+  ()
+  (local
+   (defthm rel-bigger-than-list-not-member
+     (implies (rel-bigger-than-list x l)
+              (not (member x l)))))
+
+  (defthm peak-element-not-member-proof-measure
+    (implies (exists-local-peak p)
+             (not (member (peak-element p)
+                          (proof-measure (transform-local-peak
+                                          (local-peak p)))))))))
+
+;;; We are dealing with the cdr of the proof-measure:
+
+(local
+ (defthm not-member-cdr
+   (implies (not (member x l))
+	    (not (member x (cdr l))))))
+
+;;; In this moment the only unresolved goal is:
+
+;;; Subgoal 1.2
+;;; (IMPLIES (AND (EXISTS-LOCAL-PEAK P)
+;;;               (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))
+;;;          (FORALL-EXISTS-REL-BIGGER
+;;;               (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))
+;;;               (LIST (PEAK-ELEMENT P)))).
+
+
+;;; 2: Using the following lemma, the call to forall-exists-rel-bigger
+;;; in the unresolved goal above, is reduced to a call to
+;;; rel-bigger-than-list (and then valley-rel-bigger-peak-lemma will be
+;;; applied)
+;;; ···································································
+
+
+(local
+ (defthm rel-bigger-than-list-forall-exists-rel-bigger
+   (equal (forall-exists-rel-bigger l (list x))
+          (rel-bigger-than-list x l))))
+
+;;; We are dealing with the cdr of the proof-measure:
+(local
+ (defthm rel-bigger-than-list-cdr
+   (implies (rel-bigger-than-list x l)
+            (rel-bigger-than-list x (cdr l)))))
+
+;;; With this two rules altogether with valley-rel-bigger-peak-lemma our
+;;; unresolved goal becomes T, so we have:
+
+;;; ············································································
+;;; 3.2.6  The main lemma of this book
+;;; ············································································
+
+(defthm transform-to-valley-admission
+  (implies (exists-local-peak p)
+	   (mul-rel (proof-measure (replace-local-peak p))
+		    (proof-measure p)))
+  :rule-classes nil)
+
+
+
+;;; ----------------------------------------------------------------------------
+;;; 3.3 The definition of transform-to-valley
+;;; ----------------------------------------------------------------------------
+
+(defun transform-to-valley (p)
+  (declare (xargs :measure (proof-measure p)
+                  :well-founded-relation mul-rel
+                  :hints (("Goal" :use
+                           (:instance transform-to-valley-admission)))))
+
+  (if (not (exists-local-peak p))
+      p
+    (transform-to-valley (replace-local-peak p))))
+
+
+
+;;; ============================================================================
+;;; 4. Properties of transform-to-valley (Newman's lemma)
+;;; ============================================================================
+
+;;; ----------------------------------------------------------------------------
+;;; 4.1 Some previous events
+;;; ----------------------------------------------------------------------------
+
+;;; ·············································································
+;;; 4.1.1 Previous rules needed to show that (transform-to-valley p) is eqv. to p
+;;; ·············································································
+
+
+;;; We have to see that (replace-local-peak p) is equivalent to p
+;;; ··································································
+
+;;; An useful rule to deal with concatenation of proofs
+(local
+ (defthm proof-append
+   (implies (equal z (last-of-proof x p1))
+	    (equal (equiv-p x y (append p1 p2))
+		   (and (equiv-p x z p1)
+			(equiv-p z y p2))))))
+
+;;; Last element of a local peak
+(local
+ (defthm last-element-of-a-local-peak
+   (implies (local-peak-p p)
+            (equal (last-elt p) (cadr p)))))
+
+;;; The case where (transform-local-peak (local-peak p)) is empty:
+
+(local
+ (defthm atom-proof-endpoints-are-equal
+   (implies (and (equiv-p x y p) (atom p))
+            (equal x y))
+   :rule-classes nil))
+
+(local
+ (defthm atom-transform-local-peak-forward-chaining-rule
+   (implies (and
+             (not (consp (transform-local-peak (local-peak p))))
+             (exists-local-peak p)
+             (equiv-p x y (local-peak p)))
+            (equal x y))
+   :hints (("Goal" :use ((:instance atom-proof-endpoints-are-equal
+                                    (p (transform-local-peak (local-peak p)))))))
+   :rule-classes :forward-chaining))
+
+;;; REMARK: interesting use of forward-chaining.
+
+;;; In the following bridge lemma it is fundamental
+;;; replace-local-peak-another-definition and the case distinction
+;;; generated by proof-append:
+
+(local
+ (defthm equiv-p-x-y-replace-local-peak-bridge-lemma
+   (implies (and (exists-local-peak p)
+                 (equiv-p x y (append
+                               (proof-before-peak p)
+                               (append (local-peak p)
+                                       (proof-after-peak p)))))
+            (equiv-p x y (replace-local-peak p)))))
+
+(local (in-theory (disable replace-local-peak-another-definition)))
+
+;;; And finally the intended lemma:
+
+(local
+ (defthm equiv-p-x-y-replace-local-peak
+   (implies (and (equiv-p x y p) (exists-local-peak p))
+            (equiv-p x y (replace-local-peak p)))
+   :hints (("Goal" :in-theory (enable proof-peak-append)))))
+
+;;; REMARK: It's interesting how we avoid explicit expansion of the
+;;; three pieces of p (before, at and after the peak), using the
+;;; previous bridge lemma.
+
+;;; ·············································································
+;;; 4.1.2 A rule needed to show that (transform-to-valley p) is a valley
+;;; ·············································································
+
+
+
+;;; If a proof does not have local peaks, then it is a valley:
+
+(local
+ (defthm steps-valley-not-exists-local-peak
+   (implies (equiv-p x y p)
+            (equal  (steps-valley p) (not (exists-local-peak p))))))
+
+
+;;; ·············································································
+;;; 4.1.3 Disabling the induction rule for equiv-p
+;;; ·············································································
+
+
+(local (in-theory (disable equiv-p-induct)))
+
+;;; REMARK: It is important to disable the induction rule of equiv-p
+;;; because we want the two main properties of transform-to-valley
+;;; to be proved by the induction suggested by transform-to-valley
+;;; (i.e. and induction based on the multiset relation mul-rel)
+
+
+;;; ----------------------------------------------------------------------------
+;;; 4.2 The intended properties of transform-to-valley
+;;; ----------------------------------------------------------------------------
+
+
+;;; It returns an equivalent proof
+;;; ······························
+
+
+(defthm equiv-p-x-y-transform-to-valley
+  (implies (equiv-p x y p)
+           (equiv-p x y (transform-to-valley p))))
+
+
+
+
+;;; It returns a valley proof
+;;; ·························
+
+
+(defthm valley-transform-to-valley
+   (implies (equiv-p x y p)
+            (steps-valley (transform-to-valley p))))
+
+
+;;; CONCLUSION:
+;;; The definition of transform-to-valley and the theorems
+;;; equiv-p-x-y-transform-to-valley and valley-transform-to-valley prove
+;;; the Newman's lemma