# Introduction

Relations are an important vehicle to write specifications. In this article we

study some properties of binary relations. First we start from binary

relations in general with domain, range, composition, images etc.

In the second part we study endorelations i.e. binary relations where the type

of the domain and the range are the same. The most important endorelations are

transitive relations. Transitive relations have a close connection to closure

systems.

All of the presented material in this article is part of the module

`predicate’ because relations are just predicates over tuples i.e. set of

tuples.

# Binary relations

A binary relation between the type G and the type H has the type [G,H]?,

i.e. it is a set of tuples, where the first element is an object of type G and

the second element is an object of type G.

In order to express the basic functions and properties we need some generic

types as placeholders for any type.

feature E,F,G,H: ANY end

## Domain and range

Each relation has a domain (the set of all objects which can serve as a first

component of a pair of the relation) and a range (the set of all objects which

can serve as a second component of a pair of the relation).

domain(r:[G,H]?): ghost G? -- The domain of the relation `r'. ensure Result = {x:G: some(y:H) [x,y] in r} end range(r:[G,H]?): ghost G? -- The range of the relation `r'. ensure Result = {y:H: some(x:G) [x,y] in r} end

## Inverse

For any relation and for each collection of relations we can define a unique

inverse.

feature inverse(r:[G,H]?): [H,G]? -- The inverse of the relation `r'. ensure Result = {y,x: [x,y] in r} end inverse(rr:[G,H]??): [H,G]?? -- The collection of all inverse relations of `rr'. ensure Result = {r: r.inverse in rr} end end

Note that [G,H]? is a set of tuples and [G,H]?? is a set of set of tuples,

i.e. a set of relations.

The function “inverse” is an involution.

inverse_involution: all(r:[G,H]?) check r.inverse.inverse = {y:H,x:G: [x,y] in r}.inverse -- def "inverse" = {x:G,y:H: [x,y] in r} -- def "inverse" = r ensure r.inverse.inverse = r end

The same applies to any collection of relations.

inverse_involution: all(rr:[G,H]??) check rr.inverse.inverse = {r:[H,G]?: r.inverse in rr}.inverse -- def "inverse" = {r:[G,H]?: r.inverse.inverse in rr} -- def "inverse" = {r:[G,H]?: r in rr} -- inverse_involution = rr ensure rr.inverse.inverse = rr end

Furthermore “inverse” is monotonic.

inverse_monotonic: all(r,s:[G,H]?) require r1: r<=s -- "<=" is the subset relation, -- i.e. `r' is contained in `s' check c1: all(x:G,y:H) require r2: [x,y] in r.inverse check c2: [y,x] in r -- r2 c3: [y,x] in s -- c2,r1 ensure [x,y] in s.inverse -- c3 end ensure r.inverse<=s.inverse end

For any collection of relations the infimum/supremum commutes with inverse

invers_commutes_limits: all(rr:[G,H]??) check c1: rr.infimum.inverse = {x:G,y:H: all(r:[G,H]?) r in rr => [x,y] in r}.inverse = {y:H,x:G: all(r:[G,H]?) r in rr => [x,y] in r} = {y:H,x:G: all(r:[H,G]?) r in rr.inverse => [y,x] in r} = rr.inverse.infimum ensure rr.infimum.inverse = rr.inverse.infimum -- c1 rr.supremum.inverse = rr.inverse.supremum -- c1 with "all,=>" replaced by "some,and" end

Since “x*y={x,y}.infimum” and “x+y={x,y}.supremum” we get the following laws.

inverse_commutes_order: all(r,s:[G,H]?) check c1: (r*s).invers = {r,s}.infimum.inverse -- def "*" = {r,s}.inverse.infimum -- inverse_commutes_limits = {r.inverse,s.inverse}.infimum -- def "inverse" on collection = r.inverse*s.inverse -- def "*" -- Note: {r,s} is a shorthand for {t:[G,H]?: t=s or t=r} ensure (r*s).inverse = r.inverse*s.inverse -- c1 (r+s).inverse = r.inverse+s.inverse -- c1 with infimum replaced -- by supremum end

## Composition

We can define the composition of two binary relations.

