Introduction
Recursion and fixpoint equations
The mathematical content of the definition of a recursive function is a
fixpoint equation. Let us demonstrate this statement with a simple example.
The textbook example of a recursive function is the factorial function. In our
programming language it looks like
factorial(n:NATURAL): NATURAL
ensure
Result = if n=0 then 1
else n*factorial(n1)
end
end
The keyword Result
represents factorial(n)
i.e. the value of the function
at the argument n
. Since the postcondition is an equation the specification
of this function says
all(n:NATURAL)
ensure
factorial(n) = (if n=0 then 1 else n*factorial(n1) end)
end
This specification states that the function factorial
and the function n >
are the same function.
if n=0 then 1 else n*factorial(n1) end
From the function factorial
we can extract the functional (for convenience
we call a function which accepts and returns functions a functional)
f(g:NATURAL>NATURAL): NATURAL>NATURAL
ensure
Result = (n > if n=0 then 1 else n*g(n1) end)
end
and then the specification of the function factorial
reads like
all(n:NATURAL)
ensure
factorial(n) = f(factorial)(n)
end
i.e. the function factorial
has to satisfy the fixpoint equation
factorial = f(factorial)
From the mathematical point of view two questions arise
 Does the functional
f
have a fixpoint (i.e. existence)?  Is the fixpoint of the functional
f
unique?
If the answer to both question is yes then we can say that the functional
f
defines uniquely a function.
In this article we study this question for primitive recursive functions over
natural numbers of the form
G: ANY
gr(n:NATURAL): G
ensure
Result = if n=0 then c  c: constant (function)
else h(gr(n1),n)  h: total function
end
end
where the constant (function) c
and the function h:[G,NATURAL]>G
are well
defined. For the factorial function we have c=1
and h = ([a,b] > b*a)
.
Outline of the paper
We restrict our investigation about primitive recursive functions in this
paper to primitive recursive functions on natural numbers.
We do not use a specific type NATURAL
but an abstract class
ABSTRACT_NATURAL
. This is convenient because we can have different
implementations of natural numbers. One possible implementation is to use a
machine word (e.g. 32 or 64 bit) to implement natural numbers or to use a
sequence of numbers to implement arbitrary sized natural numbers. Since the
basic properties and assertions of all implementations are identical it is
sufficient to derive them once in an abstract module.
In the first chapter we introduce the module abstract_natural
, give the
basic definitions, prove the induction law, show that there are infinitely
many natural numbers, introduce an order relation on the abstract natural
numbers and show that the order is a wellorder.
In the second chapter we introduce a general format of recursive functions and
show that typical recursive functions fit into this pattern.
In the third chapter we scrutinize the functional which represents a primitive
recursive function. We proof that the functional is monotonic, continuous and
has a unique fixpoint.
The number zero, the empty set and the undefined function
In our programming language we can use constants like 0
as names of
functions. In the class of natural numbers the constant 0
specifies the
number zero. In the class of sets 0
represents the empty set and 1
represents the universal set. In the class of partial functions (type A>B
where A
and B
are arbitrary types) the constant 0
represents the
completely undefined functions i.e. the function with an empty domain.
In this article the constant 0
appears with all these meanings. Usually it
is clear from the context whether the number zero, the empty set or the
undefined function is meant. Sometimes type annotations like 0:G?
are used
to annotate that 0
is of type G?
and represents therefore the empty set of
elements of type G
.
Abstract natural numbers
Basic definitions
In the module abstract_natural
we want to use axioms which are equivalent to
the five peano axioms. The five peano axioms are:

Zero is a natural number

All natural numbers have successor

Zero is not the successor of a natural number

Two natural numbers which have the same successor are identical

