# Introduction

## Motivation

Endofunctions are functions f of type A->A where A can be any type. Since all

functions are partial functions we can use endofunctions to model linked

structures. E.g. if we have an object which has an optional reference to an

object of the same type the optional reference can be viewed as a partial

function f of type A->A. If the reference to the next object is void (there is

no next object because we are at the end of a linked list or we have reached

the root of a tree following the parent links) then the corresponding function

f is undefined for this specific object.

## Sequences and closures

If we have an element a of type A and an endofunction f of type A->A we can

start at the element a, apply the function to a (if a is in the domain of the

function) getting f(a), reapply the function to f(a) (provided that f(a) is in

the domain of f), … I.e. we get the set

{a, f(a), f(f(a)), ... }

We call a set p of elements of type A closed under f if the image of p under f

is a subset of p, i.e. f applied to any element of p results in an element

within p. I.e. we define the predicate

is_closed(p:A?, f:A->A): ghost BOOLEAN -- Is the set `p' closed under the function `f'? ensure Result = p.image(f) <= p end

and remember the definition of image as

image(p:A?, f:A->B): ghost B? -- The image of the set `p' under `f'. ensure Result = {b: some(a) a in p and a in f.domain and f(a) = b} end

With this we get an equivalent definition of a closed set as

all(p:A?, f:A->A) ensure p.is_closed(f) = all(x:A) require x in p x in f.domain ensure f(x) in p end end

The proof of the equivalence of both definitions is a standard exercise.

The set of all sets which are closed under an endofunction f form a closure

system. Therefore we can close any set p under a function f by finding the

least set which is closed under f and contains the set p.

closed(p:A?, f:A->A): ghost A? -- The set `p' closed under the function `f'. ensure Result = {q:A?: q.is_closed(f) and p<=q}.infimum end

Since the set {q: q.is_closed(f)} is a closure system the above used infimum

is guaranteed to be closed under f (for details on closures see the article

“Complete lattices and closure systems”). We often need the closure of the

singleton set {a} under f and therefore define the closure of an element a by

closed(a:A, f:A->A): ghost A? -- The singleton set {a} closed under the function `f'. ensure Result = {a}.closed(f) end

With this definition we can write the above set in a closed form

a.closed(f) = {a, f(a), f(f(a)), f(f(f(a))), ... }

The function ‘closed’ is a closure operator, i.e. it is monotonic, ascending

and idempotent on the first argument.

all(p,q:A?, f:A->A) ensure monotonic: p <= q => p.closed(f) <= q.closed(f) ascending: p <= p.closed(f) idempotent: p.closed(f) = p.closed(f).closed(f) end

Furthermore the function closed is monotonic in the function argument

all(a:A, p:A?, f,g:A->A) ensure f <= g => p.closed(f) <= p.closed(g) f <= g => a.closed(f) <= a.closed(g) end -- Note: f<=g iff f.domain <= g.domain and the values of f and g -- coincide on f.domain

## Induction

Since p.closed(f) is the least set which contains all elements of p and is

closed under f all other sets which contain p and are closed under f must be

supersets of p.closed(f). We can use this property of the closure to prove

that all elements of a closure x satisfy a certain property e. In order to do

this we put all elements which satisfy e into the set q = {x: e}. If we can

prove that the initial set p is a subset of q and q is closed under f then we

can conclude that all p.closed(f) is a subset of q i.e. that all elements of

p.closed(f) satisfy the property e.

induction: all(p,q:A?, f:A->A) require p <= q q.is_closed(f) ensure p.closed(f) <= q end

This theorem is a direct consequence of the fact that the function closed is

monotonic, ascending and idempotent.

We can use a similar induction law if the start set is the singleton set {a}.

induction: all(a:A, q:A?, f:A->A) require a in q q.is_closed(f) ensure a.closed(f) <= q end

## Cycles and chains

If we start from an element a and repeatedly apply f forever or until we reach

an out of domain element our intuition tells us that there are three

possibilities. Either we can continue reapplying f forever without reaching an

out of domain element and without reaching an element which has already been

passed or we reach some out of domain element or we reach an element which we

have already passed.

infinite chain: a -> b -> c -> .... finite chain: a -> b -> c -> .... -> z z /in f.domain with cycle: a -> b -> c -> .... -> z ^ / \........../

In order to deal with these structures we introduce the following definitions.

is_cycle(p:A?, f:A->A): ghost BOOLEAN -- Does the set `p' form a cycle under the function `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 -- Does the set `p' contain a cycle under `f'? ensure Result = some(a) a in p and a.closed(f).is_cycle(f) end is_connected(p:A?, f:A->A): ghost BOOLEAN -- Is the set `p' connected under `f'? ensure Result = all(x,y:A) require {x,y} <= p ensure x in y.closed(f) or y in x.closed(f) end end is_chain(p:A?, f:A->A): ghost BOOLEAN -- Does the set `p' form a chain under `f'. ensure Result = (p.is_closed(f) and p.is_connected(f) and not p.has_cycle(f)) end