| (r:[F,G]?, s:[G,H]?): ghost [F,H]? -- The relation `r' composed with the relation `s'. ensure Result = {x:F,z:H: some(y:G) [x,y] in r and [y,z] in s} end

The composition is associative

composition_associative: all(r:[E,F]?, s:[F,G]?, t:[G,H]?) check r|s|t = {u:E,w:G: some(v:F) [u,v] in r and [v,w] in s} | t = {u:E,x:H: some(w:G) (some(v:F) [u,v] in r and [v,w] in s) and [w,x] in t} = {u:E,x:H: some(v:F,w:G) [u,v] in r and [v,w] in s and [w,x] in t} = {u:E,x:H: some(v:F) [u,v] in r and some(w:G) [v,w] in s and [w,x] in t} = r | {v:F,x:H: some(w:G) [v,w] in s and [w,x] in t} = r|(s|t) ensure r|s|t = r|(s|t) end

The prove is simple if one remembers the basic laws

all[G](x:G, e:BOOLEAN) x in {y:G: e} = e[y:=x] all[G](e1,e2:BOOLEAN) (some(x:G) e1) and e2 = (some(x:G) e1 and e2) -- x does not occur free in e2!

The operation “inverse” distributes over composition.

inverse_distributes_composition: all(r:[F,G]?, s:[G,H]?) check (r|s).inverse = {x:F,z:H: some(y:G) [x,y] in r and [y,z] in s}.inverse = {z:H,x:F: some(y:G) [x,y] in r and [y,z] in s} = {z:H,x:F: some(y:G) [z,y] in s.inverse and [y,x] in r.inverse} = s.inverse|r.invers ensure (r|s).inverse = s.invers|r.inverse end

## Images and preimages

Unlike a function where each argument is mapped to a unique value, a relation

does not map one element of its domain to only one element of its range. It

maps each element of its domain to a set of elements of the range. We can

define a function “image” which maps each element `x’ to a set of elements. If

`x’ is not in the domain of the relation then set is empty.

In the following we define the image for an element and the image for a set of

elements and the corresponding preimage functions.

image(x:G, r:[G,H]?): ghost H? -- The image of `x' under the relation `r'. ensure Result = {y:H: [x,y] in r} end image(p:G?, r:[G,H]?): ghost H? -- The image of the set `p' under the relation `r'. ensure Result = {y:H: some(x:G) x in p and [x,y] in r} end preimage(y,H, r:[G,H]?): ghost H? -- The preimage of `y' under the relation `r'. ensure Result = y.image(r.inverse) end preimage(q:H?, r:[G,H]?): ghost H? -- The preimage of the set `q' under the relation `r'. ensure Result = q.image(r.inverse) end

The image operator is monotonic in both arguments. First we prove that

“p.image(r)” is monotonic in “p”.

image_monotonic_in_set: all(p,q:G?, r:[G,H]?) require r1: p<=q check c1: all(y:H) require r2: y in p.image(r) check c2: some(x:G) x in p and [x,y] in r -- r2 c3: all(x:G) require r3: x in p r4: [x,y] in r check c4: x in q -- r3,r1 ensure some(x:G) x in q and [x,y] in r -- c4,r4 end c5: some(x:G) x in q and [x,y] in r -- c2,c3 ensure y in q.image(r) -- c5 end ensure p.image(r) <= q.image(r) -- c1 end

Next we prove that “p.image(r)” is monotonic in “r”.

image_monotonic_in_relation: all(p:G?, r,s:[G,H]?) require r1: r<=s check c1: all(y:H) require r2: y in p.image(r) check c2: some(x:G) x in p and [x,y] in r c3: all(x:G) require r3: x in p r4: [x,y] in r check c4: [x,y] in s -- r4,r1 ensure some(x:G) x in p and [x,y] in s -- r3,c4 end c5: some(x:G) x in p and [x,y] in s -- c2,c3 ensure y in p.image(s) -- c5 end ensure p.image(r)<=p.image(s) -- c1 end

Next we can see that containment of relations can be decided by containment

of the images.

all(r,s:[G,G]?) require r1: all(x:G) x.image(r)<=x.image(s) check c1: all(x,y:G) require r2: [x,y] in r check c2: y in x.image(r) -- r2 c3. y in x.image(s) -- c2,r1 ensure [x,y] in s -- c3 end ensure r<=s -- c1 end

Similar proofs can be done for the preimage operator.

Furthermore any set `p’ in the domain of a relation `r’ mapped through the

image operator and then back through the premage operator results in a

superset of `p’.

all(r:[G,H]?, p:G?) require r1: p<=r.domain check c0: all(x:G) require r2: x in p check c1: some(y:H) [x,y] in r -- r1,r2 c2: all(y:H) require r3: [x,y] in r ensure some(z:G,y:H) z in p and [z,y] in r and [x,y] in r -- r3,r2, witness [x,y] end c3: some(z:G,y:H) z in p and [z,y] in r and [x,y] in r -- c1,c2 c4: some(y:H) y in p.image(r) and [x,y] in r -- c3 ensure x in p.image(r).preimage(r) -- c4 end ensure p<=p.image(r).preimage(r) -- c0 end

With the same reasoning it is possible to proof the dual law

all(r:[G,H]?, q:H?) require q in r.range ensure q <= q.preimage(r).image(r) -- proof similar to proof above end

## Domain/range restrictions of relations

We can restrict the domain or the range of a relation and get a restricted

relation.

feature <: (p:G?, r:[G,H]?): [G,H]? -- The relation `r' restricted to the domain `p' ensure Result = {x:G,y:H: [x,y] in r and x in p} end <-:(p:G?, r:[G,H]?): [G,H]? -- The relation `r' without the domain `p' ensure Result = (-p)<:r end :> (r:[G,H]?, q:H?): [G,H]? -- The relation `r' restricted to the range `q' ensure Result = {x:G,y:H: [x,y] in r and y in q} end <-:(r:[G,H]?, q:H?): [G,H]? -- The relation `r' without the range `q' ensure Result = r:>(-q) end end

The restriction and substraction of domain or range respectively are

complementary operations which split the relation into two disjoint

complementary subrelations.

feature all(r:[G,H]?, p:G?, q:H?) ensure -- proof: def `<:', def `<-:' p<:r + p<-:r = r p<:r * p<-:r = 0 r:>q + r:->q = r r:>q * r:->q = 0 end end

Some obvious laws for the domains and ranges of restricted relations.

feature all(r:[G,H]?, p:G?, q:H?) ensure -- Proofs: Just expand the definitions of "<:", ":>", -- "domain", "range", "image" and "preimage" (p<:r).domain = p (p<:r).range = p.image(r) (r:>q).range = q (r:>q).domain = q.preimage(r) end end

A subrelation `r’ of a relation `s’ remains a subrelation if we substract a

set `p’ from the domain of `s’ which is disjoint from the domain of `r’.

all(r,s:[G,H]?, p:G?) require r1: r<=s r2: p*r.domain = 0 check all(x:G,y:H) require r3: [x,y] in r check c1: x in r.domain -- r3 c2: not (x in p) -- c1,r2 c3: [x,y] in s -- r3,r1 ensure [x,y] in (p<-:s) -- c2,c3 end ensure r <= p<-:s end

The same applies to range substraction.

all(r,s:[G,H]?, q:H?) require r1: r<=s r2: q*r.range = 0 check all(x:G,y:H) require r3: [x,y] in r check c1: y in r.range -- r3 c2: not (y in q) -- c1,r2 c3: [x,y] in s -- r3,r1 ensure [x,y] in (s:->q) -- c2,c3 end ensure r <= s:->q end

## Functional relations

A binary relation is functional if for all pairs [x,y] and [x,z] implies that

y is identical to z.

is_functional(r:[G,H]?): ghost BOOLEAN -- Is the relation `r' functional? ensure Result = all(x:G,y,z:H) [x,y] in r => [x,z] in r => y=z end

If a relation is functional, it is possible to convert the relation to a

function.

feature function(r:[G,H]?): ghost G->H require r.is_functional ensure Result = (agent(a) require a in r.domain ensure [a,Result] in r end) end end