Any property which is valid for the number zero and whose validity for any
number implies its validity for the successor of this number is valid for all
natural numbers.
The basic definition of the module abstract_natural
looks like:
deferred class
ABSTRACT_NATURAL
end
feature  Basic functions and axioms
0: CURRENT  peano 1
deferred end
succ(n:CURRENT): CURRENT  peano 2
deferred end
1: CURRENT
deferred ensure Result = succ(0) end
all(n,m:CURRENT)
deferred
ensure
zero_not_succ: n.succ /= 0  peano 3
succ_injective: n.succ=m.succ => n=m  peano 4
closed: (0).closed(succ) = (1:CURRENT?)  peano 5
end
end
In order to represent the first peano axiom we use the constant function
0
. The second peano axiom is represented by the successor function
succ
.
The third and forth peano axiom are represented by the assertions
zero_not_succ
and succ_injective
.
The assertion closed
says that we can reach all natural numbers by starting
from the number 0
and applying the successor function succ
an arbitrary
number of times. It will be shown in the next chapter that the assertion
closed
is equivalent to the fifth peano axiom.
Induction law
We are going to demonstrate that the assertion closed
is sufficient to prove
the classical induction law. Let us translate the fifth peano axiom
(induction) into our programming language
induction:
all(e:BOOLEAN)
require
r1: e[n:=0]
r2: all(n:CURRENT) e => e[n:=n.succ]
ensure
all(n:CURRENT) e  r1,r2, induction_lemma (see below)
end
Because (0).closed(succ)
is a closure we get the general law
closure_induction_1:
all(p:CURRENT?)
require
0 in p
p.is_closed(succ)
ensure
(0).closed(succ) <= p  See "Closures and fixpoints"
end
which have already been proved in the paper “Closures and fixpoints”. From
this law using closed
we can immediately derive the following assertion
closure_induction_2:
all(p:CURRENT?)
require
r1: 0 in p
r2: p.is_closed(succ)
check
c1: (0).closed(succ) <= p  r1,r2,closure_induction_1
c2: (1:CURRENT?) <= p  c1,closed
ensure
p = (1:CURRENT?)  c2, 1 is greatest set
end
Now it is easy to derive the classical induction law.
induction_lemma:
all(e:BOOLEAN)
require
r1: e[n:=0]
r2: all(n:CURRENT) e => e[n:=n.succ]
local
l1: p:CURRENT? := {n: e}
check
c1: 0 in p  l1,r1
c2: p.is_closed(succ)  l1,r2
c3: p = (1:CURRENT?)  c1,c2,closure_induction_2
c4: all(n:CURRENT) n in p  c3
ensure
all(n:CURRENT) e  l1,c4
end
Range of the successor function
We claim that the range of the successor function contains all natural numbers
except zero.
range:
all
ensure
succ.range = {n: n/=0}  lemma_range
end
In order to convert this into a valid proof we have to prove that succ.range
and {n:n/=0}
are the same set. Two sets are the identical if they contain
the same elements i.e. we have to prove all(n) n in {n:n/=0} = n in
. Since this is a statement about all natural numbers we prove this
succ.range
assertion by induction (Note that n in {x:e} = e[x:=n]
i.e. n in {n:n/=0} =
).
n/=0
lemma_range:
all(n:CURRENT)
check
c1: 0 /in succ.range  zero_not_succ
c2: (0/=0) = 0 in succ.range  c1
c3: all(n:CURRENT)
require
(n/=0) = n in succ.range
check
c4: n.succ /= 0  zero_not_succ
c5: n.succ in succ.range  trivial
ensure
(n.succ/=0) = n.succ in succ.range  c4,c5
end
ensure
(n/=0) = n in succ.range  c2,c3,induction
end
Infinity
One of the immediate consequences of the basic definitions is that the set of
natural numbers must be infinite. We can see this by the following reasoning.
Since the successor function is defined as a total function (no preconditions)
its domain is the set of all natural numbers.
succ.domain = (1:CURRENT?)
In the previous chapter we have proved succ.range = {n:n/=0}
. This implies
that the range of the successor function is a proper subset of its domain.
succ.range < succ.domain
Because of the axiom succ_injective
the successor function is injective
succ.is_injective
From this we can conclude that the set of natural numbers is
infinite. Remember the definition of infiniteness of a set: A set p
is
infinite if there is an endofunction f
whose domain is the set p
and
whose range is a proper subset of its domain. The successor function is such a
function for the natural numbers.
I.e. we get
(0).closed(succ).is_infinite
and because of closed
infinite: (1:CURRENT?).is_infinite
Predecessor function
Every injective function f
has an inverse function g=f.inverse
such that
f.domain=g.range
and f.range=g.domain
. The successor function is an
injective function. The range of the successor function is
{n:n/=0}
. Therefore the following predecessor function is uniquely defined.
pred(n:CURRENT): CURRENT
require
n /= 0
deferred
ensure
Result = (succ.inverse)(n)
end
Order relation
We define an order relation on natural numbers by defining n<=m
if and only
if the number m
can be reached by starting at the number n
and applying
the successor function zero or more times.
<= (n,m:CURRENT): BOOLEAN
deferred
ensure
Result = m in n.closed(succ)
end
all(a,b:CURRENT)
ensure
(<=).is_reflexive  consequence of closure
(<=).is_transitive  consequence of closure
a<=b => b<=a => a=b  lemma_anti (see below)
a<=b or b<=a  lemma_linear (see below)
end
The reflexivity and transitivity of the relation <=
are direct consequences
of its definition as a closure. The proofs of the antisymmetry and the
linearity of <=
need a little bit more reasoning. In order to prove these
properties we need some definitions and laws given in the article
“Endofunctions, closures, cycles and chains”.
Let A
be any type.
is_connected(p:A?, f:A>A): ghost BOOLEAN
 Is the set p connected under the function f?