# Simple properties

## Predecessor

In any closure of the form p.closed(f) it is guaranteed that

all elements except the elements of the initial set have predecessors within

the closure.

In order to prove this claim we assume the opposite that for a certain element

x in p.closed(f)-p all elements a of p.closed(f) are not predecessors of

x. Since x has no predecessor we can prove that the set p.closed(f)-{x} is

closed under f and contains p. This set is strictly smaller than p.closed(f)

which contradicts the fact that p.closed(f) is the least set which contains p

and is closed under f.

some_predecessor: all(x:A, p:A?, f:A->A) require r1: x in p.closed(f)-p check c1: require r2: all(a) a in p.closed(f) => a in f.domain => f(a)/=x check c2: all(a:A) require r3: a in p.closed(f)-{x} r4: a in f.domain check c3: a in p.closed(f) -- r3 c4: a /= x -- r3 c5: f(a) /= x -- c3,r4,r2 c6: f(a) in p.closed(f) -- c3,r4 ensure f(a) in p.closed(f)-{x} -- c5,c6 end c7: p <= p.closed(f)-{x} -- r1 c8: (p.closed(f)-{x}).is_closed(f) -- c2 c9: p.closed(f) <= p.closed(f)-{x} -- closure is least c10: x in p.closed(f)-{x} -- r1,c9 c11: x /in p.closed(f)-{x} -- general law ensure False -- c10,c11 end ensure some(a) a in p.closed(f) and a in f.domain and f(a)=x end

## All elements of cycles

By definition the set p is a cycle under f if there is one element a in the

domain of f such that p=a.closed(f) and a is in f(a).closed(f).

We claim that all elements of a cycle satisfy this property. We prove this

with a two step approach. First we prove the lemma that each element of a

cycle transfers this property to its successor f(a). Then we use induction to

prove that all elements of a.closed(f) and therefore all elements of p have

this property.

feature {NONE} lemma: all(a:A, p:A?, f:A->A) require r1: a.closed(f) = p r2: a in f.domain r3: a in f(a).closed(f) check c1: f(a).closed(f) <= a.closed(f) -- general property c2: a.closed(f) <= f(a).closed(f) -- r3, closure is monotonic c3: a = f(a) or a /= f(a) c4: require r4: a /= f(a) check c5: {f(a)} < f(a).closed(f) c6: a in (f(a).closed(f)-{f(a)}) -- r3,r4 c7: f(a).closed(f) - {f(a)} <= f(f(a)).closed(f) -- general property of closure ensure f(a) in f.domain -- c5 a in f(f(a)).closed(f) -- c6,c7 end ensure f(a).closed(f) = p -- r1,c1,c2 f(a) in f.domain -- c3,c4,r2 f(a) in f(f(a)).closed(f) -- c3,c4,r3 end

Having this lemma it is easy to prove that all elements of a cycle under f are

in the domain of f and their closure is the cycle and they can be reached by

their successor.

cycle_all: all(x:A, p:A?, f:A->A) require r1: p.is_cycle(f) r2: x in p local r3: q = {x:A: x.closed(f)=p and x in f.domain and x in f(x).closed(f)} check c1: some(a:A) a.closed(f)=p and a in f.domain and a in f(a).closed(f) -- r1 c2: all(a:A) require r4: a.closed(f) = p r5: a in f.domain r6: a in f(a).closed(f) check c3: a in q -- r3,r4,r5,r6 c4: q.is_closed(f) -- lemma c5: a.closed(f) <= q -- c3,c4 c6: p <= q -- c5,r4 ensure x.closed(f) = p -- r2,c6,r3 x in f.domain -- r2,c6,r3 x in f(x).closed(f) -- r2,c6,r3 end ensure x.closed(f) = p -- c1,c2 x in f.domain -- c1,c2 x in f(x).closed(f) -- c1,c2 end

# Domain restrictions

## Definitions

If f is a function and b is an element of f’s domain then f-b is the function

f without b in its domain. We can subtract a set p from the domain of