The result of the anonymous function is defined by the property it has to

satisfy. This specification of a function is valid only if it is provable that

there exists an object which satisfies the specification and that the object

is unique. I.e. the following proof is needed.

all(r:[G,H]?, a:G) require r1: r.is_functional r2: a in r.domain ensure some(b:H) [a,b] in r -- r2 all(x,y:H) [a,x] in r => [a,y] in r => x=y -- r1, def "is_functional" end

Since the proof requires just to expand the definition of `is_functional’, it

can be done automatically by the system.

If a relation is functional then whenever two images are disjoint, the

corresponding preimages have to be disjoint as well. Here is a detailed proof

of this statement.

functional_disjoint_preimages: all(r:[G,H]?, p,q:H?) require r1: r.is_functional r2: p*q = 0 check all(x:G) require r3: x in p.preimage(r) r4: x in q.preimage(r) check c1: some(y:H) [x,y] in r and y in p -- r3 c2: some(z:H) [x,z] in r and z in q -- r4 c3: all(y:H) require r5: [x,y] in r r6: y in p check c4: all(z:H) require r7: [x,z] in r r8: z in q check c5: y = z -- r1,r5,r7 c6: y /= z -- r6,r8,r2 ensure False -- c5,c6 end ensure False -- c2,c4 end ensure False -- c1,c3 end ensure p.preimage(r)*q.preimage(r) = 0 end

There is another law for functional relations.

all(r:[G,H]?, q:H?) require r.is_functional q<=r.range ensure q = q.preimage(r).image(r) -- `<=' true in general (chapter images and preimages) -- `>=' proof see below end

In general `q<=q.preimage(r).image(r)’ is valid (see chapter about images and

preimages). It remains to be proved that `q’ is a superset in the case of a

functional relation.

all(r:[G,H]?, q:H?) require r1: r.is_functional check c1: all(y:H) require r2: y in q.preimage(r).image(r) check c2: some(x:G,z:H) z in q and [x,z] in r and [x,y] in r -- r2 c3: all(x:G,z:H) require r3: z in q r4: [x,z] in r r5: [x,y] in r check c4: y=z -- r4,r5,r1 ensure y in q -- r3,c4 end ensure y in q end ensure q.preimage(r).image(r) <= q -- c1 end

# Endorelations

A binary relation is an endorelation if the type of the domain is the same as

the type of the range.

## Properties of endorelations

The most important properties of endorelations are reflexivity, transitivity

and symmetry. It is easy to define these properties formally.

is_reflexive(r:[G,G]?): ghost BOOLEAN -- Is the relation `r' reflexive? ensure Result = all(x:G) [x,x] in r end is_transitive(r:[G,G]?): ghost BOOLEAN -- Is the relation `r' transitive? ensure Result = all(x,y,z:G) [x,y] in r => [y,z] in r => [x,z] in r end is_symmetric(r:[G,G]?): ghost BOOLEAN -- Is the relation `r' symmetric? ensure Result = (r=r.inverse) end

## Duality

For endorelations we have an important duality principle which states whenever

a relation is reflexive, transitive or symmetric the inverse relation satisfies

the corresponding property.

er_1: all(r:[G,G]?) ensure r.is_reflexive => r.inverse.is_reflexive r.is_transitive => r.inverse.is_transitive r.is_symmetric => r.inverse.is_symmetric end

The proofs for reflexivity and symmetry are trivial. We spell out a proof for

transitivity.

all(r:[G,G]?) require r1: r.is_transitive check c1: all(x,y,z:G) require r2: [x,y] in r.invers r3: [y,z] in r.invers check c2: [z,y] in r -- r3 c3: [y,x] in r -- r2 c4: [z,x] in r -- c2,c3,r1 ensure [x,z] in r.invers -- c4 end ensure r.invers.is_transitive -- c1 end

## Transitivity and restricted relations

We claim that any restriction (domain or range) of a transitive relation

results in a transitive relation.

