From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 16 Jul 2007 17:51:02 +0000 (+0000)
Subject: One daemon less.
X-Git-Tag: make_still_working~6168
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a864e433a7774b1938ab8dd0beb0d87b7f3517cf;p=helm.git

One daemon less.
---

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: