From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 20 Jul 2007 16:59:27 +0000 (+0000)
Subject: Another nicer version.
X-Git-Tag: make_still_working~6142
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1af4dbaef15ec116e5d592334acc2ba79b732472;p=helm.git

Another nicer version.
---

diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma
index a9726efcb..644cebaa9 100644
--- a/helm/software/matita/library/assembly/test.ma
+++ b/helm/software/matita/library/assembly/test.ma
@@ -216,21 +216,10 @@ lemma loop_invariant':
               reflexivity
             |6: intro;
               simplify in ⊢ (? ? ? %);
+              normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? (? %) ?) ?) ?) ?);
               change in ⊢ (? ? % ?) with
-               (update
-                (update
-                 (update
-                  (update (update (mult_memory x y) 30 x) 31
-                   (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
-                    (byte_of_nat (nat_of_byte y-S n)))
-                   (nat_of_byte
-                    (update
-                     (update
-                      (update (update (mult_memory x y) 30 x) 31
-                       (byte_of_nat (S (nat_of_byte y-S n)))) 32 (byte_of_nat (nat_of_byte x*n))) 31
-                      (byte_of_nat (nat_of_byte y-S n)) 15))
-                     (byte_of_nat (nat_of_byte x*S n)) a);
-              normalize in ⊢ (? ? (? ? % ? ?) ?);
+               ((mult_memory x y){30↦x}{31↦#(S (y-S n))}{32↦#(x*n)}{31↦#(y-S n)}
+                {〈x2,x0〉↦ #(x*S n)} a);
               apply inj_update;
               intro;
               apply inj_update;