f. Furthermore we can restrict the domain of a function. In order to express

these domain restrictions we use the following definitions.

- (f:A->B, p:A?): ghost A->B -- The function `f' without the elements of the set `p' in -- its domain. ensure Result.domain = f.domain - p Result <= f end - (f:A->B, a:A): ghost A->B -- The function `f' without the element `a' in its domain. ensure Result = f - {a} end | (f:A->B, p:A?): ghost A->B -- The function `f' with its domain restricted to `f.domain*p'. ensure Result.domain = f.domain * p Result <= f end

## Out of domain elements are unique

If a closure a.closed(f) has an element which is not in the domain of f then

this element is unique.

out_of_domain_unique: all(a,b,c:A, f:A->A) require {b,c} <= a.closed(f) {b,c} * f.domain = 0 ensure b = c -- lemma below end

Proof: Assume that b and c are different, i.e. there are two out of domain

elements in the closure. We put all objects whose closure contains b and c

into the set p. Clearly a is in the set p. Furthermore the set p is closed

under f. Assume that x is an element of p and in the domain of f. Thus x is

neither b nor c. Therefore f(x).closed(f) must contain b and c as well and is

therefore an element of p. So we have that all elements of a.closed(f) are in

p. This contradicts the fact that b and c are in a.closed(f) which cannot be

in p.

feature {NONE} -- Proof of 'out_of_domain_unique' lemma: all(a,b,c:A, f:A->A) require r1: {b,c} <= a.closed(f) r2: {b,c} * f.domain = 0 r3: b /= c local r4: p = {x:A: {b,c} <= x.closed(f)} check c1: a in p -- r4,r1 c2: all(x:A) require r5: x in p r6: x in f.domain check c3: x /= b -- r6,r2 c4: x /= c -- r6,r2 c5: {b,c} <= f(x).closed(f) -- r5,r4,c3,c4 ensure f(x) in p -- c5 end c6: p.is_closed(f) -- c2 c7: a.closed(f) <= p -- c1,c6 c8: b /in p -- r4,r2,r3 c9: b /in a.closed(f) -- c8,c7 c10: b in a.closed(f) -- r1 ensure False -- c9,c10 end end

## Sequencing

If we have a closure of the form a.closed(f) and two elements b and c within

this closure then starting from a we either first encounter b or c. This

intuitively clear fact can be expressed by the claim

sequence: all(a,b,c:A, f:A->A) require {b,c} <= a.closed(f) ensure b in a.closed(f-c) or c in a.closed(f-b) end

We prove this claim by a series of intermediate lemmas.

First we show that all b in the closure a.closed(f) are also in the closure of

a.closed(f-b) (f-b is the function f with b removed from its domain). We prove

this claim by contradiction.

sequence_1: all(a,b:A, f:A->A) require r1: b in a.closed(f) check c1: require r2: b /in a.closed(f-b) check c2: b in f.domain or b /in f.domain c3: require r3: b in f.domain check c4: a.closed(f-b) = a.closed(f-b+{b->f(b)}) -- r2,r3, -- modification of a function outside -- the closure has no effect on the -- closure c5: a.closed(f-b) = a.closed(f) -- c4 c6: b /in a.closed(f) -- r2,c5 ensure False -- r1,c6 end c7: require r4: b /in f.domain check c8: f-b = b c9: b /in a.closed(f) -- r2,c8 ensure False -- r1,c9 end ensure False -- c2,c3,c7 end ensure b in a.closed(f-b) -- c1 end

Next we show that for any c in a.closed(f) and b in a.closed(f-c) that the

closure of a.closed(f-b) is a subset of the closure a.closed(f-c).

sequence_2: all(a,b,c:A, f:A->A) require r1: c in a.closed(f) r2: b in a.closed(f-c) check c1: b=c or b/=c -- first trivial c2: c in f.domain or c /in f.domain -- second trivial c3: require r3: c in f.domain r4: b /= c check c4: b in a.closed(f-c-b) -- r2, sequence_1 c5: c /in a.closed(f-c-b) -- c4, out_of_domain_unique c6: f-b = f-c-b + {c->f(c)} -- r3, general law c7: a.closed(f-c-b) = a.closed(f-b) -- c5,c6,modify_out_of_closure c8: a.closed(f-c-b) <= a.closed(f-c) -- monotonic ensure a.closed(f-b) <= a.closed(f-c) -- c7,c8 end ensure a.closed(f-b) <= a.closed(f-c) -- c1,c2,c3 end

Consider an element b and an element c which is not in the closure

