include "ground/notation/functions/exp_3.ma".
include "ground/arith/pnat.ma".
-(* POSITIVE INTEGERS ********************************************************)
+(* ITERATED FUNCTION FOR POSITIVE INTEGERS **********************************)
+(* Note: see also: lib/arithemetics/bigops.ma *)
rec definition piter (p:pnat) (A:Type[0]) (f:A→A) (a:A) ≝
match p with
[ punit ⇒ f a
"iterated function (positive integers)"
'Exp A f p = (piter p A f).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
lemma piter_unit (A) (f) (a): f a = (f^{A}𝟏) a.
// qed.
lemma piter_succ (A) (f) (p) (a): f (f^p a) = f^{A}(↑p) a.
// qed.
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
lemma piter_appl (A) (f) (p) (a): f (f^p a) = f^{A}p (f a).
#A #f #p elim p -p //