ensure
Result = all(a,b)
require
{a,b}<=p
ensure
b in a.closed(f) or a in b.closed(f)
end
end
is_cycle(p:A?, f:A>A): ghost BOOLEAN
 Does the set p form a cycle under f?
ensure
Result = some(a)
a.closed(f) = p
and a in f.domain
and a in f(a).closed(f)
end
has_cycle(p:A?, f:A>A): ghost BOOLEAN
 Has the set p a subset which forms a cycle under f?
ensure
Result = some(q:A?) q<=p and q.is_cycle(f)
end
is_chain(p:A?, f:A>A): ghost BOOLEAN
 Is the set p a chain under f?
ensure
Result = (p.is_closed(f)
and p.is_connected(f)
and not p.has_cycle(f))
end
With these definitions the following laws have been derived within the article
“Endofunctions, closures, cycles and chains”:
all(a:A, f:A>A)
ensure
connected: a.closed(f).is_connected(f)
infinite_chain:
a.closed(f).is_infinite => a.closed(f).is_chain(f)
end
Having these laws it is easy to prove the linearity of the order relation.
lemma_linear:
all(a,b:CURRENT)
check
c1: (0).closed(succ).is_connected(succ)  connected
c2: b in a.closed(succ) or a in b.closed(succ)
 c1, def is_connected
ensure
a<=b or b<=a  c2
end
The antisymmetry of the order relation requires all(a,b) a<=b => b<=a =>
. We prove this law by contradiction and assume that
a=ba/=b
is
inconsistent with the assertions a<=b
and b<=a
. The inequality a/=b
implies that the set of natural numbers contained a cycle. This contradicts
the fact that the natural numbers form a chain which cannot contain a cycle.
lemma_anti:
all(a,b:CURRENT)
require
r1: a<=b
r2: b<=a
check
c1: require
r3: a/=b
check
c2: b in a.closed(succ)  r1
c3: a in b.closed(succ)  r2
c4: b in a.succ.closed(succ)  c2,r3
c5: a in a.succ.closed(succ)  c3,c4
c6: a.closed(succ).is_cycle(succ)  c5
c7: a.closed(succ)<=(0).closed(succ)  closed
c8: (0).closed(succ).has_cycle(succ)  c6,c7
c9: (0).closed(succ).is_infinite  infinite,closed
c10: (0).closed(succ).is_chain(succ)  c9,infinite_chain
c11: not (0).closed(succ).has_cycle(succ)
 c10,def chain
