From d4383305e3d0fae68326d9f078b28d58b8e1f94a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 16 Jul 2007 16:07:42 +0000 Subject: [PATCH] One less daemon (about "update"s). --- helm/software/matita/library/assembly/test.ma | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) 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 ] ] ]. -- 2.39.2