a.closed(f-b). From this we can conclude that a.closed(f-b) is a subset of

a.closed(f-c).

sequence_3: all(a,b,c:A, f:A->A) require r1: c /in a.closed(f-b) check c1: a.closed(f-b) = a.closed(f-b-c) -- r1 c2: a.closed(f-b) = a.closed(f-c-b) -- c1 c3: a.closed(f-c-b) <= a.closed(f-c) -- monotonic ensure a.closed(f-b) <= a.closed(f-c) -- c2,c3 end

From these intermediate lemmas it is easy to prove the main theorem.

sequence_4: all(a,b,c:A, f:A->A) require r1: {b,c} <= a.closed(f) check c1: require r2: c /in a.closed(f-b) check c2: a.closed(f-b) <= a.closed(f-c) -- r1, r2, sequence_3 c3: b in a.closed(f-b) -- r1, sequence_1 ensure b in a.closed(f-c) -- c3,c2 end ensure b in a.closed(f-c) or c in a.closed(f-b) -- c1 end

# Cycles

In this chapter we concentrate on closures which have cycles or which are a

cycle.

## Two cycles are identical or disjoint

If we have two sets p and q which form a cycle under f then they are either

identical or disjoint.

cycle_disjoint_or_identical: all(p,q:A?, f:A->A) require r1: p.is_cycle(f) r2: q.is_cycle(f) check c1: require r3: p*q /= 0 check c2: some(a:A) a in p and a in q -- r3 c3: all(a:A) require r4: a in p r5: a in q check c4: p = a.closed(f) -- r4,r1,cycle_all c5: q = a.closed(f) -- r5,r2,cycle_all ensure p = q -- c4,c5 end ensure p = q -- c2,c3 end ensure p*q=0 or p=q -- c1 end

## Cycles are unique

A closure of the form a.closed(f) cannot have two different cycles.

cycle_unique: all(a:A, p,q:A?, f:A->A) require r1: p.is_cycle(f) r2: q.is_cycle(f) r3: p <= a.closed(f) r4: q <= a.closed(f) check c1: require r5: p /= q local r6: s = {a:A: not a.closed(f).is_cycle(f) and p+q<=a.closed(f)} check c2: p*q = 0 -- r1,r2,r5,cycle_disjoint_or_identical c3: not a.closed(f).is_cycle(f) -- r1,r2,r5,r3,r4 if a.closed(f) were a -- cycle it would have to be identical to -- p and q which contradicts r5 c4: a in s -- c3,r3,r4 c5: all(x:A) require r7: x in s r8: x in f.domain check c6: x /in p -- r7,r6,r1 c7: x /in q -- r7,r6,r2 c8: p+q <= f(x).closed(f) -- c6,c7 c9: not f(x).closed(f).is_cycle(f) -- if it were a cycle it would have to be -- identical to p and q which contradicts r5 ensure f(x) in s -- c8,c9 end c10: s.is_closed(f) -- c5 c11: a.closed(f) <= s -- c4,c10 c12: not p.is_cycle(f) -- c11,r3 ensure False -- r1,c12 end ensure p = q -- c1 end

## All elements of a cycle have predecessors

In some previous chapter we have already proved that each element in

a.closed(f) except a is guaranteed to have a predecessor. In a cycle each

element is guaranteed to have a predecessor.

cycle_all_predecessor: all(p:A?, f:A->A) require r1: p.is_cycle(f) check c1: all(y:A) require r2: y in p check c1: y in f.domain -- r1,r2 c2: y in f(y).closed(f) -- r1,r2,cycle_all c3: f(y).closed(f)=p -- r1,r2,cycle_all c4: y=f(y) or y/=f(y) c5: y=f(y) => some(x) x in p and f(x)=y -- witness y c6: y/=f(y) => some(x) x in p and f(x)=y -- c2,c3,some_predecessor ensure some(x:A) x in p and f(x)=y -- c4,c5,c6 end ensure all(y) y in p => some(x) x in p and f(x)=y -- c1 end

## All elements of a cycle have unique predecessors

If the set p is a cycle under f we claim that each element in p has a unique

predecessor. In order to prove this claim we assume that a, b and c are three

elements of the cycle where b and c are different predecessors of a and lead

this to a contradiction. As a first step we assume additionally that b is in

a.closed(f-c).

Since a, b and c are elements of the cycle they are in the domain of f. b and

c are different therefore b is in the domain of f-c, i.e (f-c)(b)=a because b

is a predecessor of a. Together with the additional assumption that b is in

