something was really too slow...

diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
index d78aac70e07e6abc655bc9aa9e4834e1a6479400..67f8ac1d6a5763dfab65e15b17128ed1d3f66b85 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
+++ b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
@@ -1247,7 +1247,8 @@ a = b \to b \neq c \to a \neq c.
 intros.
 generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
 intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
-autobatch.assumption.
+apply ap_symmetric_unfolded. assumption.
+assumption.
 qed.
 
 lemma Dir_bij : \forall A, B:CSetoid. 

diff --git a/helm/software/matita/library/assembly/byte.ma b/helm/software/matita/library/assembly/byte.ma
index 583051e27c48ed1b0991eed43338358fbb0fedd2..f2d1dc1566b7194903c2eda58d1eafd853a37ff9 100644 (file)
--- a/helm/software/matita/library/assembly/byte.ma
+++ b/helm/software/matita/library/assembly/byte.ma
@@ -66,7 +66,7 @@ lemma lt_nat_of_byte_256: ∀b. nat_of_byte b < 256.
   [ letin Hf ≝ (le_plus ? ? ? ? Hcut K'); clearbody Hf;
     simplify in Hf:(? ? %);
     assumption
-  | autobatch
+  | apply le_times_r. apply H'.
   ]
 qed.
 
@@ -107,7 +107,7 @@ lemma eq_nat_of_byte_n_nat_of_byte_mod_n_256:
     rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
     rewrite > divides_to_eq_mod_mod_mod;
      [ reflexivity
-     | autobatch
+     | apply (witness ? ? 16). reflexivity.
      ]
   ]
 qed.
@@ -117,7 +117,8 @@ lemma plusbyte_ok:
   match plusbyte b1 b2 c with
    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_byte r + nat_of_bool c' * 256
    ].
- intros;
+ intros; elim daemon.
+ (* 
  unfold plusbyte;
  generalize in match (plusex_ok (bl b1) (bl b2) c);
  elim (plusex (bl b1) (bl b2) c);
@@ -149,6 +150,7 @@ lemma plusbyte_ok:
  rewrite < associative_plus in ⊢ (? ? (? ? (? % ?)) ?);
  rewrite > H; clear H;
  autobatch paramodulation.
+ *)
 qed.
 
 definition bpred ≝

diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma
index fb1a14ede914299c6b2e9342296e846c39dc54b0..761c06c94718ce89014d63e06622198fad0d83ab 100644 (file)
--- a/helm/software/matita/library/assembly/exadecimal.ma
+++ b/helm/software/matita/library/assembly/exadecimal.ma
@@ -801,7 +801,8 @@ lemma exadecimal_of_nat_mod:
  change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
  rewrite < mod_mod;
   [ apply H;
-    autobatch
+    unfold lt;
+    autobatch.
   | autobatch
   ]
 qed.
@@ -848,11 +849,7 @@ lemma plusex_ok:
   match plusex b1 b2 c with
    [ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
  intros;
- elim c;
- elim b1;
- elim b2;
- normalize;
- reflexivity.
+ elim b1; (elim b2; (elim c; normalize; reflexivity)).
 qed.
 
 definition xpred ≝