er_2: all(r:[G,G]?, p:G?) require r1: r.is_transitive check all(x,y,z) require r2: [x,y] in (p<:r) r3: [y,z] in (p<:r) check c1: [x,y] in r -- r2 c2: x in p -- r2 c3: [y,z] in r -- r3 c4: [x,z] in r -- c1,c3,r1 ensure [x,z] in (p<:r) -- c4,c2 end ensure (p<:r).is_transitive end

er_3: all(r:[G,G]?, q:G?) require r1: r.is_transitive check all(x,y,z) require r2: [x,y] in (r:>q) r3: [y,z] in (r:>q) check c1: [x,y] in r -- r2 c2: [y,z] in r -- r3 c3: z in q -- r3 c4: [x,z] in r -- c1,c2,r1 ensure [x,z] in (r:>q) -- c4,c3 end ensure (r:>q).is_transitive end

## Transitivity and images

We call a set `p’ closed under a relation `r’ if it satisfies the following

predicate.

is_closed(p:G?, r:[G,G]?): ghost BOOLEAN -- Is the set `p' closed under the relation `r'? ensure Result = all(x,y:G) [x,y] in r => x in p => y in p end

All images of a transitive relation `r’ are closed under the relation `r’.

er_4: all(p,q:G?, r:[G,G]?) require r1: r.is_transitive r2: q = p.image(r) check c1: all(y,z:G) require r3: [y,z] in r r4: y in q check c2: some(x:G) x in p and [x,y] in r -- r4,r2 c3: all(x:G) require r5: x in p r6: [x,y] in r check c4: [x,z] in r -- r6,r3,r1 ensure z in q -- r5,c4,r2 end ensure z in q -- c2,c3 end ensure q.is_closed(r) -- c1 end

The same applies to the union of a set `p’ with its image under `r’.

er_4a: all(p,q:G?, r:[G,G]?) require r1: r.is_transitive r2: q = p.image(r) check c1: all(x,y:G) require r3: [x,y] in r r4: x in (p+q) check c2: x in p or x in q -- r4 c3: x in p => y in q -- r2 c4: x in q => y in q -- r2,r1,er_4 c5: y in q -- c2,c3,c4 ensure y in (p+q) -- c5 end ensure (p+q).is_closed(r) -- c1 end

## Closure systems

The set of all reflexive relations, the set of all symmetric relations and the

set of all transitive relations are closure systems. Recall that a set is a

closure system if arbitrary intersections of elements remain within the set

(for more details please read the article “Complete lattices and closure

systems).

Let us state the properties first.

er_5: all(rr:[G,G]??) ensure rr={r: r.is_transitive} => rr.is_closure_system -- proof see below rr={r: r.is_reflexive} => rr.is_closure_system -- def "is_closure_system", "infimum", "is_reflexive" rr={r: r.is_symmetric} => rr.is_closure_system -- def "is_closure_system", "infimum", "is_symmetric" end

The most important closure system is the set of transitive relations. We give

a formal proof that the set of transitive relations form a closure system (the

proof for reflexive and symmetric relations is similar). The proof is spelled

out in detail in the following.

all(rr:[G,G]??) require r1: rr = {r: r.is_transitive} check c1: all(ss:[G,G]??) require r2: ss<=rr check c2: all(x,y,z:G) require r3: all(r:[G,G]?) r in ss => [x,y] in r r4: all(r:[G,G]?) r in ss => [y,z] in r check c3: all(r:[G,G]?) require r5: r in ss check c4: r.is_transitive -- r5,r2 c5: [x,y] in r -- r5,r3 c6: [y,z] in r -- r5,r4 ensure [x,z] in r -- c4,c5,c6 end ensure all(r:[G,G]?) r in ss => [x,z] in r end c7: {x,y:G: all(r:[G,G]?) r in ss => [x,y] in r}.is_transitive -- c2 c8: s.infimum.is_transitive -- c7,def "infimum" ensure ss.infimum in rr -- c8,r1 end ensure rr.is_closure_system -- c1, def "is_closure_system" end

The proof seems complicated at first glance because it contains all detailed

steps. But it is just an expansion of the definitions of “is_closure_system”,

“infimum”, and “is_transitive”. Since it requires just the expansion of

defintions and some simple algebraic transformations, the proof can be done by

the system automatically.

# Transitive closures