ensure
false  c8,c11
end
ensure
a=b  c1
end
Wellorder
We claim that the order relation is a wellorder i.e. each nonempty set p
has
a minimal element.
wellorder:
all(p:CURRENT?)
require
p /= 0
ensure
some(n) n.is_least(p)
end
Before proving this theorem we first prove the related theorem all(n:CURRENT)
which says that for
all(p:CURRENT?) p*{m:m<=n}/=0 => some(m) m.is_least(p)
all natural numbers n
and for all sets p
the nonemptiness of the
intersection of p
with the downward closure of n
implies that there is a
least element of p
. Since this is a statement about all natural number we
can use induction to proof it.
lemma_wo:
all(n:CURRENT, p:CURRENT?)
check
c1: require
r1: p*{m:m<=0} /= 0
check
c2: 0 in p  r1
ensure
some(m) m.is_least(p)  c2, witness 0
end
c3: all(n:CURRENT)
require
r2: p*{m:m<=n}/=0 => some(m) m.is_least(p)
r3: p*{n:m<=n.succ}/=0
check
c4: p*{m:m<=n}=0 or p*{m:m<=n}/=0
c5: require
r4: p*{m:m<=n}=0
check
c6: n.succ in p  r3,r4
c7: n.succ.is_least(p)  c6,r4
ensure
some(m) m.is_least(p)  c7, witness n.succ
end
ensure
some(m) m.is_least(p)  c4,c5,r2
end
ensure
p*{m:m<=n}/=0 => some(m) m.is_least(p)
end
Having this we can prove the wellorder theorem.
wellorder:
all(p:CURRENT?)
require
r1: p /= 0
check
c1: some(n:CURRENT) n in p
c2: some(n:CURRENT) p*{m:m<=n}/=0  c1
c3: all(n:CURRENT)
require
r2: p*{m:m<=n}/=0
ensure
some(m) m.is_least(p)  r2, lemma_wo
end
ensure
some(n) n.is_least(p)  c2,c3
end
Recursive functions
Examples of recursive functions on natural numbers
Let us look at some primitive recursive functions on natural numbers. First we
can define addition of two natural numbers n+m
. We use a definition
which is recursive in the first argument (an equivalent definition being
recursive in the second argument is possible as well).
+ (n,m:CURRENT): CURRENT
 The sum of the numbers n and m.
deferred
ensure
Result = if n=0 then m
else (n.pred+m).succ
end
end
Then we can define multiplication of two natural number n*m
.
* (n,m:CURRENT): CURRENT
 The product of the numbers n and m.
deferred
ensure
Result = if n=0 then 0
else (n.pred*m) + m
end
end
As a third typical primitive recursive function we define n^m
which
represents the number n
raised to the m
th power.
^ (n,m:CURRENT): CURRENT
 The number n raised to the mth power.
deferred
ensure
Result = if m=0 then 1
else
n^(m.pred) * n
end
end
Transformation into a general form
Now we want to transform the definition of a recursive function into the
general form
gr(n:CURRENT): G
ensure
Result = if n=0 then c
else h(gr(n.pred),n)
end
end
where
c: CURRENT>G
h: [G,CURRENT]>G
Let us look at the function +
+ (n,m:CURRENT): CURRENT
deferred
ensure
Result = if n=0 then m  (m>m)(m)
else (n.pred+m).succ  (m>(n.pred+m).succ)(m)
end
end
to derive the transformation.
The function gr
is a function of one argument and the function +
has two
arguments. Therefore the result type G
of the function gr
has to be a
function of type CURRENT>CURRENT
so that n+m = gr(n)(m)
i.e. the function
gr
is the curried version of +
. If we uncurry the definition of gr
we
get the generic form
gr2(n,m:CURRENT): CURRENT
ensure
Result = if n=0 then c(m)
else h((m>gr2(n.pred,m)),n)(m)
end
end
 where
gr(n.pred) = (m>gr2(n.pred,m))
If we match the definition of +
with the generic definition of gr2
we get
the following correspondences:
c = (m > m)
h = ([g,n] > m > g(m).succ)
For the functions *
and ^
we get the following:
* (n,m:CURRENT): CURRENT
deferred
ensure
Result = if n=0 then 0
else (n.pred*m) + m
end
end
c = (m > 0)
h = ([g,n] > m > g(m) + m)
^ (n,m:CURRENT): CURRENT  '^' is recursive in the second argument!!
deferred
ensure
Result = if m=0 then 1
else
n^m.pred * n
end
end
c = (n > 1)
h = ([g,m] > n > g(n) * n)
 Note: because '^' is recursive in the second argument we get
 gr2(m,n) = n^m !!
Functional of a recursive function
Definition
The general definition of a (primitive) recursive function on natural numbers
looks like:
gr(n:CURRENT): G
ensure
Result = if n=0 then c
else h(gr(n.pred),n)
end
end
with c:G
and h:[G,CURRENT]>G
where h
is a total function. From this
definition we extract the functional f
f(g:CURRENT>G): CURRENT>G
ensure
Result = (n > if n=0 then c
else h(g(n.pred),n)
end)
end
so that the function gr
is a fixpoint of the functional f
.
gr = f(gr)  gr is fixpoint of f
The functional f
depends only on c
and h
. Therefore we define a function
functional
which given c
and h
returns the functional.
functional(c:G, h:[G,CURRENT]>G): (CURRENT>G)>(CURRENT>G)
require
h.is_total
ensure
Result = (g > n > if n=0 then c
else h(g(n.pred),n)
end)
end
Domain transformation
The functional f=functional(c,h)
transforms the domain of any function
g:CURRENT>G
according to the formula f(g).domain = {0} +
. I.e. zero is contained in
g.domain.image(succ)f(g).domain
as well as all
elements of g.domain
shifted one up. We prove this claim by the following
reasoning:
fdtrans:
all(c:G, h:[G,CURRENT]>G, f:(CURRENT>G)>(CURRENT>G), g:CURRENT>G)
require
r1: f = functional(c,h)
r2: h.is_total
check
c1: g.domain.image(succ) = {n: some(m) m.succ = n and m in g.domain}
 def image
