X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fbyte8.ma;h=c49297e3a8a2e14f141a9d77e9dbd7b1475ec7e7;hb=6ee4fa0ba5f4b6601b62afd482d4f30bd2de2f91;hp=dfff4c8a80e883a04467196392e85de986f19592;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma
index dfff4c8a8..c49297e3a 100644
--- a/helm/software/matita/contribs/assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/assembly/freescale/byte8.ma
@@ -340,12 +340,12 @@ lemma nat_of_byte8_byte8_of_nat: ∀n. nat_of_byte8 (byte8_of_nat n) = n \mod 25
  rewrite > mod_plus in ⊢ (? ? % ?);
  rewrite > mod_plus in ⊢ (? ? ? %);
  apply eq_mod_to_eq_plus_mod;
- rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch];
- rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch];
+ rewrite < mod_mod in ⊢ (? ? ? %); [ | autobatch by divides_n_n];
+ rewrite < mod_mod in ⊢ (? ? % ?); [ | autobatch by divides_n_n];
  rewrite < (eq_mod_times_times_mod ? ? 16 256) in ⊢ (? ? (? % ?) ?); [2: reflexivity | ];
  rewrite < mod_mod in ⊢ (? ? % ?);
   [ reflexivity
-  | autobatch
+  | autobatch by divides_n_n
   ].
 qed.
 
@@ -412,8 +412,11 @@ theorem plusb8nc_ok:
  rewrite > mod_plus;
  letin K ≝ (eq_nat_of_byte8_mod a); clearbody K;
  letin K' ≝ (eq_mod_times_n_m_m_O (nat_of_bool b) 256 ?); clearbody K';
-  [ autobatch | ];
- autobatch paramodulation.
+  [ unfold;apply le_S_S;apply le_O_n| ];
+ rewrite > K' in ⊢ (? ? ? (? (? ? %) ?));
+ rewrite < K in ⊢ (? ? ? (? (? % ?) ?));
+ rewrite < plus_n_O;
+ apply K;
 qed.
 
 lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
@@ -434,7 +437,7 @@ lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
     | unfold eq_b8;
       change in ⊢ (? ? (? % ?) ?) with (eq_ex x0 (exadecim_of_nat (S b/16)));
       letin K ≝ (leq_m_n_to_eq_div_n_m_S (S b) 16 ? ?);
-       [ autobatch
+       [ unfold; autobatch by le_S_S,le_O_n;
        | unfold in H1;
          apply le_S_S;
          assumption
@@ -447,12 +450,12 @@ lemma eq_eqb8_x0_x0_byte8_of_nat_S_false:
             unfold lt in H;
             rewrite < H2;
             clear H2; clear a; clear H1; clear Hcut;
-            apply (le_times_to_le 16) [ autobatch | ] ;
-            rewrite > (div_mod (S b) 16) in H;[2:autobatch|]
-            rewrite > (div_mod 255 16) in H:(? ? %);[2:autobatch|]
+            apply (le_times_to_le 16) [ autobatch by le_S_S,le_O_n;| ] ;
+            rewrite > (div_mod (S b) 16) in H;[2:unfold; autobatch by le_S_S,le_O_n;|]
+            rewrite > (div_mod 255 16) in H:(? ? %);[2:unfold; autobatch by le_S_S,le_O_n;|]
             lapply (le_to_le_plus_to_le ? ? ? ? ? H);
             [apply lt_S_to_le;
-             apply lt_mod_m_m;autobatch
+             apply lt_mod_m_m; unfold; apply le_S_S; apply le_O_n;
             |rewrite > sym_times;
              rewrite > sym_times in ⊢ (? ? %);
              normalize in ⊢ (? ? %);apply Hletin;
@@ -486,9 +489,9 @@ lemma eq_b8pred_S_a_a:
     rewrite > nat_of_exadecim_exadecim_of_nat in Hletin1;
     elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
     rewrite > H1;
-    rewrite > lt_O_to_div_times; [2: autobatch | ]
+    rewrite > lt_O_to_div_times; [2: unfold; apply le_S_S; apply le_O_n; | ]
     lapply (eq_f ? ? (λx.x/16) ? ? H1);
-    rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
+    rewrite > lt_O_to_div_times in Hletin; [2: unfold; apply le_S_S; apply le_O_n; | ]
     lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
     rewrite > eq_mod_times_n_m_m_O in Hletin1;
     elim daemon
@@ -521,7 +524,7 @@ lemma plusb8nc_S:
  rewrite > eq_nat_of_byte8_n_nat_of_byte8_mod_n_256 in ⊢ (? ? ? %);
  rewrite > mod_plus in ⊢ (? ? (? %) ?);
  rewrite > mod_plus in ⊢ (? ? ? (? %));
- rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: autobatch | ];
+ rewrite < mod_mod in ⊢ (? ? (? (? (? % ?) ?)) ?); [2: apply divides_n_n; | ];
  rewrite > sym_plus in ⊢ (? ? (? (? % ?)) ?);
  reflexivity.
 qed.