a.closed(f-c) we get that b is in (f-c)(b).closed(f-c) which is sufficient to

conclude that b.closed(f-c) is a cycle and therefore that a.closed(f-c) is a

cycle as well. From the lemma ‘sequence_1 we can conclude that c is in

a.closed(f-c). In a cycle all elements are in the domain of the function,

therefore c must be in the domain of f-c which contradicts the definition of

f-c.

feature {NONE} lemma: all(a,b,c:A, f:A->A) require r1: a.closed(f).is_cycle(f) r2: {b,c} <= a.closed(f) r3: f(b) = a r4: f(c) = a r5: b in a.closed(f-c) check c1: require r7: b /= c check c2: b in (f-c).domain -- r1,r2,r7 c3: (f-c)(b)=a -- c2,r3 c4: b in (f-c)(b).closed(f-c) -- c3,r5 c5: b.closed(f-c).is_cycle(f-c) -- c4 c6: a.closed(f-c).is_cycle(f-c) -- c5,c3 c7: c in a.closed(f-c) -- r2,sequence_1 c8: c in (f-c).domain -- c6,c7,cycle_all c9: c /in (f-c).domain -- by definition ensure False -- c8,c9 end ensure b = c end end

Having this lemma we can prove that every element of a cycle has a unique

predecessor.

cycle_unique_predecessor: all(p:A?, f:A->A) require r1: p.is_cycle(f) check c1: all(a,b,c:A) require r2: {a,b,c} <= p r3: f(b) = a r4: f(c) = a check c2: a.closed(f) = p -- r1,r2,cycle_all c3: {b,c} <= a.closed(f) -- c2,r2 c4: b in a.closed(f-c) or c in a.closed(f-b) -- c3,sequence ensure b = c -- c4,r2,r3,r4,lemma end ensure all(a,b,c) {a,b,c} <= p => f(b)=a => f(c)=a => b=c end

As a corollary we get the fact that if the set p is a cycle under f then f is

injective on p.

cycle_injective: all(p:A?, f:A->A) require r1: p.is_cycle(f) check c1: all(b,c:A) require r2: {b,c} in (f|p).domain r3: f(b) = f(c) check c2: p <= f.domain -- r1 c3: (f|p).domain = p -- c2 c4: {b,c} <= p -- r2,c3 ensure b = c -- r2,r3,c4, -- cycle_unique_predecessor end ensure (f|p).is_injective end -- Note: f|p is the function f restricted to the domain -- f.domain*p

## Closures with cycles are completely in the domain

If a closure a.closed(f) has a cycle then it is guaranteed that all elements

of the closure are within the domain of f. This claim is easy to prove. We put

all elements of f.domain whose closure has a cycle into the set p and show that

a is in p and that p is closed under f.

The element a is in p because a.closed(f) has a cycle. Therefore either

a is in the cycle and is therefore in f.domain or it is not in the cycle. If

it is not in the cycle and not in the domain then a.closed(f) could not

contain a cycle.

Assume an arbitrary element x of p i.e. x is in f.domain and x.closed(f) has a

cycle. Since x.closed(f) has a cycle f(x).closed(f) has a cycle as well. Now

either f(x).closed(f) is a cycle. Then f(x) is in p as well. Or f(x).closed(f)

is not a cycle. Then f(x) must be in f.domain otherwise it could not contain a

cycle.

cycles_in_domain: all(a:A, f:A->A) require r1: a.closed(f).has_cycle(f) local r2: p = f.domain * {x:A: x.closed(f).has_cycle(f)} check c1: a in f.domain -- r1 c2: a in p -- c1,r2 c3: all(x:A) require r3: x in p r4: x in f.domain check c4: x.closed(f).has_cycle(f) -- r3,r2 c5: f(x).closed(f).has_cycle(f) -- c4 c6: f(x).closed(f).is_cycle(f) or not f(x).closed(f).is_cycle(f) c7: require r5: f(x).closed(f).is_cycle(f) check c8: f(x) in f.domain ensure f(x) in p -- c8,c5 end c9: require r6: not f(x).closed(f).is_cycle(f) check c10: f(x) in f.domain -- r6,c5 ensure f(x) in p -- c10,c5 end ensure f(x) in p end c11: p.is_closed(f) -- c3 c12: a.closed(f) <= p -- c1,c11 ensure a.closed(f) <= f.domain -- c12,r2 end

# Closures are connected

If we have a closure of the form a.closed(f) we can take any element b of the

closure and form the subclosure b.closed(f). From the properties that ‘closed’

