(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)
        )))