c2: g.domain.image(succ) = {n: n/=0 and n.pred in g.domain}
 c1, def pred
c3: f(g).domain = {0} + {n: n/=0 and n.pred in g.domain}
 r1, def functional
ensure
f(g).domain = {0} + g.domain.image(succ)  c3,c2
end
Monotonicity
Any functional f=functional(c,h)
is monotonic i.e. for all pairs of
functions a,b:CURRENT>G
with a<=b
we get f(a)<=f(b)
. Note that the
category of functions of type CURRENT>G
forms a complete partial order. The
relation a<=b
states that the domain of a
is a subset of the domain of
b
and that a
and b
restricted to the domain of a
(i.e. ba.domain
)
are the same function.
We give a formal prove of the monotonicity of the functional f
.
fmono:
all(c:G, h:[G,CURRENT]>G, f:(CURRENT>G)>(CURRENT>G))
require
r1: h.is_total
r2: f = functional(c,h)
check
c1: all(a,b:CURRENT>G)
require
r1: a <= b
check
c2: a.domain <= b.domain  r1
c3: {0} + a.domain.image(succ) <= {0} b.domain.image(succ)
 c2
c4: f(a).domain <= f(b).domain  c3,fdtrans
c5: all(n:CURRENT)
require
r2: n in f(a).domain
check
c6: n in f(b).domain
c7: n=0 or n/=0
c8: f(a)(0) = f(b)(0)  = c
c9: require
r3: n/=0
check
c10: n.pred in a.domain  r2
c11: n.pred in b.domain  c10,c2
c12: a(n.pred)=b(n.pred)  r1,c10,c11
c13: f(a)(n) = h(a(n.pred),n)  def f
c14: f(b)(n) = h(b(n.pred),n)  def f
ensure
f(a)(n) = f(b)(n)  c12,c13,c14
end
ensure
f(a)(n) = f(b)(n)  c7,c8,c9
end
c15: f(a) = f(b)f(a).domain  c4,c5
ensure
f(a) <= f(b)  c4,c15
end
ensure
f.is_monotonic
end
Continuity
We claim that the functional f=functional(c,h)
is continuous. Continuity
requires that the suprema of directed sets are maintained. I.e. if d
is a
directed set and s=d.supremum
its supremum then we have to prove that
d.image(f).supremum = f(s)
.
Since f
is monotonic it is guaranteed that d.image(f)
is a directed set
and that upper bounds of all sets are mapped to upper bounds. This implies
d.image(f) <= f(s)
.
In order to prove that f(s)
is the least upper bound of d.image(f)
we show
that the assumption of another upper bound g
with d.image(f)<=g
and
g<f(s)
leads to a contradiction.
If there exists such an upper bound g
then there has to be one element n
in the domain of f(s)
which is not in the domain of g
. In the case n=0
the contradiction is evident because all functions in d.image(f) have zero in
their domain and therefore g
cannot be an upper bound. In the case n/=0
we
get n.pred in s.domain
because n in f(s).domain
. This implies that there
has to be one function a
within d
so that n.pred in a.domain
otherwise
s
would not be a supremum. This implies that there is another function a in
so that
d.image(f)n in a.domain
. Therefore n
has to be in the domain of
g
because g
is an upper bound of d.image(f)
. This contradicts the fact
that n /in g.domain
.
fconti:
all(c:G, h:[G,CURRENT]>G, f:(CURRENT>G)>(CURRENT>G))
require
r1: h.is_total
r2: f = functional(c,h)
check
c1: all(d:(CURRENT>G)?, s:CURRENT>G)
require
r3: d.is_directed
r4: s = d.supremum
check
c2: d <= s  r4
c3: d.image(f) <= f(s)  c2, fmono
c4: require
r5: some(g:CURRENT>G)
d.image(f)<=g and g<f(s)
ensure
false  contra_fconti (see below)
end
c5: all(g:CURRENT>G)
d.image(f)<=g => f(s)<=g
 c4
