2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/nat.ma".
16 let rec iter (A:Type[0]) (g:A→A) n a on n ≝
19 |S m ⇒ g (iter A g m a)].
21 interpretation "iteration" 'exp g i = (iter ? g i).
23 lemma le_iter: ∀g,a. (∀x. x ≤ g x) → ∀i. a ≤ g^i a.
24 #g #a #leg #i elim i //
25 #n #Hind @(transitive_le … Hind) @leg
28 lemma iter_iter: ∀A.∀g:A→A.∀a,b,c.
29 g^c (g^b a) = g^(b+c) a.
31 [<plus_n_O normalize //
32 |#m #Hind <plus_n_Sm normalize @eq_f @Hind
36 lemma monotonic_iter: ∀g,a,b,i. (monotonic ? le g) → a ≤ b →
38 #g #a #b #i #Hmono #leab elim i //
39 #m #Hind normalize @Hmono //
42 lemma monotonic_iter2: ∀g,a,i,j. (∀x. x ≤ g x) → i ≤ j →
44 #g #a #i #j #leg #leij elim leij //
45 #m #leim #Hind normalize @(transitive_le … Hind) @leg