## Transitive relations with logical implication

The boolean operation `=>’ is transitive. This can be used to create the

transitive relation `{x,y:G: e => e[x;=y]}’ over any type G with the help of a

boolean expression `e’ with one free variable.

tc_1: all(r:[G,G]?, e:BOOLEAN) require r1: r = {x,y: e => e[x:=y]} check c1: all(x,y,z:G) require r2: [x,y] in r r3: [y,z] in r check c2: e => e[x:=y] -- r2,r1 c3: e[x:=y] => e[x:=z] -- r3,r1 c4: e => e[x:=z] -- c2,c3 ensure [x,z] in r -- c4,r1 end ensure r.is_transitive -- c1 end

## Inheriting properties via relations and transitive closures

In the article “complete lattices and closure systems” we have given a

definition for the statement that a set `p:G?’ is closed under a relation

`r:[G,G]?’

p.is_closed(r) = all(x,y) x in p => [x,y] in r => y in p -- or equivalent p.is_closed(r) = all(x) x in p => (x.image(r)<=p)

This definition says that the relation `r’ inherits the property of an element

`x’ of being in `p’ to all elements in its image.

If we rewrite the definition of `p.is_closed(r)’ slightly we can verify the

following assertion.

tc_2: all(r,rp:[G,G]?, p:G?) require r1: rp = {x,y: x in p => y in p} check c1: (r<=rp) = all(x,y:G) [x,y] in r => x in p => y in p -- def "<=", r1 ensure rp.is_transitive -- r1, tc_1 p.is_closed(r) = (r<=rp) -- c1, def "is_closed" end

This assertions states that the relation `{x,y: x in p => y in p}’ is a

transitive relation and that the statement `p.is_closed(r)’ is equivalent to

`r’ being a subset of this relation.

From this we can conclude immediately that if `p’ is closed under a relation

`r’ then it is closed under any subset of `r’ as well.

tc_3: all(r,s:[G,G]?, p:G?) require r1: p.is_closed(r) r2: s<=r check c1: r<={x,y: x in p => y in p} -- r1, tc_2 c2: s<={x,y: x in p => y in p} -- r2,c1 ensure p.is_closed(s) -- c2, tc_2 end

This proof is straighforward, because `s’ is a subset of `r’ and the subset

relation is transitive. But we can prove the closedness under the transitive

closure of `r’ which is a superset of `r’ as well.

We claim that if a set `p’ is closed under a relation `r’ then its closed

under the transitive closure `rc’ as well.

tc_4: all(r,rc,rp:[G,G]?, p:G?) require r1: p.is_closed(r) r2: rc = r.closed(is_transitive) r3: rp = {x,y: x in p => y in p} check c1: rp.is_transitive -- r3, tc_1 c2: r <= rp -- r1, tc_2 c3: rc <= rp -- c1,c2,r2 ensure p.is_closed(rc) -- c3, tc_2 end

This proof is based on the crucial fact that the transitive closure of a

relation `r’ is the least relation which is transitive and contains `r’. Since

`rp’ is transitive and contains `r’ by `tc_2′, `rc’ must be less or equal

`rp’ which implies that `p’ is closed under the transitive closure as well.

## Reachability via a relation

If we have a set `p’ of elements of type G and a relation `r:[G,G]?’ then we

can ask the question which elements can be reached from `p’ via `r’ in zero or

more steps. This set can be calculated via a closure operation as demonstrated

in the paper “Complete lattices and closure systems” by the expression

`pc=p.closed(r)’.

Since `pc’ is calculated via a closure operation it is the least set which

contains `p’ and is closed under the relation `r’.

