```
(def-recursive-constant iterate
"lambda(iter:[zz,ind_1], f:[ind_1,ind_1],x:ind_1,
lambda(n:zz, if(n=0,x,f(iter(n-1)))))"
(theory generic-theory-1)
(definition-name iterate))
```

```
(def-theorem iterate-definedness
"forall(f:[ind_1,ind_1],x:ind_1,z:zz,
total_q{f,[ind_1,ind_1]} and 0<=z implies #(iterate(f,x)(z)))"
(theory generic-theory-1)
(usages transportable-macete)
(proof
(
(induction integer-inductor ())
)))
```

```
(def-theorem undefined-for-negative
"forall(n:zz,x:ind_1,f:[ind_1,ind_1],n<0 implies not(#(iterate(f,x)(n))))"
(theory generic-theory-1)
(usages transportable-macete)
(proof
(
(instantiate-theorem iterate-minimality_generic-theory-1 ("f" "x"))
(instantiate-universal-antecedent "with(f:[ind_1,ind_1],x:ind_1,
forall(h_0:[zz,ind_1],
h_0=lambda(n:zz,if(n=0, x, f(h_0(n-1))))
implies
forall(u_0:zz,
#(iterate(f,x)(u_0))
implies
iterate(f,x)(u_0)=h_0(u_0))));" ("lambda(n:zz,if(n<0,?ind_1,iterate(f,x)(n)))"))
(contrapose "with(p:prop, not(p))")
extensionality
direct-inference
(unfold-single-defined-constant (0) iterate)
(case-split ("x_0<0"))
simplify
simplify
direct-inference
(backchain "with(p:prop, t:ind_1,  forall(u:zz, #(t) implies p))")
simplify
)))
```

```
(def-theorem iterate-translate
"forall(n:zz,x:ind_1,f:[ind_1,ind_1],
f oo (iterate(f,x))=lambda(n:zz,if(n=[-1],?ind_1,iterate(f,x)(n+1))))"
(theory generic-theory-1)
(usages transportable-macete)
(proof
(

direct-inference
(unfold-single-defined-constant (1) iterate)
extensionality
direct-inference
simplify-insistently
(instantiate-theorem undefined-for-negative ("x_0" "x" "f"))
simplify
simplify
))
)
```

```
(def-theorem iterate-totality
"total_q{iterate,[[ind_1,ind_1],ind_1,[zz,ind_1]]}"
(theory generic-theory-1)
(usages d-r-convergence transportable-macete)
(proof
(
insistent-direct-inference
(unfold-single-defined-constant (0) iterate)
)))
```