- bugfix: eta abstractions ignores attributed node while counting lambdas

[helm.git] / helm / matita / library / Z / times.ma

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index c4e965fbf356f7e198a8e24f7d26d3767ad70700..a36bd078c01877187072ee6fb804fd44beaacdaa 100644 (file)
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -78,24 +78,24 @@ intros.elim x.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

         apply lt_O_times_S_S.apply lt_O_times_S_S.
   elim y.
     simplify.reflexivity.
         apply lt_O_times_S_S.apply lt_O_times_S_S.
   elim y.
     simplify.reflexivity.


@@ -104,24 +104,24 @@ intros.elim x.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
          apply lt_O_times_S_S.apply lt_O_times_S_S.
     elim z.
       simplify.reflexivity.
       change with 
       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
          apply lt_O_times_S_S.apply lt_O_times_S_S.
       change with 
       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
         (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).

-        rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+        rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.

          apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
 
          apply lt_O_times_S_S.apply lt_O_times_S_S.
 qed.
 


@@ -134,8 +134,8 @@ eq nat (times (S n) (S (pred (minus (S p) (S q)))))
        (minus (pred (times (S n) (S p))) 
               (pred (times (S n) (S q)))).
 intros.
        (minus (pred (times (S n) (S p))) 
               (pred (times (S n) (S q)))).
 intros.

-rewrite < S_pred ? ?.  
-rewrite > minus_pred_pred ? ? ? ?.
+rewrite < S_pred.  
+rewrite > minus_pred_pred.

 rewrite < distr_times_minus. 
 reflexivity.  
 (* we now close all positivity conditions *)
 rewrite < distr_times_minus. 
 reflexivity.  
 (* we now close all positivity conditions *)


@@ -151,7 +151,7 @@ intros.
 simplify. 
 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
 simplify. 
 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).

-rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_pred_pred.

 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.
 apply nat_compare_elim p q.
 rewrite < nat_compare_times_l.
 rewrite < nat_compare_S_S.
 apply nat_compare_elim p q.


@@ -236,4 +236,4 @@ qed.
 
 variant distr_Ztimes_Zplus: \forall x,y,z.
 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
 
 variant distr_Ztimes_Zplus: \forall x,y,z.
 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def

-distributive_Ztimes_Zplus.
\ No newline at end of file
+distributive_Ztimes_Zplus.