From tc_4 we can conclude doing the closure operation with `r’ and doing it

with its transitive closure must yield the same result.

tc_5: all(r,rc:[G,G], q,qc:G?) require r1: rc = r.closed(is_transitive) r2: qc = q.closed(r) check c1: all(p:G?) q<=p => q.is_closed(r) => qc<=q -- r2, closure is least set c2: qc.is_closed(r) -- r2 c3: qc.is_closed(rc) -- c2, tc_4 c4: all(p:G?) require r3: q<=p r4: q.is_closed(rc) check c5: q.is_closed(r) -- r4, r1, tc_3 ensure qc<=q -- r3,c5,c1 end c6: qc = q.closed(rc) -- c3,c4 ensure q.closed(r) = q.closed(rc) -- r2,c6 end

## Equivalent expressions for transitive closures

We want to show that the relations

r.closed(is_transitive) {x,y: y in x.image(r).closed(r)}

are equivalent. We proof this by

tc_6: all(r,s,rc:[G,G]?) require rc = r.closed(is_transitive) s = {x,y: y in x.image(r).closed(r)} check rc <= s -- lemma_1 below s <= rc -- lemma_2 below ensure rc = s end

The following `lemma_1′ proves that `s’ is transitive and includes `r’ and

therefore must be a superset of `rc’.

lemma_1: all(r,s:[G,G]?) require r1: s = {x,y: y in x.image(r).closed(r)} r2: rc = r.closed(is_transitive) check c1: all(x,y,z:G) require r2: [x,y] in s r3: [y,z] in s check c2: y in x.image(r).closed(r) -- r2 c3: z in y.image(r).closed(r) -- r3 c4: z in x.image(r).closed(r) -- c2,c3,closure is monotonic ensure [x,z] in s -- c4 end c5: s.is_transitive -- c1 c6: all(x,y) require r4: [x,y] in r check c7: y in x.image(r) -- r4 c8: y in x.image(r).closed(r) -- c7, closure is ascending ensure [x,y] in s -- c8 end c9: r<=s -- c6 ensure rc <= s -- c5,c9,r2 end

The following `lemma_2′ shows that a transitive closure `rc’ of a relation `r’

always produces closed images (under the relation `r’) and every image under

`rc’ contains the corresponding image under `r’ and therfore must contain the

corresponding images of `s’ which are least sets by definition.

lemma_2: all(r,s,rc:[G,G]?) require r1: rc = r.closed(is_transitive) r2: s = {x,y: y in x.image(r).closed(r)} check c0: all(x:G) check c1: r<=rc -- r1 c2: x.image(r) <= x.image(rc) -- c1, image monotonic c3: x.image(rc).is_closed(rc) -- r1, er_4 c4: x.image(rc).is_closed(r) -- c3, tc_5 c5: x.image(r).closed(r) <= x.image(rc) -- c2,c4 ensure x.image(s) <= x.image(rc) -- c5,r2 end ensure s <= rc -- c0 end

## Equivalent expressions for closed sets

We want to show that the sets

p.closed(r) p + p.image(r.closed(is_transitive))

are equivalent. Proof:

tc_7: all(p,pc:G?, r,rc:[G,G]?) require pc = p.closed(r) rc = r.closed(is_transitive) check pc <= p + p.image(rc) -- lemma_1 below p + p.image(rc) <= pc -- lemma_2 below ensure pc = p + p.image(rc) end

lemma_1: all(p,pc:G?, r,rc:[G,G]?) require r1: pc = p.closed(r) r2: rc = r.closed(is_transitive) check c1: p <= p + p.image(rc) c2: p.image(rc).is_closed(r) -- r2, tc_4 c3: all(x,y:G) require r3: x in p r4: [x,y] in r check c4: y in x.image(r) -- r4 c5: y in x.image(rc) -- c4,r2 ensure y in p+p.image(rc) end c4: (p+p.image(rc)).is_closed(r) -- c3 ensure pc <= p + p.image(rc) -- c1,c4,r1 end

lemma_2: all(p,pc:G?, r,rc:[G,G]?) require r1: pc = p.closed(r) r2: rc = r.closed(is_transitive) check c3: p.image(r) <= pc -- r1 c4: p.image(r).closed(r) <= pc.closed(r) -- c3, closure monotonic c5: p.image(r).closed(r) <= pc -- c4, closure idempotent c6: p.image(rc) = p.image({x,y: y in x.image(r).closed(r)}) -- tc_6 c7: p.image(rc) = p.image(r).closed(r) -- c6 c8: p.image(rc) <= pc -- c5,c7 ensure p + p.image(rc) <= pc -- c1,c8 end