X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FRELATIONAL%2FNPlus%2Ffwd.ma;h=0b8ba2b889b35456329db195600137dee4dbed4d;hb=e876a6805b98ae4cf5d826234001fac907d0ecc2;hp=9b23cb2fb3c3248d6904ac841a3da2424b0c6f17;hpb=b531c938515b0ea6cb92df2e8732c587e0bc026b;p=helm.git

diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
index 9b23cb2fb..0b8ba2b88 100644
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
@@ -22,68 +22,66 @@ include "NPlus/defs.ma".
 theorem nplus_gen_zero_1: \forall q,r. (zero + q == r) \to q = r.
  intros. elim H; clear H q r; intros;
  [ reflexivity
- | clear H1. auto
+ | clear H1. auto new timeout=30
  ].
 qed.
 
 theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to 
-                           \exists s. r = (succ s) \land (p + q == s).
+                          \exists s. r = (succ s) \land p + q == s.
  intros. elim H; clear H q r; intros;
  [
  | clear H1.
    decompose.
-   rewrite > H1. clear H1 n2
- ]; apply ex_intro; [| auto || auto ]. (**)
+   subst.
+ ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**)
 qed.
 
 theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r.
  intros. inversion H; clear H; intros;
- [ auto
+ [ auto new timeout=30
  | clear H H1.
    lapply eq_gen_zero_succ to H2 as H0. apply H0
  ].
 qed.
 
 theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to 
-                           \exists s. r = (succ s) \land (p + q == s).
+                          \exists s. r = (succ s) \land p + q == s.
  intros. inversion H; clear H; intros;
  [ lapply eq_gen_succ_zero to H as H0. apply H0
  | clear H1 H3 r.
    lapply linear eq_gen_succ_succ to H2 as H0.
-   rewrite > H0. clear H0 q.
-   apply ex_intro; [| auto ] (**)
+   subst.
+   apply ex_intro; [| auto new timeout=30 ] (**)
  ].
 qed.
 
 theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to 
-                           p = zero \land q = zero.
+                          p = zero \land q = zero.
  intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1 p.
-   auto
+ [ subst. auto new timeout=30
  | clear H H1.
    lapply eq_gen_zero_succ to H3 as H0. apply H0
  ].
 qed.
 
 theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to
-                           \exists s. p = succ s \land (s + q == r) \lor
-                                      q = succ s \land (p + s == r).
+                          \exists s. p = succ s \land (s + q == r) \lor
+                                     q = succ s \land p + s == r.
  intros. inversion H; clear H; intros;
- [ rewrite < H1. clear H1 p
+ [ subst.
  | clear H1.
    lapply linear eq_gen_succ_succ to H3 as H0.
-   rewrite > H0. clear H0 r.
- ]; apply ex_intro; [| auto || auto ] (**)
+   subst.
+ ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ] (**)
 qed.
 (*
 (* alternative proofs invoking nplus_gen_2 *)
 
 variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to 
-                               p = zero \land q = zero.
+                              p = zero \land q = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p.
-   auto
+   subst. auto new timeout=30
  | clear H.
    lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
@@ -92,17 +90,17 @@ variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to
 qed.
 
 variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to
-                               \exists s. p = succ s \land (s + q == r) \lor
-                                          q = succ s \land (p + s == r).
+                              \exists s. p = succ s \land (s + q == r) \lor
+                                         q = succ s \land p + s == r.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p
+   subst
  | clear H.
    lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    lapply linear eq_gen_succ_succ to H1 as H0.
-   rewrite > H0. clear H0 r.
- ]; apply ex_intro; [| auto || auto ]. (**)
+   subst
+ ]; apply ex_intro; [| auto new timeout=30 || auto new timeout=30 ]. (**)
 qed.
 *)
 (* other simplification lemmas *)
@@ -110,21 +108,21 @@ qed.
 theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
-   rewrite > H0. clear H0 p
+   subst
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    lapply linear eq_gen_succ_succ to H2 as H0.
-   rewrite < H0 in H3. clear H0 a
- ]; auto.
+   subst
+ ]; auto new timeout=30.
 qed.
 
 theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  intros 1. elim p; clear p; intros;
  [ lapply linear nplus_gen_zero_1 to H as H0.
-   rewrite > H0. clear H0 q
+   subst
  | lapply linear nplus_gen_succ_1 to H1 as H0.
    decompose.
    lapply linear eq_gen_succ_succ to H2 as H0.
-   rewrite < H0 in H3. clear H0 a
- ]; auto.
+   subst
+ ]; auto new timeout=30.
 qed.