- 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 72e8177b8a559e26be039f624bf1797f0c04fc3c..a36bd078c01877187072ee6fb804fd44beaacdaa 100644 (file)
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -16,7 +16,6 @@ set "baseuri" "cic:/matita/Z/times".
 
 include "nat/lt_arith.ma".
 include "Z/plus.ma".
 
 include "nat/lt_arith.ma".
 include "Z/plus.ma".

-include "higher_order_defs/functions.ma".

 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.
 
 definition Ztimes :Z \to Z \to Z \def
 \lambda x,y.


@@ -79,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.


@@ -105,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.
 


@@ -135,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 *)


@@ -152,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.


@@ -237,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.