X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Ftest.ma;h=1fd030efb1bb998c0302fdb3bab8c8f7695ef905;hb=ee24d241030e7577e5456f6dd151faf7622b86ce;hp=b2494615be6dc7444ac87f04c156f780dba2ca1a;hpb=6e2b36b557fd85add998926a777e7f12933293fc;p=helm.git

diff --git a/helm/software/matita/library/assembly/test.ma b/helm/software/matita/library/assembly/test.ma
index b2494615b..1fd030efb 100644
--- a/helm/software/matita/library/assembly/test.ma
+++ b/helm/software/matita/library/assembly/test.ma
@@ -214,7 +214,9 @@ lemma loop_invariant':
            normalize in ⊢ (? ? (? (? ? % ? ? ? ? ?) ?) ?);
            normalize in ⊢ (? ? (? (? ? ? ? ? ? (? ? % ?) ?) ?) ?);
            cut (y - S n = a);
-            [2: elim daemon | ];
+            [2: rewrite > eq_minus_S_pred;
+                rewrite > H2;
+                reflexivity | ];
            rewrite < Hcut; clear Hcut; clear H3; clear H2; clear a;          
            (* instruction ADDd *)
            letin K ≝
@@ -330,7 +332,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
         ]
      ]
   ].