From a864e433a7774b1938ab8dd0beb0d87b7f3517cf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 16 Jul 2007 17:51:02 +0000 Subject: [PATCH] One daemon less. --- helm/software/matita/library/assembly/byte.ma | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma index d0f1ada88..67eb0b4cf 100644 --- a/helm/software/matita/library/assembly/byte.ma +++ b/helm/software/matita/library/assembly/byte.ma @@ -255,11 +255,13 @@ lemma plusbytenc_S: rewrite < byte_of_nat_nat_of_byte; rewrite > (plusbytenc_ok (byte_of_nat (x*n)) x); rewrite < times_n_Sm; - rewrite > mod_plus; - rewrite < eq_nat_of_byte_mod in ⊢ (? ? (? (? (? ? %) ?)) ?); - rewrite > nat_of_byte_byte_of_nat; - rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); -elim daemon. + rewrite > nat_of_byte_byte_of_nat in ⊢ (? ? (? (? (? % ?) ?)) ?); + rewrite > eq_nat_of_byte_n_nat_of_byte_mod_n_256 in ⊢ (? ? ? %); + rewrite > mod_plus in ⊢ (? ? (? %) ?); + rewrite > mod_plus in ⊢ (? ? ? (? %)); + rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ]; + rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?); + reflexivity. qed. lemma eq_plusbytec_x0_x0_x_false: -- 2.39.2