made executable again

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_iter.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
index 89c464804225a25d65e3d3ac5f00c1ac76dae44c..fc824317ab5e517f08f63f73c9945ef5528dfac3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
@@ -15,12 +15,13 @@
 include "ground/arith/pnat_iter.ma".
 include "ground/arith/nat.ma".
 
-(* NON-NEGATIVE INTEGERS ****************************************************)
+(* ITERATED FUNCTION FOR NON-NEGATIVE INTEGERS ******************************)
 
+(*** iter *)
 definition niter (n:nat) (A:Type[0]) (f:A→A) (a:A) ≝
 match n with
 [ nzero  ⇒ a
-| ninj p ⇒ f^{A}p a
+| ninj p ⇒ (f^{A}p) a
 ]
 .
 
@@ -28,17 +29,27 @@ interpretation
   "iterated function (non-negative integers)"
   'Exp A f n = (niter n A f).
 
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
 
+(*** iter_O *)
 lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
 // qed.
 
-lemma niter_inj (A) (f) (p) (a): f^p a = f^{A}(ninj p) a.
+lemma niter_inj (A) (f) (p): f^p ⊜ f^{A}(ninj p).
 // qed.
 
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
 
-lemma niter_appl (A) (f) (n) (a): f (f^n a) = f^{A}n (f a).
+(*** iter_n_Sm *)
+lemma niter_appl (A) (f) (n): f ∘ f^n ⊜ f^{A}n ∘ f.
 #A #f * //
-#p #a <niter_inj <niter_inj <piter_appl //
+#p @exteq_repl
+/2 width=5 by piter_appl, compose_repl_fwd_dx/
+qed.
+
+lemma niter_compose (A) (B) (f) (g) (h) (n):
+      h ∘ f ⊜ g ∘ h → h ∘ (f^{A}n) ⊜ (g^{B}n) ∘ h.
+#A #B #f #g #h * //
+#p #H @exteq_repl
+/2 width=5 by piter_compose, compose_repl_fwd_dx/
 qed.