run check_if_goal_is_solved on all goals (active+passive)

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index fb60178391e968425257d08ad297b0620ddeb28b..96b4d515bef9792e68a862998179adec61c7cc50 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -903,7 +903,7 @@ let check_if_goals_set_is_solved bag env active passive goals =
             (fun bag -> check_if_goal_is_subsumed bag env (last passive))
              ])
 (* provare active and passive?*)
-    (bag,None) active_goals
+    (bag,None) (active_goals @ passive_goals)
 ;;
 
 let infer_goal_set bag env active goals = 

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index ce79a875b42437cf809d72d2433bfc9f2cb59409..9e7ba97f5afbb4c03c5c358bcd4f9c02ad9f8dd3 100644 (file)
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -204,18 +204,18 @@ intros;autobatch paramodulation;
 qed. *)
 
 lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro; autobatch paramodulation. 
-(*
+(*intro; autobatch paramodulation.*)  
+intros;
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
 rewrite < assoc_Rplus;
 apply eq_f2;autobatch paramodulation;
-*)
+
 qed.
 
 lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro. autobatch paramodulation. (*
-auto paramodulation.
+intro. (*autobatch paramodulation.*) 
+
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
 rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
@@ -225,7 +225,7 @@ rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?);
 apply eq_f2 [reflexivity]
 rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
 rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
-*)
+
 qed.
 
 lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
@@ -362,16 +362,13 @@ lapply (Rlt_times_l (Rinv x * Rinv y) ? ? H1)
 qed.
 
 lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros;
-(* cut (∀x,y.x+(-x+y) = y);[2:
-intros.demodulate all.]
-applyS (Rlt_plus_l c (-?+a) (-b) ?) by (Hcut c a);
- [2: applyS Hletin;
-lapply (Rlt_plus_l (-b) ?? H); autobatch; applyS Hletin; *)
+intros; autobatch depth=4;
+(*
 rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
 rewrite < assoc_Rplus;
 rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
 apply Rlt_plus_l;assumption;
+*)
 qed.
 
 lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b.

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index 8e7483e96acf6551e376cc3445736c21cdd97a74..a425dfcc357783ee52a23f8215be3d91265d29b5 100644 (file)
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -259,10 +259,13 @@ theorem derivative_power: ∀n:nat. D[X \sup n] = n·X \sup (pred n).
      (D[X \sup (1+m)])
    = (D[X · X \sup m]).
    = (D[X] · X \sup m + X · D[X \sup m]).
-   = (X \sup m + X · (m · X \sup (pred m))) timeout=30.
+   = (X \sup m + X · (m · X \sup (pred m))). 
+   lapply depth=0 Fmult_associative;
+   lapply depth=0 Fmult_commutative;
+   = (X \sup m + m · (X · X \sup (pred m))) by Fmult_associative, Fmult_commutative.
    = (X \sup m + m · (X \sup (1 + pred m))).
    = (X \sup m + m · X \sup m).
-   = ((1+m) · X \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
+   = ((1+m) · X \sup m) by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
   done.
 qed.