is monotonic, ascending and idempotent it is immediately evident that

b.closed(f) is a subset of a.closed(f).

But there are more properties in subclosures. Suppose we pick two elements b

and c of a.closed(f). Then we claim that either b is in the subclosure

c.closed(f) or c is in the subclosure b.closed(f) i.e. we can reach either b

from c or c from b which says that all elements of the closure are connected.

We are going to prove this claim by induction. But before doing the induction

let us split out the induction step.

Assume that b and c are in a.closed(f) and c is in b.closed(f). Then we prove

that either c is in f(b).closed(f) or f(b) is in c.closed(f).

feature {NONE} lemma: all(a,b,c:A, f:A->A) require r1: {b,c} <= a.closed(f) r2: c in b.closed(f) r3: b in f.domain check c1: b=c or b/=c c2: require r4: b=c check c3: f(b) in c.closed(f) -- r3,r4 ensure c in f(b).closed(f) or f(b) in c.closed(f) -- c3 end c4: require r5: b/=c check c5: c in f(b).closed(f) -- r2,r3,r5 ensure c in f(b).closed(f) or f(b) in c.closed(f) -- c5 end ensure c in f(b).closed(f) or f(b) in c.closed(f) -- c1,c2,c4 end end

Having this lemma we can prove the main theorem.

subclosure: all(a,b,c:A, f:A->A) require r1: {b,c} <= a.closed(f) local r2: p = {b:A: c in b.closed(f) or b in c.closed(f)}*a.closed(f) check c1: a in p -- r2,r1 c2: all(x:A) require r3: x in p r4: x in f.domain check c3: x in a.closed(f) c4: c in x.closed(f) or x in c.closed(f) c5: require r5: c in x.closed(f) check c6: c in f(x).closed(f) or f(x) in c.closed(f) -- r4,r1,c3,r5,lemma ensure f(x) in p -- c3,r2,c6 end c7: require r6: x in c.closed(f) check c8: f(x) in c.closed(f) -- r6,r4 ensure f(x) in p -- c8,c3 end ensure f(x) in p -- c4,c5,c7 end c9: p.is_closed(f) -- c2 c10: a.closed(f) <= p -- c1,c9 ensure c in b.closed(f) or b in c.closed(f) -- c10,r2 end

# Chains

## A chain has an injective function

Whenever we have a set p which is a chain under the function f we can conclude

that f is injective on p.

Remember that a function g is injective if for all pairs x and y in the domain

of g the equality g(x)=g(y) implies x=y. The function g is our function f

restricted to p i.e. f|p. We claim that f|p is injective if p is a chain under

f.

We prove this claim by contradiction. Assume that f|p is not injective. Then

there are x and y in the domain of f|p such that f(x)=f(y) and x/=y. Without

loss of generality we can assume that y is in x.closed(f) (see definition of a

chain).

Since y is in x.closed(f) and x/=y we get y in f(x).closed(f) and therefore y

in f(y).closed(f). This implies that y.closed(f) is a cycle which contradicts

the fact that p is a chain.

In order to keep the proof readable we split out the contradiction as a lemma

and then prove the main theorem.

feature {NONE} lemma: all(p:A?, x,y:A, f:A->A) require r1: p.is_chain(f) r2: {x,y} <= (f|p).domain r3: f(x) = f(y) r4: x /= y r5: y in x.closed(f) check c1: y in f(x).closed(f) -- r5,r4 c2: y in f(y).closed(f) -- c1,r3 c3: y.closed(f).is_cycle(f) -- r2,c2 c4: not y.closed(f).is_cycle(f) -- r2,r1 ensure False -- c3,c4 end end

chain_injective: all(p:A?, f:A->A) require r1: p.is_chain(f) check c1: require r2: not (f|p).is_injective check c2: some(x,y:A) {x,y}<=(f|p).domain and f(x)=f(y) and x/=y -- r2 c3: all(x,y:A) require r3: {x,y} <= (f|p).domain r4: f(x) = f(y) r5: x /= y check c4: y in x.closed(f) or x in y.closed(f) -- r1,r3 c5: y in x.closed(f) => False -- r1,r3,r4,r5,lemma c6: x in y.closed(f) => False -- r1,r3,r4,r5,lemma ensure False -- c4,c5,c6 end ensure False -- c2,c3 end ensure (f|p).is_injective end

## The image of a chain does not contain the first element

Consider a closure a.closed(f) which is a chain under f. The image of the

closure under f does not contain a.