ensure
d.image(f).supremum = f(s)  c3,c5
end
ensure
f.is_continuous
end
contra_fconti:
all(c:G, h:[G,CURRENT]>G,
f:(CURRENT>G)>(CURRENT>G),
d: (CURRENT>G)?, s,g:CURRENT>G,
)
require
r1: h.is_total
r2: f = functional(c,h)
r3: d.is_directed
r4: s = d.supremum
r5: d.image(f) <= g
r6: g < f(s)
check
c1: some(n:CURRENT) n in (f(s).domaing.domain)  r6
c2: all(n:CURRENT)
require
r7: n in f(s).domain
r8: n /in g.domain
check
c3: all(a) a in d.image(f) => 0 in a.domain  fdtrans
c4: 0 in g.domain  c3,r5
c6: n=0 or n/=0
c7: n=0 => n in g.domain and n /in g.domain  c4,r8
c8: require
r9: n/=0
check
c9: n.pred in s.domain  r7,r9,fdtrans
c10: some(a:CURRENT>G)
a in d and n.pred in a.domain
 c9,r4
c11: some(a:CURRENT>G)
a in d.image(f) and n in a.domain
 c10,fdtrans
c12: n in g.domain  c11,r5
ensure
false  c12,r8
end
ensure
false  c6,c7,c8
end
ensure
false  c1,c2
end
Continuous functions and least fixpoints
We cite the central fixpoint law from the article “Closures and fixpoints”:
Whenever an endofunction f
on a complete partial order is continuous and
there is an element a
which is a prefixpoint of f
and the set
a.closed(f)
and its supremum are completely in the domain of f
then
a.closed(f).supremum
is the least fixpoint above a
(Note that
a.closed(f)
is a chain and is therefore directed so that the supremum
exists).
CPO: COMPLETE_PARTIAL_ORDER
least_fixpoint:
all(a,s:CPO, f:CPO>CPO)
require
f.is_continuous
a in f.prefixpoints
s = a.closed(f).supremum
a.closed(f) + {s} <= f.domain
ensure
s.is_least(f.fixpoints * {x:a<=x})
end
We can apply this theorem to the functions of type CURRENT>G
and the
functional f=functional(c,h)
.
Since the functions form a complete partial order and the completely undefined
function 0
is the least function within this order we get that 0
is a
prefixpoint of the functional f
and (0).closed(f).supremum
is the least
fixpoint of the functional f
.
Unique fixpoint
From the least_fixpoint
theorem it follows that the supremum s
with
s=(0).closed(f).supremum
is the least fixpoint of a functional of the form
f=functional(c,h)
.
We claim that the supremum s
is a unique fixpoint of the functional
f
. We prove this claim by showing that s
is a total function. If s
is a
total function then there is no function above s
i.e. there cannot be any
fixpoint above s
(and there is no fixpoint below s
because s
is the
least fixpoint).
In order to demonstrate that s
is a total function we look at the functions
in the closure (0).closed(f)
. For each natural number n
there is an
element in the closure which has n
in its domain. We proof this by induction
on n
(see below). If this is the case then all natural numbers n
must be
in the domain of the supremum s
as well. Otherwise s
were not an upper
bound of (0).closed(f)
.
all(n:CURRENT,
c:G, h:[G,CURRENT]>G,
f:(CURRENT>CURRENT)>CURRENT>CURRENT)
require
r1: f = functional(c,h)
check
c1: f(0) in (0).closed(f)
c2: 0 in f(0).domain
c3: all(n:CURRENT)
require
r2: some(g) g in (0).closed(f) and n in g.domain
check
c4: all(g:CURRENT>G)
require
r3: g in (0).closed(f)
r4: n in g.domain
check
c5: f(g) in (0).closed(f)  f is total
c6: f(g).domain
= {0}+g.domain.image(succ)  fdtrans
c7: n.succ in f(g).domain  r4,c6
ensure
some(g)
g in (0).closed(f)
and n.succ in g.domain  c5,c7, witness f(g)
end
ensure
some(g)
g in (0).closed(f)
and n.succ in g.domain  r2,c4
end
ensure
some(g:CURRENT>G)
g in (0).closed(f)
and n in g.domain  c1,c2,c3, induction
end