Import acl2_7.4dfsg.orig.tar.gz

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

1 files changed, 1320 insertions, 0 deletions

diff --git a/books/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Equiv-From-M-Corr.lisp b/books/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Equiv-From-M-Corr.lisp
new file mode 100644
index 0000000..bb06f01
--- /dev/null
+++ b/books/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Equiv-From-M-Corr.lisp
@@ -0,0 +1,1320 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;; Section 4: Definition of m-correspondence
+;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;
+;;;
+;;; Definition of mapping-induced correspondence:
+;;;
+;;; In order for a Gem memory and and Rtm memory to be m-correspondent via m,
+;;; the following conditions must hold:
+;;;
+;;; - Correctness w.r.t. the types of the variables appearing into the memories:
+;;;   I.e., m must map boolean Gem variables into single Rtm variables, and integer Gem
+;;;   variables into tuples of |*rns*| Rtm variables;
+;;;
+;;; - Correctness w.r.t. the values and attributes of the variables appearing into the memories:
+;;;   for each entry of the mapping,
+;;;   the values obtained by direct application of rns to the gem variable of the entry must
+;;;   match those of the rtm variables, and
+;;;   the attributes of the rtm variables must match that of the rtm variable.
+;;;
+;;; - A mapping must have every Gem variable within the range of the Gem memory it references
+;;;
+;;; - A mapping must contain every variable of the Gem memory it references
+;;;
+;;;
+;;; Similar properties to the least two will be needed for the Rtm memories (e.g., every Rtm
+;;; variable should be in the range of the Rtm memory), when proving properties about
+;;; programs. We will insert them then.
+;;;
+
+
+
+(in-package "ACL2")
+
+(include-book "CRTcorollaries")
+
+(in-theory (current-theory 'ground-zero))
+
+(include-book "Mapping")
+
+
+;;;
+;;; Subsection 4.1:
+;;;
+;;; Memories must be correspondent via m in terms of types
+;;;
+
+
+
+(defun correct-wrt-arity (m gem-typed-mem)
+  (if (endp m)
+      (null m)
+    (and
+     (correct-type (type-0 m))
+     (equal
+      (type-0 m)
+      (var-type (get-cell (gemvar-0 m) gem-typed-mem)))
+     (correct-wrt-arity (cdr m) gem-typed-mem))))
+
+(defthm correct-arity-all-i-need
+ (implies
+  (and
+   (not (endp m))
+   (correct-wrt-arity m gem-typed-mem))
+  (and
+   (correct-type (type-0 m))
+   (equal
+    (type-0 m)
+    (var-type (get-cell (gemvar-0 m) gem-typed-mem)))
+   (not (null (var-attributes (rtmintvars-0 m) rtm-typed-mem)))
+   (correct-wrt-arity (cdr m) gem-typed-mem))))
+
+
+
+;;
+;; Section 4.5:
+;;
+;; Every entry of the mapping must point to a coherent set of rtm variables, i.e. to a set of of rtm
+;; variables which share the same attribute.
+;;
+
+(defun get-common-value (l)
+  (if (equal-elements (car l) (cdr l))
+      (car l)
+    'error-value))
+
+(defthm if-every-element-matches-val-then-get-common-value-amounts-to-val
+ (implies
+  (and
+   (true-listp l)
+   (not (null l))
+   (equal-elements v l))
+  (equal (get-common-value l) v)))
+
+(in-theory (disable if-every-element-matches-val-then-get-common-value-amounts-to-val))
+
+
+(defun m-entries-point-to-good-rtm-var-sets (m rtm-typed-mem)
+  (if (endp m)
+      (null m)
+    (and
+     (not (endp (rtmintvars-0 m)))
+     (true-listp (rtmintvars-0 m))
+     (not (equal 'error-value (get-common-value (var-attributes (rtmintvars-0 m) rtm-typed-mem))))
+     (m-entries-point-to-good-rtm-var-sets (cdr m) rtm-typed-mem))))
+
+(in-theory (disable m-entries-point-to-good-rtm-var-sets))
+
+
+
+;;;
+;;; Subsection 4.6:
+;;;
+;;; Values and attributes must be correspondent via the mapping.
+;;;
+;;; In order to allow this definition, we first provide
+;;; definitions of transformations of gem values into tuples of rtm values (by *rns*) and
+;;; viceversa (by inverse application of *rns*).
+;;;
+;;; Notice that these transformations are actually just ``stubs'', since we provide a
+;;; simplified form of axiomatization of the chinese remainder inversion theorem.
+;;; Additional hypothesis (e.g., boundedness of Gem and Rtm integers, and relations between such
+;;; bounds) shall (and will) be added and taken into account when proving properties of programs.
+;;; In the cureent state of the proof, however, we can limit ourselves to consider 'generic'
+;;; transformations of Gem vars into tuples of Rtm vars, and their corresponding generic inverse.
+;;;
+;;; However, since memories could contain nil cells, we have to lift our transformations, and
+;;; the 'simplified axiomatization of CRT', to deal with nils.
+;;;
+;;; We extend transformations so that nils transform into sequences of nils and viceversa.
+;;; We lift the simplified CRT axiomatization to such extended version.
+;;;
+;;;
+
+
+
+
+(defun make-null-list (l)
+ (if (endp l)
+     nil
+     (cons nil (make-null-list (cdr l)))))
+
+(defthm make-null-list-is-invariant-on-value-slicing (equal (make-null-list rtmvars) (make-null-list (var-values rtmvars rm))))
+
+(in-theory (disable make-null-list-is-invariant-on-value-slicing))
+
+(defun equal-values (val-list-1 val-list-2)
+ (equal val-list-1 val-list-2))
+
+(defun build-values-by-rns (gem-value rns)
+ (if (endp rns)
+     nil
+     (cons (mod gem-value (car rns))
+           (build-values-by-rns gem-value (cdr rns)))))
+
+(in-theory (enable build-values-by-rns))
+
+(defun mod-extended-for-nil (val1 val2)
+ (if (null val1)
+     nil
+     (mod val1 val2)))
+
+(defun build-values-by-rns-extended-for-nil (gem-value rns)
+ (if (endp rns)
+     nil
+     (cons (mod-extended-for-nil gem-value (car rns))
+           (build-values-by-rns-extended-for-nil gem-value (cdr rns)))))
+
+(defthm build-values-by-rns-extended-behaves-standardly-on-non-nils
+ (implies
+  (not (null gem-value))
+  (equal
+    (build-values-by-rns-extended-for-nil gem-value rns)
+    (build-values-by-rns gem-value rns))))
+
+(defthm build-values-by-rns-extended-for-nils-provides-integers-from-integer
+ (implies
+  (and
+   (integerp val)
+   (not (null rns))
+   (integer-listp rns))
+  (and
+   (not (null (build-values-by-rns-extended-for-nil val rns)))
+   (integer-listp (build-values-by-rns-extended-for-nil val rns)))))
+
+
+
+
+(defun build-value-by-inverse-rns (rtm-values rns)
+ (crtmod rtm-values rns))
+
+
+(defun build-value-by-inverse-rns-extended-for-nil (rtm-values rns)
+ (if
+     (integer-listp rtm-values)
+     (crtmod rtm-values rns)
+   nil))
+
+
+(defthm build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists
+ (implies
+  (integer-listp rtm-values)
+  (equal
+    (build-value-by-inverse-rns-extended-for-nil rtm-values rns)
+    (build-value-by-inverse-rns rtm-values rns))))
+
+
+
+
+(defthm crt-inversion-inst
+ (implies
+  (and
+   (rel-prime-moduli rns)
+   (natp gem-value)
+   (< gem-value (prod rns)))
+ (equal
+  (build-value-by-inverse-rns (build-values-by-rns gem-value rns) rns)
+  gem-value))
+ :hints (("Goal" :in-theory (enable crt-inversion))))
+
+
+(in-theory (enable natp))
+
+
+(defthm crt-inversion-extended-to-nils-in-integer-case
+ (implies
+  (and
+   (rel-prime-moduli rns)
+   (< gem-value (prod rns))
+   (not (null rns))
+   (integer-listp rns)
+   (natp gem-value))
+ (equal
+  (build-value-by-inverse-rns-extended-for-nil (build-values-by-rns-extended-for-nil gem-value rns) rns)
+  gem-value))
+ :hints (("goal"
+          :use (
+                crt-inversion-inst
+                build-values-by-rns-extended-behaves-standardly-on-non-nils
+                (:instance build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists
+			   (rtm-values (build-values-by-rns gem-value rns)))
+                (:instance build-values-by-rns-extended-for-nils-provides-integers-from-integer
+			   (val gem-value))))))
+
+(defthm crt-inversion-extended-to-nils-in-nil-case
+ (implies
+  (and
+   (rel-prime-moduli rns)
+   (not (null rns))
+   (integer-listp rns)
+   (null gem-value))
+ (equal
+  (build-value-by-inverse-rns-extended-for-nil (build-values-by-rns-extended-for-nil gem-value rns) rns)
+  gem-value)))
+
+(defthm crt-inversion-extended-to-nils
+ (implies
+  (and
+   (rel-prime-moduli rns)
+   (integer-listp rns)
+   (not (null rns))
+  (or
+   (null gem-value)
+   (and
+    (natp gem-value)
+    (< gem-value (prod rns)))))
+ (equal
+  (build-value-by-inverse-rns-extended-for-nil (build-values-by-rns-extended-for-nil gem-value rns) rns)
+  gem-value))
+ :hints (("goal"
+          :cases (
+                  (and (not (null gem-value)) (not (and (natp gem-value) (< gem-value (prod rns)))))
+                  (null gem-value)
+                  (and (natp gem-value) (< gem-value (prod rns)))))
+	 ("Subgoal 2" :use crt-inversion-extended-to-nils-in-nil-case)
+         ("subgoal 1" :use (:instance crt-inversion-extended-to-nils-in-integer-case))))
+
+
+(in-theory (disable build-values-by-rns-extended-for-nil
+                    build-values-by-rns
+                    build-value-by-inverse-rns-extended-for-nil
+                    build-value-by-inverse-rns
+                    build-values-by-rns-extended-behaves-standardly-on-non-nils
+                    build-values-by-rns-extended-for-nils-provides-integers-from-integer
+                    build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists
+                    crt-inversion-extended-to-nils-in-integer-case
+		    crt-inversion-extended-to-nils-in-nil-case))
+
+
+
+
+
+
+
+;;
+;; m-correspondence definition w.r.t. values and attributes of memories
+;;
+
+
+
+
+(defun apply-direct-rns-to-value-according-to-type (gem-cell type)
+ (cond
+  ( (equal type 'bool)
+    (list (var-value gem-cell)))
+  ( (equal type 'int)
+    (build-values-by-rns-extended-for-nil (var-value gem-cell) *rns*))
+  ( t nil)))
+
+
+
+(defun apply-invers-rns-to-values-according-to-type (vals type)
+ (cond
+  ( (equal type 'bool)
+    (car vals) )
+  ( (equal type 'int)
+    (build-value-by-inverse-rns-extended-for-nil vals *rns*))
+  ( t nil )))
+
+
+
+
+(defun invert-cell (rtmvars rtm-typed-mem type)
+  (if
+     (equal-values
+       (var-values     rtmvars rtm-typed-mem)
+       (make-null-list rtmvars))
+      (apply-invers-rns-to-values-according-to-type
+       (var-values rtmvars rtm-typed-mem)
+       type)
+    (make-cell
+     (apply-invers-rns-to-values-according-to-type
+      (var-values rtmvars rtm-typed-mem)
+      type)
+     (get-common-value (var-attributes rtmvars rtm-typed-mem))
+     type)))
+
+(defun equal-values-and-attributes (gem-cell rtmvars rtm-typed-mem type)
+(and
+ (equal-values
+  (var-values rtmvars rtm-typed-mem)
+  (apply-direct-rns-to-value-according-to-type gem-cell type))
+ (equal-elements
+  (var-attribute gem-cell)
+  (var-attributes rtmvars rtm-typed-mem))))
+
+
+
+(defthm apply-direct-rns-unfolding-for-integer-case
+ (implies
+  (equal type 'int)
+  (equal
+   (apply-direct-rns-to-value-according-to-type gem-cell type)
+   (build-values-by-rns-extended-for-nil (var-value gem-cell) *rns*))))
+
+(defthm apply-direct-rns-unfolding-for-boolean-case
+ (implies
+  (equal type 'bool)
+  (equal
+   (apply-direct-rns-to-value-according-to-type gem-cell type)
+   (list (var-value gem-cell)))))
+
+
+
+(defthm apply-inverse-rns-unfolding-for-integer-case
+ (implies
+  (equal type 'int)
+  (equal (apply-invers-rns-to-values-according-to-type values type)
+	 (build-value-by-inverse-rns-extended-for-nil values *rns*))))
+
+
+(defthm apply-inverse-direct-retrieves-same-value-for-typed-cells
+ (implies
+  (and
+  (rel-prime-moduli *rns*)
+  (integer-listp *rns*)
+  (not (null *rns*))
+   (or
+    (equal type 'int)
+    (equal type 'bool))
+   (or
+    (and
+     (natp (var-value gem-cell))
+     (< (var-value gem-cell) (prod *rns*)))
+    (null (var-value gem-cell))))
+  (equal
+   (apply-invers-rns-to-values-according-to-type
+    (apply-direct-rns-to-value-according-to-type gem-cell type) type)
+   (var-value gem-cell)))
+ :hints (("goal" :cases ( (equal type 'bool)
+                          (equal type 'int)))
+         ("subgoal 1"
+          :in-theory (disable null
+                              apply-inverse-rns-unfolding-for-integer-case
+                              crt-inversion-extended-to-nils
+                              apply-direct-rns-unfolding-for-integer-case
+                              apply-direct-rns-to-value-according-to-type
+                              var-value
+                              apply-invers-rns-to-values-according-to-type
+                              build-value-by-inverse-rns-extended-for-nil
+                              build-values-by-rns-extended-for-nil)
+          :use ((:instance apply-direct-rns-unfolding-for-integer-case)
+                (:instance apply-inverse-rns-unfolding-for-integer-case (values (build-values-by-rns-extended-for-nil (var-value gem-cell) *rns*)))
+                (:instance crt-inversion-extended-to-nils (rns *rns*) (gem-value (var-value gem-cell)))))))
+
+
+
+
+(defthm inversion-for-empty-cell
+ (implies
+  (and
+   (null cell)
+   (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
+   (correct-type type))
+  (and
+   (equal-values (var-values rtmvars rm) (make-null-list rtmvars))
+   (equal (apply-invers-rns-to-values-according-to-type (var-values rtmvars rm) type) cell)))
+ :hints (("goal"
+	  :in-theory (enable make-null-list-is-invariant-on-value-slicing)
+	  :cases ( (equal type 'bool) (equal type 'int)))))
+
+
+(in-theory (disable  make-cell))
+
+
+(defthm ad-hoc-2-for-inversion-of-one-nonempty-cell-by-decode
+  (implies
+   (and (not (null bui)) (integer-listp bui))
+   (not (equal (make-null-list l) bui))))
+
+
+(defthm ad-hoc-3-for-inversion-of-one-nonempty-cell-by-decode
+  (implies
+   (integerp (var-value cell))
+   (not (equal (make-null-list l) (build-values-by-rns-extended-for-nil (var-value cell) *rns*))))
+  :hints (("goal" :use ((:instance build-values-by-rns-extended-for-nils-provides-integers-from-integer
+				   (val (var-value cell)) (rns *rns*))
+			(:instance ad-hoc-2-for-inversion-of-one-nonempty-cell-by-decode
+				   (l l)
+				   (bui (build-values-by-rns-extended-for-nil (var-value cell) *rns*)))))))
+
+(defthm nonempty-cell-is-not-mapped-into-nils-by-rns
+  (implies
+   (and
+    (true-listp (var-attributes rtmvars rm))
+    (not (null (var-attributes rtmvars rm)))
+    (is-mem-cell-p cell)
+    (not (null cell))
+    (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
+    (equal-elements (var-attribute cell) (var-attributes rtmvars rm))
+    (equal type (var-type cell)))
+    (not (equal-values (var-values rtmvars rm) (make-null-list rtmvars))))
+ :hints (("goal" :cases ( (equal type 'bool) (equal type 'int)))))
+
+
+
+(in-theory (disable my-or-2 my-or-3))
+
+(defthm silly00
+  (IMPLIES (AND (TRUE-LISTP CELL6)
+		(EQUAL (+ 3 (LEN CELL6)) 3))
+	   (NOT CELL6))
+  :rule-classes nil)
+
+(defthm reconstruction-of-cell
+ (implies
+  (is-mem-cell-p cell)
+  (equal
+   (make-cell
+    (var-value cell)
+    (var-attribute cell)
+    (var-type cell))
+   cell))
+  :hints (("Subgoal 1.1" :use silly00)
+	  ("Subgoal 2.1" :use silly00)
+	  ("goal"
+	   :in-theory
+	   (union-theories (current-theory 'ground-zero)
+	   '((:definition is-mem-cell-p)
+	     (:definition make-cell)
+	     (:definition var-type)
+	     (:definition var-value)
+	     (:definition var-attribute)))))
+  :rule-classes nil)
+
+
+
+(defthm nonempty-rtm-vars-which-correspond-to-gem-var-by-values-and-atributes-map-back-to-gem-var
+  (implies
+   (and
+    (rel-prime-moduli *rns*)
+    (integer-listp *rns*)
+    (not (null *rns*))
+    (true-listp (var-attributes rtmvars rm))
+    (not (null (var-attributes rtmvars rm)))
+    (is-mem-cell-p cell)
+    (not (null cell))
+    (natp (var-value cell))
+    (< (var-value cell) (prod *rns*))
+    (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
+    (equal-elements (var-attribute cell) (var-attributes rtmvars rm))
+    (equal type (var-type cell)))
+    (equal
+     (make-cell
+      (apply-invers-rns-to-values-according-to-type (var-values rtmvars rm) type)
+      (get-common-value (var-attributes rtmvars rm))
+      type)
+     cell))
+  :hints (("goal" :in-theory '((:definition my-or-2)
+			       (:definition is-mem-cell-p)
+			       (:definition natp)
+			       (:definition equal-values)
+			       (:definition is-mem-cell-p))
+	          :use (reconstruction-of-cell
+			(:instance if-every-element-matches-val-then-get-common-value-amounts-to-val
+				  (l (var-attributes rtmvars rm)) (v (var-attribute cell)))
+			(:instance apply-inverse-direct-retrieves-same-value-for-typed-cells
+				   (type type) (gem-cell cell))))))
+
+
+
+
+
+
+
+
+
+
+(defthm decode-inversion-for-nonempty-gem-cell
+  (implies
+   (and
+    (rel-prime-moduli *rns*)
+    (integer-listp *rns*)
+    (not (null *rns*))
+    (true-listp (var-attributes rtmvars rm))
+    (not (null (var-attributes rtmvars rm)))
+    (is-mem-cell-p cell)
+    (not (null cell))
+    (natp (var-value cell))
+    (< (var-value cell) (prod *rns*))
+    (equal-values (var-values rtmvars rm) (apply-direct-rns-to-value-according-to-type cell type))
+    (equal-elements (var-attribute cell) (var-attributes rtmvars rm))
+    (equal type (var-type cell)))
+   (and
+    (not (equal-values (var-values rtmvars rm) (make-null-list rtmvars)))
+    (equal
+     (make-cell
+      (apply-invers-rns-to-values-according-to-type (var-values rtmvars rm) type)
+      (get-common-value (var-attributes rtmvars rm))
+      type)
+     cell)))
+  :hints (("goal" :use (nonempty-cell-is-not-mapped-into-nils-by-rns
+			nonempty-rtm-vars-which-correspond-to-gem-var-by-values-and-atributes-map-back-to-gem-var))))
+
+
+
+
+
+
+(defthm var-attributes-always-true-listp
+ (true-listp (var-attributes rtmvars rtm-typed-mem)))
+
+(defun bounded-value (cell)
+  (if (null cell)
+      t
+    (and (natp (var-value cell)) (< (var-value cell) (prod *rns*)))))
+
+(defthm invert-cell-inverts-for-m-correspondents
+ (implies
+  (and
+   (rel-prime-moduli *rns*)
+   (integer-listp *rns*)
+   (not (null *rns*))
+   (not (null (var-attributes rtmvars rtm-typed-mem)))
+   (equal type (var-type gem-cell))
+   (correct-type type)
+   (or (null gem-cell) (is-mem-cell-p gem-cell))
+   (bounded-value gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+  (equal
+   (invert-cell rtmvars rtm-typed-mem type)
+   gem-cell))
+ :hints (("Goal"
+	  :in-theory (disable equal-values)
+	  :use ( var-attributes-always-true-listp
+		 (:instance decode-inversion-for-nonempty-gem-cell
+			    (cell gem-cell)
+			    (rm rtm-typed-mem))
+		 (:instance inversion-for-empty-cell
+			    (cell gem-cell)
+			    (rm rtm-typed-mem))))))
+
+
+(defun is-typed-amem-p (mem)
+  (if (endp mem)
+      (null mem)
+    (and
+     (consp (car mem))
+     (is-mem-cell-p (cdr (car mem)))
+     (is-typed-amem-p (cdr mem)))))
+
+(in-theory (enable get-cell))
+
+(defthm any-cell-of-a-typed-mem-is-nil-or-a-typed-cell
+ (implies
+  (is-typed-amem-p gem-typed-mem)
+  (or
+   (and
+    (null (assoc-equal v gem-typed-mem))
+    (null (get-cell v gem-typed-mem)))
+   (is-mem-cell-p (get-cell v gem-typed-mem))))
+ :rule-classes nil)
+
+
+
+
+
+
+
+
+(defun m-correspondent-values-p (m gem-typed-mem rtm-typed-mem)
+ (cond
+  ( (endp m)
+    (null m) )
+  ( t
+    (and
+     (equal-values-and-attributes
+      (get-cell (gemvar-0 m) gem-typed-mem)
+      (rtmintvars-0 m)
+      rtm-typed-mem (type-0 m))
+     (m-correspondent-values-p (cdr m)  gem-typed-mem rtm-typed-mem)))))
+
+(defun decode (m rtm-typed-mem)
+ (if
+  (endp m)
+    nil
+    (put-cell
+     (gemvar-0 m)
+     (invert-cell (rtmintvars-0 m) rtm-typed-mem (type-0 m))
+     (decode (cdr m) rtm-typed-mem))))
+
+
+(defthm silly1
+     (equal (caar m) (gemvar-0 m)))
+
+(in-theory (disable silly1))
+
+(defthm silly2
+  (implies
+   (correct-wrt-arity m gem-typed-mem)
+   (correct-wrt-arity (cdr m) gem-typed-mem)))
+
+(in-theory (disable silly1 silly2))
+
+(defun bounded-amem-p (mem)
+  (if
+      (endp mem)
+      (null mem)
+    (and (bounded-value (cdr (car mem)))
+	 (bounded-amem-p (cdr mem)))))
+
+(defthm any-cell-of-bounded-mem-is-bounded
+ (implies
+  (bounded-amem-p gem-typed-mem)
+  (bounded-value (get-cell v gem-typed-mem)))
+ :rule-classes nil)
+
+(defthm decode-equals-retrieve-vars
+ (implies
+  (and
+   (rel-prime-moduli *rns*)
+   (integer-listp *rns*)
+   (not (null *rns*))
+   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem)
+   (is-typed-amem-p gem-typed-mem)
+   (bounded-amem-p gem-typed-mem)
+   (correct-wrt-arity m gem-typed-mem))
+  (equal
+   (decode m rtm-typed-mem)
+   (retrieve-vars m gem-typed-mem)))
+ :hints (("Goal" :induct (len m))
+	 ("Subgoal *1/1"
+	  :in-theory nil
+	  :use (silly1
+		silly2
+		decode
+		(:instance retrieve-vars (vars m) (mem gem-typed-mem))
+		m-correspondent-values-p
+		(:instance any-cell-of-a-typed-mem-is-nil-or-a-typed-cell (v (gemvar-0 m)))
+		(:instance any-cell-of-bounded-mem-is-bounded (v (gemvar-0 m)))
+		correct-arity-all-i-need
+		(:instance invert-cell-inverts-for-m-correspondents
+			   (rtmvars (rtmintvars-0 m))
+			   (gem-cell (get-cell (gemvar-0 m) gem-typed-mem))
+			   (type (type-0 m)))))))
+
+
+(defthm decode-retrieves-gem-memory
+ (implies
+  (and
+   (rel-prime-moduli *rns*)
+   (integer-listp *rns*)
+   (not (null *rns*))
+   (vars-inclusion gem-typed-mem m)
+   (vars-inclusion m gem-typed-mem)
+   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem)
+   (is-typed-amem-p gem-typed-mem)
+   (bounded-amem-p gem-typed-mem)
+   (correct-wrt-arity m gem-typed-mem))
+  (equal-memories (decode m rtm-typed-mem) gem-typed-mem))
+ :hints (("Goal" :in-theory (enable retrieving-keeps-equality))))
+
+
+(defun projectiocell (cell attr)
+ (if (null cell)
+     cell
+     (if (equal (var-attribute cell) attr)
+	 cell
+         nil )))
+
+(defun projectio (mem attr)
+  (if (endp mem)
+      nil
+      (put-cell (caar mem)
+		(projectiocell (cdr (car mem))  attr)
+		(projectio (cdr mem) attr))))
+
+
+
+(defthm cell-of-projected-mem-is-projected-cell
+ (equal
+  (get-cell cell (projectio mem attr))
+  (projectiocell (get-cell cell mem) attr)))
+
+
+
+
+(defthm projection-of-null-list-is-null-list
+ (implies
+   (equal-values (var-values l rtm-typed-mem) (make-null-list l))
+   (equal-values (var-values l (projectio rtm-typed-mem attr)) (make-null-list l))))
+
+
+(defthm null-cell-corresponds-to-null-lists-of-values
+ (implies
+  (and
+   (null gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+  (equal-values (var-values rtmvars rtm-typed-mem) (make-null-list rtmvars)))
+ :hints (("Goal" :in-theory (disable get-cell var-value var-attribute ))))
+
+
+
+(defthm project-invert-commute-for-empty-cell
+ (implies
+  (and
+   (null gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
+	(invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
+ :hints (("Goal" :use (null-cell-corresponds-to-null-lists-of-values
+		       (:instance projection-of-null-list-is-null-list (l rtmvars))))))
+
+
+
+(defthm rtmvars-correspondent-to-nonemptycell-is-not-emptylist
+ (implies
+  (and
+   (not (null (var-attributes rtmvars rtm-typed-mem)))
+   (equal type (var-type gem-cell))
+   (correct-type type)
+   (not (null gem-cell))
+   (equal (var-attribute gem-cell) attr)
+   (is-mem-cell-p gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+  (not
+   (equal-values
+    (var-values rtmvars rtm-typed-mem)
+    (make-null-list rtmvars)))))
+
+
+
+
+(defthm values-remain-the-same-if-correspondent-attrs
+ (implies
+  (and
+   (not (null (var-attributes rtmvars rtm-typed-mem)))
+   (equal type (var-type gem-cell))
+   (correct-type type)
+   (not (null gem-cell))
+   (equal (var-attribute gem-cell) attr)
+   (is-mem-cell-p gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal
+  (var-values rtmvars (projectio rtm-typed-mem attr))
+  (var-values rtmvars rtm-typed-mem)))
+ :hints (("Goal" :do-not '(generalize))))
+
+
+
+(defthm attributes-same-1
+ (implies
+  (equal-elements attr (var-attributes rtmvars rtm-typed-mem))
+     (equal
+      (var-attributes rtmvars (projectio rtm-typed-mem attr))
+      (var-attributes rtmvars rtm-typed-mem))))
+
+
+
+
+(defthm inversion-2-for-nonempty-projected-on-same-attr
+ (implies
+  (and
+   (not (null (var-attributes rtmvars rtm-typed-mem)))
+   (equal type (var-type gem-cell))
+   (correct-type type)
+   (not (null gem-cell))
+   (equal (var-attribute gem-cell) attr)
+   (is-mem-cell-p gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal (invert-cell rtmvars (projectio rtm-typed-mem attr) type)
+	(invert-cell rtmvars rtm-typed-mem type)))
+ :hints (("Goal" :in-theory nil
+          ;; modified for Version  2.7 fertilization
+	  :use (
+                (:instance invert-cell (rtm-typed-mem (projectio rtm-typed-mem attr)))
+                invert-cell
+                equal-values-and-attributes
+                (:instance attributes-same-1 (attr (var-attribute gem-cell)))
+                rtmvars-correspondent-to-nonemptycell-is-not-emptylist
+                values-remain-the-same-if-correspondent-attrs)
+          :expand ((:free (x) (hide x))))))
+
+
+(defthm inversion-1-for-nonempty-projected-on-different-attr
+ (implies
+  (and
+   (not (null (var-attributes rtmvars rtm-typed-mem)))
+   (equal type (var-type gem-cell))
+   (correct-type type)
+   (not (null gem-cell))
+   (not (equal (var-attribute gem-cell) attr))
+   (is-mem-cell-p gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
+	nil)))
+
+
+(defthm projecting-on-different-attr-gets-nils
+ (implies
+  (and
+   (not (equal (var-attribute gem-cell) attr))
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+  (equal-values
+   (var-values rtmvars (projectio rtm-typed-mem attr))
+   (make-null-list rtmvars))))
+
+
+
+(defthm decode-one-entry-of-null-list-is-nil
+(implies
+ (and
+  (true-listp l)
+  (not (endp l))
+  (equal-values (var-values l rtm-typed-mem) (make-null-list l)))
+ (equal (apply-invers-rns-to-values-according-to-type (var-values l rtm-typed-mem) ty) nil))
+ :hints(("goal" :in-theory (enable build-value-by-inverse-rns-extended-for-nil))))
+
+
+(defthm inversion-2-for-nonempty-projected-on-different-attr
+ (implies
+  (and
+   (true-listp rtmvars)
+   (not (null rtmvars))
+   (not (equal (var-attribute gem-cell) attr))
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal (invert-cell rtmvars (projectio rtm-typed-mem attr) type)
+	nil))
+ :hints (("Goal" :use
+	  ((:instance decode-one-entry-of-null-list-is-nil
+		      (l rtmvars)
+		      (rtm-typed-mem  (projectio rtm-typed-mem attr))
+		      (ty type))
+	   (:instance invert-cell (rtm-typed-mem (projectio rtm-typed-mem attr)))
+	   projecting-on-different-attr-gets-nils))))
+
+
+
+
+(defthm inversion-for-nonempty-projected-on-different-attr
+ (implies
+  (and
+   (true-listp rtmvars)
+   (not (null rtmvars))
+   (not (null (var-attributes rtmvars rtm-typed-mem)))
+   (equal type (var-type gem-cell))
+   (correct-type type)
+   (not (null gem-cell))
+   (not (equal (var-attribute gem-cell) attr))
+   (is-mem-cell-p gem-cell)
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
+	(invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
+ :hints (("Goal"
+	  :in-theory nil
+	  :use
+	  (inversion-1-for-nonempty-projected-on-different-attr
+	   inversion-2-for-nonempty-projected-on-different-attr))))
+
+
+
+
+
+(defthm project-invert-commuting
+ (implies
+  (and
+   (true-listp rtmvars)
+   (not (null rtmvars))
+   (not (null (var-attributes rtmvars rtm-typed-mem)))
+   (or
+    (null gem-cell)
+    (equal type (var-type gem-cell)))
+   (correct-type type)
+   (or (null gem-cell) (is-mem-cell-p gem-cell))
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
+	(invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
+ :hints (("Goal" :cases
+	  ( (and (not (null gem-cell)) (not (equal (var-attribute gem-cell) attr)))
+	    (and (not (null gem-cell)) (equal (var-attribute gem-cell) attr))))
+	 ("Subgoal 3" :use project-invert-commute-for-empty-cell)
+	 ("Subgoal 2" :use inversion-for-nonempty-projected-on-different-attr)))
+
+(defthm letssimplify
+  (implies
+  (and
+   (true-listp rtmvars)
+   (not (null rtmvars)))
+   (not (null (var-attributes rtmvars rtm-typed-mem)))))
+
+
+(defthm project-invert-commuting-better
+ (implies
+  (and
+   (true-listp rtmvars)
+   (not (null rtmvars))
+   (or
+    (null gem-cell)
+    (equal type (var-type gem-cell)))
+   (correct-type type)
+   (or (null gem-cell) (is-mem-cell-p gem-cell))
+   (equal-values-and-attributes gem-cell rtmvars rtm-typed-mem type))
+ (equal (projectiocell (invert-cell rtmvars rtm-typed-mem type) attr)
+	(invert-cell rtmvars (projectio rtm-typed-mem attr) type)))
+ :hints (("Goal" :use (letssimplify project-invert-commuting))))
+
+
+
+(in-theory (enable
+		   m-entries-point-to-good-rtm-var-sets
+		   m-correspondent-values-p))
+
+(in-theory (disable gemvar-0 rtmintvars-0))
+
+(defthm lil-helper
+ (implies
+  (and
+   (not (endp m))
+   (is-typed-amem-p gem-typed-mem)
+   (correct-wrt-arity m gem-typed-mem)
+   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
+   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem))
+  (and
+   (or
+    (null (get-cell (gemvar-0 m) gem-typed-mem))
+    (is-mem-cell-p (get-cell (gemvar-0 m) gem-typed-mem)))
+   (true-listp (rtmintvars-0 m))
+   (not (null (rtmintvars-0 m)))
+   (correct-type (type-0 m))
+   (or
+    (null (get-cell (gemvar-0 m) gem-typed-mem))
+    (equal (type-0 m) (var-type (get-cell (gemvar-0 m) gem-typed-mem))))
+   (equal-values-and-attributes
+    (get-cell (gemvar-0 m) gem-typed-mem)
+    (rtmintvars-0 m)
+    rtm-typed-mem
+    (type-0 m))
+   (correct-wrt-arity (cdr m) gem-typed-mem)
+   (m-entries-point-to-good-rtm-var-sets (cdr m) rtm-typed-mem)
+   (m-correspondent-values-p (cdr m) gem-typed-mem rtm-typed-mem)))
+ :hints (("Goal" :use (:instance any-cell-of-a-typed-mem-is-nil-or-a-typed-cell
+				 (v (gemvar-0 m)))))
+ :rule-classes nil)
+
+
+
+(defun decode-projection (m rtm-typed-mem attr)
+  (if (endp m)
+      nil
+    (put-cell (gemvar-0 m)
+	      (projectiocell
+	       (invert-cell
+		(rtmintvars-0 m)
+	        rtm-typed-mem
+		(type-0 m))
+	       attr)
+	      (decode-projection (cdr m) rtm-typed-mem attr))))
+
+
+(in-theory (enable m-entries-point-to-good-rtm-var-sets))
+
+(defthm project-of-decode-is-decode-projection
+  (equal
+   (projectio (decode m rtm-typed-mem) attr)
+   (decode-projection m rtm-typed-mem attr)))
+
+
+(defthm decode-projection-is-decode-of-projection
+ (implies
+  (and
+   (is-typed-amem-p gem-typed-mem)
+   (correct-wrt-arity m gem-typed-mem)
+   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
+   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem))
+ (equal
+  (decode-projection  m rtm-typed-mem attr)
+  (decode m (projectio rtm-typed-mem attr))))
+ :hints (("Goal"  :induct (len m))
+	 ("Subgoal *1/1" :in-theory nil
+	  :use (lil-helper
+		(:instance decode (rtm-typed-mem  (projectio rtm-typed-mem attr)))
+		decode-projection
+			       (:instance project-invert-commuting-better
+				 (type (type-0 m))
+				 (gem-cell (get-cell (gemvar-0 m) gem-typed-mem))
+				 (rtmvars (rtmintvars-0 m)))))))
+
+
+
+(defthm decode-project-commuting
+ (implies
+  (and
+   (is-typed-amem-p gem-typed-mem)
+   (correct-wrt-arity m gem-typed-mem)
+   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
+   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem))
+ (equal
+  (projectio (decode m rtm-typed-mem) attr)
+  (decode m (projectio rtm-typed-mem attr)))))
+
+
+
+(in-theory (disable get-cell put-cell))
+
+(defthm equalwrt-holds-on-project
+ (implies
+  (equal-wrt-vars m0 m1 m2)
+  (equal-wrt-vars m0 (projectio m1 attr) (projectio m2 attr))))
+
+(defthm projectio-keeps-caars
+  (same-caars-p m0 (projectio m0 attr))
+ :hints (("Goal" :in-theory (enable put-cell))))
+
+
+(defthm equalwrt-holds-on-project-all
+ (implies
+  (equal-wrt-vars m0 m1 m2)
+  (equal-wrt-vars (projectio m0 attr) m1 m2))
+ :hints (("Goal" :use (:instance if-same-caars-same-equality-wrt-vars
+				 (vars1 m0)
+				 (vars2 (projectio m0 attr))
+				 (mem1 m1)
+				 (mem2 m2)))))
+
+(defthm equalwrt-holds-on-project-all-all
+ (implies
+  (equal-wrt-vars m0 m1 m2)
+  (equal-wrt-vars (projectio m0 attr) (projectio m1 attr) (projectio m2 attr)))
+ :hints (("Goal" :use (:instance if-same-caars-same-equality-wrt-vars
+				 (vars1 m0)
+				 (vars2 (projectio m0 attr))
+				 (mem1 m1)
+				 (mem2 m2)))))
+
+(defthm equal-memories-holds-by-projection
+ (implies
+  (equal-memories m1 m2)
+  (equal-memories (projectio m1 attr) (projectio m2 attr))))
+
+
+
+
+(defthm equalities-on-io
+ (implies
+  (and
+   (rel-prime-moduli *rns*)
+   (integer-listp *rns*)
+   (not (null *rns*))
+   (m-entries-point-to-good-rtm-var-sets m rtm-typed-mem)
+   (vars-inclusion gem-typed-mem m)
+   (vars-inclusion m gem-typed-mem)
+   (m-correspondent-values-p m gem-typed-mem rtm-typed-mem)
+   (is-typed-amem-p gem-typed-mem)
+   (bounded-amem-p gem-typed-mem)
+   (correct-wrt-arity m gem-typed-mem))
+  (equal-memories (decode m (projectio rtm-typed-mem attr)) (projectio gem-typed-mem attr)))
+ :hints (("Goal"
+	  :in-theory (enable
+		      equal-memories-commutative
+		      retrieving-keeps-equality
+		      decode-equals-retrieve-vars
+		      equal-wrt-vars-reflexive
+		      equal-wrt-vars-transitive
+		      equalwrt-holds-on-project-all)
+	  :use ( (:instance equal-memories-holds-by-projection
+			    (m1 (decode m rtm-typed-mem))
+			    (m2 gem-typed-mem))))))
+
+
+(defthm fact-bout-rns-v0
+  (and
+   (integer-listp *rns*)
+   (rel-prime-moduli *rns*)
+   (posp-all *rns*)
+   (not (null *rns*))
+   (natp (prod *rns*))
+   (> (prod *rns*) 1))
+  :hints (("Goal" :in-theory (enable prod posp rel-prime-moduli rel-prime-all rel-prime g-c-d
+  posp-all
+  (:executable-counterpart nonneg-int-gcd))))
+  :rule-classes nil)
+
+(defun append-lists (list-of-lists)
+ (if (endp list-of-lists)
+     nil
+     (append (car list-of-lists)
+             (append-lists (cdr list-of-lists)))))
+
+(defun retrieve-gemvars (m)
+  (if
+      (endp m)
+      nil
+    (cons (gemvar-0 m) (retrieve-gemvars (cdr m)))))
+
+(defun retrieve-rtmvars (m)
+  (if (endp m)
+      nil
+    (cons (cdr (car m))
+	  (retrieve-rtmvars (cdr m)))))
+
+(defun gem-variables (m) (retrieve-gemvars m))
+(defun rtm-variables (m) (append-lists (retrieve-rtmvars m)))
+
+(defun same-vars (m1 m2)
+ (and
+  (vars-inclusion m1 m2)
+  (vars-inclusion m2 m1)))
+
+(defun member-equal-bool (el l)
+ (declare (xargs :guard (true-listp l)))
+ (cond ((endp l) nil)
+       ((equal el (car l)) t)
+       (t (member-equal-bool el (cdr l)))))
+
+(defun no-tmp-into-mapping (m)
+  (if (endp m)
+      t
+    (and
+     (not (member-equal-bool 'tmp (rtmintvars-0 m)))
+     (no-tmp-into-mapping (cdr m)))))
+
+(defun no-duplicates-p (l)
+ (if (endp l)
+     t
+     (and (not (member-equal-bool (car l) (cdr l)))
+          (no-duplicates-p (cdr l)))))
+
+
+(defun apply-direct-rns-to-value-depending-on-type (gemvalue type)
+ (cond ( (equal type 'bool) (list gemvalue) )
+       ( (equal type 'int)  (build-values-by-rns-extended-for-nil gemvalue *rns*) )
+       ( t nil )))
+
+(defun represent-same-values-p (gemvalue rtmvalues type)
+ (equal-values
+  rtmvalues
+  (apply-direct-rns-to-value-depending-on-type gemvalue type)))
+
+
+(defun m-correspondent-vals-p (m gem-typed-mem rtm-typed-mem)
+ (cond
+  ( (endp m)
+    (null m) )
+  ( t
+    (and
+     (represent-same-values-p
+      (var-value (get-cell (gemvar-0 m) gem-typed-mem))
+      (var-values (rtmintvars-0 m) rtm-typed-mem)
+      (type-0 m))
+     (m-correspondent-vals-p (cdr m)  gem-typed-mem rtm-typed-mem)))))
+
+
+(defun attributes-correspondence (m gem-typed-mem rtm-typed-mem)
+  (if (endp m)
+      (null m)
+    (and
+     (not (endp (rtmintvars-0 m)))
+     (true-listp (rtmintvars-0 m))
+     (not (equal 'error-value (get-common-value (var-attributes (rtmintvars-0 m) rtm-typed-mem))))
+     (equal-elements
+      (var-attribute (get-cell (gemvar-0 m) gem-typed-mem))
+      (var-attributes (rtmintvars-0 m) rtm-typed-mem))
+    (attributes-correspondence (cdr m) gem-typed-mem rtm-typed-mem))))
+
+
+(defthm redefinition-of-m-corr
+ (equal
+  (and
+   (m-entries-point-to-good-rtm-var-sets m rtm-vars)
+   (m-correspondent-values-p m gem-vars rtm-vars))
+  (and
+   (attributes-correspondence m gem-vars rtm-vars)
+   (m-correspondent-vals-p m gem-vars rtm-vars)))
+ :rule-classes nil)
+
+
+
+(defun is-variable-mapping (m gem-vars rtm-vars)
+  (and
+   (alistp m)
+   (no-tmp-into-mapping m)
+   (no-duplicates-p (gem-variables m))
+   (no-duplicates-p (rtm-variables m))
+   (correct-wrt-arity m gem-vars)
+   (same-vars gem-vars m)
+   (attributes-correspondence m gem-vars rtm-vars)
+   (m-correspondent-vals-p m gem-vars rtm-vars)))
+
+(defun output (mem) (projectio mem 'Output))
+
+(defun is-gem-mem-p (mem)
+ (and (is-typed-amem-p mem)
+      (bounded-amem-p mem)))
+
+(defthm mapping-correspondence-implies-same-outputs
+ (implies
+  (and
+   (is-variable-mapping m gem-mem rtm-mem)
+   (is-gem-mem-p gem-mem))
+  (equal-memories
+   (output gem-mem)
+   (decode m (output rtm-mem))))
+ :hints (("Goal" :use
+          (fact-bout-rns-v0
+           (:instance redefinition-of-m-corr
+                      (gem-vars gem-mem)
+                      (rtm-vars rtm-mem))
+           (:instance equalities-on-io
+                      (gem-typed-mem gem-mem)
+                      (rtm-typed-mem rtm-mem))
+           (:instance equal-memories-commutative
+                      (mem1 (output gem-mem))
+                      (mem2 (decode m (output rtm-mem)))))))
+ :rule-classes nil)
+
+
+
+(in-theory (disable correct-arity-all-i-need
+		    if-every-element-matches-val-then-get-common-value-amounts-to-val
+		    make-null-list-is-invariant-on-value-slicing
+		    build-values-by-rns-extended-for-nils-provides-integers-from-integer
+		    build-value-by-inverse-rns-extended-for-nils-behaves-standardly-on-integer-lists
+		    crt-inversion-extended-to-nils-in-integer-case
+		    apply-direct-rns-unfolding-for-integer-case
+		    apply-direct-rns-unfolding-for-boolean-case
+		    apply-inverse-direct-retrieves-same-value-for-typed-cells
+		    inversion-for-empty-cell
+		    ad-hoc-2-for-inversion-of-one-nonempty-cell-by-decode
+		    ad-hoc-3-for-inversion-of-one-nonempty-cell-by-decode
+		    nonempty-cell-is-not-mapped-into-nils-by-rns
+		    nonempty-rtm-vars-which-correspond-to-gem-var-by-values-and-atributes-map-back-to-gem-var
+		    decode-inversion-for-nonempty-gem-cell
+		    invert-cell-inverts-for-m-correspondents
+		    ;any-cell-of-a-typed-mem-is-nil-or-a-typed-cell
+		    silly1
+		    silly2
+		    decode-equals-retrieve-vars
+		    decode-retrieves-gem-memory
+		    cell-of-projected-mem-is-projected-cell
+		    projection-of-null-list-is-null-list
+		    null-cell-corresponds-to-null-lists-of-values
+		    project-invert-commute-for-empty-cell
+		    rtmvars-correspondent-to-nonemptycell-is-not-emptylist
+		    values-remain-the-same-if-correspondent-attrs
+		    attributes-same-1
+		    inversion-2-for-nonempty-projected-on-different-attr
+		    inversion-1-for-nonempty-projected-on-different-attr
+		    projecting-on-different-attr-gets-nils
+		    decode-one-entry-of-null-list-is-nil
+		    inversion-2-for-nonempty-projected-on-different-attr
+		    inversion-for-nonempty-projected-on-different-attr
+		    project-invert-commuting
+		    letssimplify
+		    project-invert-commuting-better
+		    decode-projection-is-decode-of-projection
+		    decode-project-commuting
+		    equalwrt-holds-on-project-all
+		    equalwrt-holds-on-project-all-all
+		    equal-memories-holds-by-projection
+		    equalities-on-io))
+
+
+
+
+
+
+
+