all(a:A, f:A->A) require r1: a.closed(f).is_chain(f) check c1: a in f.domain or a /in f.domain c2: require r2: a in f.domain check c3: a.closed(f) = {a} + f(a).closed(f) -- general law c4: a /in f(a).closed(f) -- r1 c5: f(a).closed(f) = a.closed(f) - {a} -- c3,c4 c6: a.closed(f).image(f) = f(a).closed(f) -- general law ensure a.closed(f).image(f) = a.closed(f) - {a} -- c5,c6 end c7: require r3: a /in f.domain check c8: a.closed(f) = {a} -- r3 c9: {a}.image(f) = 0 -- r3 ensure a.closed(f).image(f) = a.closed(f) - {a} -- c8,c9 end ensure a.closed(f).image(f) = a.closed(f) - {a} -- c1,c2,c7 end

# Finiteness

In this chapter we want to prove the following facts:

– Each chain which has no out of domain elements is infinite.

– Each chain which has an out of domain element is finite.

– Each cycle is finite.

– Each closure which has a cycle is finite.

In this chapter we don’t do all proofs in full formality. Some proofs will be

given with textual arguments only. However it is an easy exercise to

construct the formal proofs.

## Definitions

Let us recall the definition of infiniteness of a set.

is_infinite(p:A?): ghost BOOLEAN -- Is the set `p' infinite? ensure Result = some(f:A->A) f.is_injective and p <= f.domain and p.image(f) < p end

I.e. a set p is infinite if there is an injective map f mapping all elements

of p to a proper subset of p.

A set is finite if it is not infinite.

is_finite(p:A?): ghost BOOLEAN -- Is the set `p' finite? ensure Result = not p.is_infinite end

This gives us an equivalent definition of finiteness.

all(p:A?) ensure p.is_finite = all(f:A->A) require f.is_injective p <= f.domain p.is_closed(f) -- i.e. p.image(f)<=p ensure p = p.image(f) end end

From the definitions we can immediately conclude that the empty set is

finite since there is no proper subset of the empty set (and therefore not any

function mapping to a proper subset).

Furthermore we can prove that p+{a} is a finite set provided that p is a

finite set. Without loss of generality we can analyze the case that the

element a is not in p (if a is in p then p+{a}=p which is a trivial case).

Let’s assume the opposite that p+{a} is infinite. Then there is a injective

function f which maps p+{a} to a proper subset. We analyze the case where a is

in the image and where a is not in the image.

If a is not in the image then (p+{a}).image(f) <= p. This implies p.image(f)<p

because f(a) is missing in the image. Thus p must be infinite which

contradicts the fact that p is finite.

If a is in the image then there is a unique element b in p+{a} with f(b)=a

because of the injectivity of f. We define a new function g which is f with

the values for a and b swapped. g is still injective with g(a)=a and

(p+{a}).image(g)<p+{a}. Thus p.image(g)<p which says that p is infinite and

therefore contradicts the assumption that p is a finite set.

all(a:A, p:A?) require r1: (p+{a}).is_infinite r2: a /in p check c1: all(f:A->A) require r3: f.is_injective r4: p+{a} <= f.domain r5: (p+{a}).image(f) < p+{a} check c2: a /in (p+{a}).image(f) or a in (p+{a}).image(f) c3: require r6: a /in (p+{a}).image(f) check c4: (p+{a}).image(f) <= p -- r5,r6 c5: p.image(f) = (p+{a}).image(f)-{f(a)} -- r2 c6: p.image(f) < p -- c4,c5 ensure p.is_infinite -- r3,r4,c6 end c7: require r7: a in (p+{a}).image(f) local r8: b = (-f)(a) -- -f is the inverse of f r9: g = f <+ {a->f(b),b->f(a)} check c8: g.is_injective -- r3,r9 c9: g(a) = a -- r8,r9 c10: (p+{a}).image(g) < p+{a} -- r5,r9 c11: p.image(g) < p -- c9,c10 c12: p <= g.domain -- r4,r9 ensure p.is_infinite -- c8,c11,c12 end ensure p.is_infinite -- c2,c3,c7 end ensure p.is_infinite -- r1,c1 end

all(a:A, p:A?) require r1: p.is_finite check c1: a in p or a /in p c2: a in p => (p+{a}).is_finite -- trivial c3: require r2: a /in p r3: (p+{a}).is_infinite check c4: p.is_infinite -- r2,r3,previous theorem ensure False -- r1,c4 end ensure (p+{a}).is_finite -- c1,c2,c3 end

## Infinite chains

Let a.closed(f) be a chain under the function f and all elements of the chain

