From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jul 2007 16:07:42 +0000 (+0000)
Subject: One less daemon (about "update"s).
X-Git-Tag: make_still_working~6171
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d4383305e3d0fae68326d9f078b28d58b8e1f94a;p=helm.git

One less daemon (about "update"s).
---

diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma
index b2494615b..894e1bc96 100644
--- a/helm/software/matita/library/assembly/test.ma
+++ b/helm/software/matita/library/assembly/test.ma
@@ -330,7 +330,15 @@ theorem test_x_y:
      | rewrite < minus_n_n;
        apply status_eq;
         [1,2,3,4,5,7: normalize; reflexivity
-        | elim daemon
+        | intro;
+          change with (update (update (update (mult_memory x y) 30 x) 31 (byte_of_nat O)) 32
+(byte_of_nat (nat_of_byte x*nat_of_byte y)) a =
+           update (update (mult_memory x y) 31 (mk_byte x0 x0)) 32
+(byte_of_nat (nat_of_byte x*nat_of_byte y)) a);
+          apply inj_update; intro;
+          apply inj_update; intro;
+          change in ⊢ (? ? (? ? ? % ?) ?) with (mult_memory x y 30);
+          apply eq_update_s_a_sa
         ]
      ]
   ].