are in the domain of f. This implies that the set p is infinite.

Proof: Since f is an injection on a.closed(f) and a.closed(f) is completely

contained in the domain of f and f maps the chain to a proper subset

(a.closed(f).image(f) does not contain a) we have a witness for the injective

function required in the definition of infiniteness.

all(a:A, f:A->A) require r1: a.closed(f).is_chain(f) r2: a.closed(f) <= f.domain check c1: (f|a.closed(f)).is_injective -- r1 c2: a.closed(f) <= (f|a.closed(f)).domain -- r2 c3: a.closed(f).image(f|a.closed(f)) = a.closed(f).image(f) -- general law c4: a.closed(f).image(f) = a.closed(f)-{a} c5: a.closed(f).image(f) < a.closed(f) -- c4 c6: a.closed(f).image(f|a.closed(f) < a.closed(f) -- c3,c5 c7: some(g:A->A) g.is_injective and a.closed(f) <= g.domain and a.closed(f).image(g) < a.closed(f) -- c1,c2,c6, witness f|a.closed(f) ensure a.closed(f).is_infinite -- c7 end

This theorem implies in the contrapositive that any finite chain of the form

a.closed(f) must have one out of domain element.

all(a:A, f:A->A) require a.closed(f).is_chain(f) a.closed(f).is_finite ensure some(x:A) x in a.closed(f) and x /in f.domain -- contrapositive of the above theorem end

## Finite chains

In the previous chapter we have proved that all finite chains of the form

a.closed(f) must have some out of domain element. In the following we prove

that the existence of an out of domain element in a chain of the form

a.closed(f) is sufficient to conclude that the chain is finite.

We first prove that for all elements x in a.closed(f) the closure

a.closed(f-x) is finite. We do this by induction. We put all elements x with

a.closed(f-x).is_finite into a set p. The start element a is in this set

because a.closed(f-a) is the one element set {a} which is definitely

finite. Now assume that a.closed(f-x) is finite and x is in the domain of

f. The set a.closed(f-f(x)) is equal to the set a.closed(f-x) + {f(x)}. Since

a.closed(f-x) is finite a.closed(f-f(x)) is finite as well and therefore p is

closed under f. Thus for all x in a.closed(f) we have a.closed(f-x) is finite.

Now assume that there is one element e in a.closed(f) which is not in the

domain of f. Therefore f = f-e. Since e is in a.closed(f) we have

a.closed(f-e) is finite and therefore a.closed(f) is finite as well.

## Cycles are finite

Let’s assume that a.closed(f) is a cycle. From this we conclude that a is in

f(a).closed(f) and f(a).closed(f) = a.closed(f) by definition of a cycle. By

induction we can prove that all elements of f(a).closed(f) are in

f(a).closed(f-a). Since f-a <= f and the closure is monotonic in the function

we get the equality f(a).closed(f) = f(a).closed(f-a). Since f(a).closed(f-a)

is a chain with an out of domain element it is finite. Therefore a.closed(f)

is finite as well.

## Closures with cycles are finite

Let’s assume that a.closed(f) has a cycle. Then we claim that a.closed(f) is

finite.

From our intuition we know that there is an element e in a.closed(f) so that

a.closed(f-e) is a chain which contains all elements of a.closed(f). Since a

chain with one out of domain element is finite we can conclude that

a.closed(f) is finite. It remains to be proved that an element e exists within

a.closed(f) such that a.closed(f) = a.closed(f-e).

We prove this claim by contradiction. We assume that for all elements e of

a.closed(f) we have a.closed(f-e) < a.closed(f). We define a set p = {x:

all(e) e in x.closed(f) => x.closed(f-e)<x.closed(f)}. From our assumption we

conclude that a is in this set. Furthermore we can prove that p is closed

under f. Assume an element x in p and in the domain of f. x.closed(f) does not

contain an element e so that x.closed(f-e)=x.closed(f). Since f(x).closed(f)

is a subset of x.closed(f) the same applies to f(x). Therefore f(x) is in p as

well.

But a.closed(f) has a cycle. I.e. there is an element b in a.closed(f) so that

b.closed(f) is a cycle. f is injective on b.closed(f) therefore there is a

unique predecessor e of b which is also in a.closed(f). By the same reasoning

as in the previous chapter we can conclude that b.closed(f-e)=b.closed(f) which

contradicts the assumption that there is no element a.closed(f) which has this

property. Therefore the assumption must be wrong that there is no element e in

a.closed(f) so that a.closed(f-e)=a.closed(f).