# HAMILTON CYCLES IN EMBEDDED GRAPHS

N/A
N/A
Protected

Share "HAMILTON CYCLES IN EMBEDDED GRAPHS"

Copied!
51
0
0

Full text

(1)

## HAMILTON CYCLES IN EMBEDDED GRAPHS

Roman Nedela and Martin ˇSkoviera University of West Bohemia, Pilsen

Comenius University, Bratislava

joint work with Michal Kotrbˇc´ık

SCDO 2016 Queenstown, New Zealand

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 1 / 32

(2)

## Lov´ asz problem

Problem (Lov´asz, 1969)

Does every vertex-transitive graphadmit a Hamilton path?

Conjecture (folklore)

Every Cayley graph(of order at least 3) has a Hamilton cycle.

Critical case: cubic Cayley graphs

(3)

## Lov´ asz problem

Problem (Lov´asz, 1969)

Does every vertex-transitive graphadmit a Hamilton path?

Conjecture (folklore)

Every Cayley graph(of order at least 3) has a Hamilton cycle.

Critical case: cubic Cayley graphs

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 2 / 32

(4)

## Lov´ asz problem

Problem (Lov´asz, 1969)

Does every vertex-transitive graphadmit a Hamilton path?

Conjecture (folklore)

Every Cayley graph(of order at least 3) has a Hamilton cycle.

Critical case: cubic Cayley graphs

(5)

## Hamilton cycles in cubic Cayley graphs

Theorem (Glover, Maruˇsiˇc, Kutnar, Malniˇc, 2007–2012) Let K =Cay(H;r,r−1,l) be a cubic Cayley graph, where H =hr,l |rs =l2 = (rl)3 = 1, . . .i is a finite quotient

of the modular group PSL(2,Z). ThenK has a Hamilton path.

Moreover, if |H| ≡2 (mod 4)or if |r| ≡0,±1 (mod 4), then K has a Hamilton cycle.

Question 1.

What about the missing case |H| ≡0 (mod 4)and|r| ≡2 (mod 4)? Question 2.

What about the finite quotients of the group

hx,y,z |x2=y2=z2 = (xy)3= (yz)3= 1, . . .i ?

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 3 / 32

(6)

## Hamilton cycles in cubic Cayley graphs

Theorem (Glover, Maruˇsiˇc, Kutnar, Malniˇc, 2007–2012) Let K =Cay(H;r,r−1,l) be a cubic Cayley graph, where H =hr,l |rs =l2 = (rl)3 = 1, . . .i is a finite quotient

of the modular group PSL(2,Z). ThenK has a Hamilton path.

Moreover, if |H| ≡2 (mod 4)or if |r| ≡0,±1 (mod 4), then K has a Hamilton cycle.

Question 1.

What about the missing case |H| ≡0 (mod 4)and|r| ≡2 (mod 4)?

Question 2.

What about the finite quotients of the group

hx,y,z |x2=y2=z2 = (xy)3= (yz)3= 1, . . .i ?

(7)

## Hamilton cycles in cubic Cayley graphs

Theorem (Glover, Maruˇsiˇc, Kutnar, Malniˇc, 2007–2012) Let K =Cay(H;r,r−1,l) be a cubic Cayley graph, where H =hr,l |rs =l2 = (rl)3 = 1, . . .i is a finite quotient

of the modular group PSL(2,Z). ThenK has a Hamilton path.

Moreover, if |H| ≡2 (mod 4)or if |r| ≡0,±1 (mod 4), then K has a Hamilton cycle.

Question 1.

What about the missing case |H| ≡0 (mod 4)and|r| ≡2 (mod 4)?

Question 2.

What about the finite quotients of the group

hx,y,z |x2=y2=z2 = (xy)3= (yz)3 = 1, . . .i?

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 3 / 32

(8)

l r

(9)

## Proof: topological background

Main idea

Take the Cayley mapM corresponding to H =hr,l |rs =l2 = (rl)3= 1, . . .i

Select a suitable setF of faces ofMsuch thatSF isconnectedand null-homologous, i.e., a ‘tree’of faces.

Construct a Hamilton cycle as the topological boundary∂(SF) The result is acontractible Hamilton cycle in CM(H;r,r−1,l).

The idea of constructing a Hamilton cycle as a boundary of a set of faces of map goes back to W. R. Hamilton (1858).

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 5 / 32

(10)

Do we need symmetry?

Do we need orientability?

Do we need contractibleHamilton cycles?

(11)

## Bounding Hamilton cycles in embedded graphs

Definition 1. LetK ,→S be a graph embedded in a closed surface S and let B ⊆K. We say that B is one-sidedin S ifS−B is connected and the boundary is also connected.

Example: Atree in an embedded graph is always one-sided.

Definition 2. LetG ,→S be an embedding of a graph forming polytopal map M. Aweak 2-face colouringof Mis a colouring of faces ofMwith two colours s.t. at each vertex of there are precisely two edges separating differently coloured faces.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 7 / 32

(12)

## Bounding Hamilton cycles in embedded graphs

Definition 1. LetK ,→S be a graph embedded in a closed surface S and let B ⊆K. We say that B isone-sided inS ifS−B is connected and the boundary is also connected.

Example: Atree in an embedded graph is always one-sided.

Definition 2. LetG ,→S be an embedding of a graph forming polytopal map M. Aweak 2-face colouringof Mis a colouring of faces ofMwith two colours s.t. at each vertex of there are precisely two edges separating differently coloured faces.

(13)

## Bounding Hamilton cycles in embedded graphs

Definition 1. LetK ,→S be a graph embedded in a closed surface S and let B ⊆K. We say that B isone-sided inS ifS−B is connected and the boundary is also connected.

Example: Atree in an embedded graph is always one-sided.

Definition 2. LetG ,→S be an embedding of a graph forming polytopal map M. Aweak 2-face colouringof Mis a colouring of faces ofMwith two colours s.t. at each vertex of there are precisely two edges separating differently coloured faces.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 7 / 32

(14)

## Bounding Hamilton cycles in embedded graphs

Definition 1. LetK ,→S be a graph embedded in a closed surface S and let B ⊆K. We say that B isone-sided inS ifS−B is connected and the boundary is also connected.

Example: Atree in an embedded graph is always one-sided.

Definition 2. LetG ,→S be an embedding of a graph forming polytopal map M. Aweak 2-face colouringof Mis a colouring of faces ofMwith two colours s.t. at each vertex of there are precisely two edges separating differently coloured faces.

(15)

## Bounding Hamilton cycles: characterisation

Theorem 1

Let Mbe a polytopal map on a closed surface of Euler genus g. The following statements are equivalent.

(i) Mhas a bounding Hamilton cycle.

(ii) The vertices of M can be a partitioned into two subsets which induceone-sided subgraphs H and K such that β(H) +β(K) =g. (iii) Mhas a weak2-face-colouring such that the vertices of M

receiving colour 1 induce a one-sided subgraph ofM.

Theorem 2

A polytopal map Madmits acontractible Hamilton cycle ⇐⇒ M has aweak2-face-colouring such that the vertices of M receiving colour1 induce a tree.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 8 / 32

(16)

## Bounding Hamilton cycles: characterisation

Theorem 1

Let Mbe a polytopal map on a closed surface of Euler genus g. The following statements are equivalent.

(i) Mhas a bounding Hamilton cycle.

(ii) The vertices of M can be a partitioned into two subsets which induceone-sided subgraphs H and K such that β(H) +β(K) =g. (iii) Mhas a weak2-face-colouring such that the vertices of M

receiving colour 1 induce a one-sided subgraph ofM.

Theorem 2

A polytopal map Madmits acontractible Hamilton cycle ⇐⇒

Mhas a weak2-face-colouring such that the vertices of M receiving colour1 induce a tree.

(17)

## Remarks

Remark 1

According to the Strong Embedding Conjecture, every 2-connected graph has a polytopal embedding.

=⇒ Theorem 1 can potentially be applied toall2-connected graphs.

Remark 2

Part (ii) of Theorem 1 implies that a Hamilton cycle in a planar map M corresponds to a vertex partition of M into two induced trees.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 9 / 32

(18)

## Remarks

Remark 1

According to the Strong Embedding Conjecture, every 2-connected graph has a polytopal embedding.

=⇒ Theorem 1 can potentially be applied toall2-connected graphs.

Remark 2

Part (ii) of Theorem 1 implies that a Hamilton cycle in a planar map M corresponds to a vertex partition of M into two induced trees.

(19)

## Hamilton cycles in 2-face-coloured cubic polytopal maps

In certain cases a map may be given an initial2-face-colouring.

Typical example: truncated maps t(M) vertex-faces 7→ colour0

face-faces 7→ colour1

Theorem

Let Mbe a cubic polytopal map with a fixed weak2-face colouring. If the vertices of M receiving colour 1can be partitioned into an induced tree and anindependent set, then Madmits acontractibleHamilton cycle.

Theorem

A connected cubic graph G admits a partition of its vertex-set into an induced treeand anindependent set ⇐⇒

G has cellular embedding into an orientable surface with a single face.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 10 / 32

(20)

## Hamilton cycles in 2-face-coloured cubic polytopal maps

In certain cases a map may be given an initial2-face-colouring.

Typical example: truncated maps t(M) vertex-faces 7→ colour0

face-faces 7→ colour1

Theorem

Let Mbe a cubic polytopal map with a fixed weak2-face colouring. If the vertices of M receiving colour 1can be partitioned into an induced tree and anindependent set, then Madmits acontractibleHamilton cycle.

Theorem

A connected cubic graph G admits a partition of its vertex-set into an induced treeand anindependent set ⇐⇒

G has cellular embedding into an orientable surface with a single face.

(21)

## Hamilton cycles in 2-face-coloured cubic polytopal maps

In certain cases a map may be given an initial2-face-colouring.

Typical example: truncated maps t(M) vertex-faces 7→ colour0

face-faces 7→ colour1

Theorem

Let Mbe a cubic polytopal map with a fixed weak2-face colouring. If the vertices ofM receiving colour 1can be partitioned into an induced tree and anindependent set, then Madmits acontractibleHamilton cycle.

Theorem

A connected cubic graph G admits a partition of its vertex-set into an induced treeand anindependent set ⇐⇒

G has cellular embedding into an orientable surface with a single face.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 10 / 32

(22)

## Hamilton cycles in 2-face-coloured cubic polytopal maps

In certain cases a map may be given an initial2-face-colouring.

Typical example: truncated maps t(M) vertex-faces 7→ colour0

face-faces 7→ colour1

Theorem

Let Mbe a cubic polytopal map with a fixed weak2-face colouring. If the vertices ofM receiving colour 1can be partitioned into an induced tree and anindependent set, then Madmits acontractibleHamilton cycle.

Theorem

A connected cubic graph G admits a partition of its vertex-set into an induced treeand anindependent set ⇐⇒

G has cellular embedding into an orientable surface with a single face.

(23)

## Contractible Hamilton cycles in truncated triangulations

Every truncated triangulation t(T) has a natural weak 2-face-colouring vertex-faces 7→ colour0

face-faces 7→ colour1

Theorem

Let T be a triangulation of a closed surface and let t(T) be the truncation of T. The following statements are equivalent.

(i) t(T)has a contractible Hamilton cycle.

(ii) The vertex set of T admits a partition{A,J}whereAinduces a tree in the underlying graph ofT andJ isindependent.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 11 / 32

(24)

END OF PART I

Thank you!

(25)

HAMILTON CYCLES IN EMBEDDED GRAPHS

PART II

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 13 / 32

(26)

l r

(27)

## Contractible Hamilton cycles in truncated triangulations

Every truncated triangulation t(T) has a natural weak 2-face-colouring vertex-faces 7→ colour0

face-faces 7→ colour1

Observation

The subgraph of t(T) induced by the vertices of colour 1is isomorphic to the underlying graph of T and is therefore cubic.

Theorem

Let T be a triangulation of a closed surface and let t(T) be the truncation of T. The following statements are equivalent.

(i) t(T)has a contractible Hamilton cycle.

(ii) The vertex set of T admits a partition{A,J}whereAinduces a tree in the underlying graph ofT andJ isindependent.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 15 / 32

(28)

## Contractible Hamilton cycles in truncated triangulations

Every truncated triangulation t(T) has a natural weak 2-face-colouring vertex-faces 7→ colour0

face-faces 7→ colour1 Observation

The subgraph of t(T) induced by the vertices of colour 1is isomorphic to the underlying graph of T and is therefore cubic.

Theorem

Let T be a triangulation of a closed surface and let t(T) be the truncation of T. The following statements are equivalent.

(i) t(T)has a contractible Hamilton cycle.

(ii) The vertex set of T admits a partition{A,J}whereAinduces a tree in the underlying graph ofT andJ isindependent.

(29)

## Contractible Hamilton cycles in truncated triangulations

Every truncated triangulation t(T) has a natural weak 2-face-colouring vertex-faces 7→ colour0

face-faces 7→ colour1 Observation

The subgraph of t(T) induced by the vertices of colour 1is isomorphic to the underlying graph of T and is therefore cubic.

Theorem

Let T be a triangulation of a closed surface and let t(T) be the truncation of T. The following statements are equivalent.

(i) t(T)has a contractible Hamilton cycle.

(ii) The vertex set of T admits a partition{A,J}whereAinduces a tree in the underlying graph ofT andJ isindependent.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 15 / 32

(30)

(31)

## Example: Construction of a Hamilton cycle in t(T )

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 17 / 32

(32)

(33)

## Example: Construction of a Hamilton cycle in t(T )

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 19 / 32

(34)

(35)

## Example: Construction of a Hamilton cycle in t(T )

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 21 / 32

(36)

(37)

## When does such a structure exist?

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 23 / 32

(38)

## Vertex-partitions in cubic graphs

Theorem

The following are equivalent for every connected cubic graph G . (i) V(G) has a partition{A,J}where Ainduces a tree andJ is

independent.

(ii) G has an orientable cellular embedding with a single face.

(39)

## Contractible Hamilton cycles in truncated triangulations

Theorem

Let T be a triangulation of a closed surface and let t(T) be the truncation of T. The following statements are equivalent.

(i) t(T)has a contractible Hamilton cycle.

(ii) The underlying graph of T admits an orientable cellular embedding with asingle face.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 25 / 32

(40)

## Corollaries

Corollary

Let T be a triangulation of a closed surface with f faces. If T has no separating 3-cycles, then its trucation admits a Hamilton path. Moreover, t(T) has acontractible Hamilton cycle in each of the following cases:

(i) f ≡2 (mod 4)

(ii) T is cyclically 5-connected andT has a vertex of degree0 (mod 4).

(iii) T is cyclically 6-connected andT has two adjacent vertices with degrees deg(u)≡deg(v)≡ ±1 (mod 4).

(41)

## Interesting example

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 27 / 32

(42)

## A unified approach to results of Glover, Maruˇsiˇ c et al.

Theorem

Let K =Cay(H;r,r−1,l) be a cubic Cayley graph, where H =hr,l |rs =l2 = (rl)3 = 1, . . .i is a finite quotient of the modular group PSL(2,Z). Then the following hold.

(i) K has a Hamilton path.

(ii) K has abounding Hamilton cycle with respect to its natural embedding as a Cayley map CM(H;r,l) ⇐⇒

|H| ≡2 (mod 4)or if|r| ≡0,±1 (mod 4).

Furthemore, if CM(H;r,l)has a bounding Hamilton cycle, then it has a contractible one.

(43)

## A unified approach to results of Glover, Maruˇsiˇ c et al.

Proof of (ii).

“=⇒”: Construction.

“⇐=”: Counting argument: Theorem

Let Mbe a polytopal map withn vertices and let Q be a one-sided subgraph of M determining a bounding Hamilton cycle in M. Ifβ(Q) =b, then

X

v∈V(Q)

(deg(v)−2)−2b+ 2 =n.

In our case, M=CM(H;r,l) is orientable, so Q must have an even Betti number. Hence n =|H|=2 (mod 4), a contradiction.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 29 / 32

(44)

## A unified approach to results of Glover, Maruˇsiˇ c et al.

Proof of (ii).

“=⇒”: Construction.

“⇐=”: Counting argument:

Theorem

Let Mbe a polytopal map withn vertices and let Q be a one-sided subgraph of M determining a bounding Hamilton cycle in M. Ifβ(Q) =b, then

X

v∈V(Q)

(deg(v)−2)−2b+ 2 =n.

In our case, M=CM(H;r,l) is orientable, so Q must have an even Betti number. Hence n =|H|=2 (mod 4), a contradiction.

(45)

## A unified approach to results of Glover, Maruˇsiˇ c et al.

Proof of (ii).

“=⇒”: Construction.

“⇐=”: Counting argument:

Theorem

Let Mbe a polytopal map withn vertices and let Q be a one-sided subgraph of M determining a bounding Hamilton cycle in M.

Ifβ(Q) =b, then

X

v∈V(Q)

(deg(v)−2)−2b+ 2 =n.

In our case, M=CM(H;r,l) is orientable, so Q must have an even Betti number. Hence n =|H|=2 (mod 4), a contradiction.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 29 / 32

(46)

## A unified approach to results of Glover, Maruˇsiˇ c et al.

Proof of (ii).

“=⇒”: Construction.

“⇐=”: Counting argument:

Theorem

Let Mbe a polytopal map withn vertices and let Q be a one-sided subgraph of M determining a bounding Hamilton cycle in M.

Ifβ(Q) =b, then

X

v∈V(Q)

(deg(v)−2)−2b+ 2 =n.

In our case, M=CM(H;r,l) is orientable, so Q must have an even Betti number. Hence n=|H|=2 (mod 4), a contradiction.

(47)

## Truncations of Coxeter triangulations of the torus

Coxeter and Moser classified regular toroidal triangulations as{3,6}b,c where b andc are non-negative integer parameters. The size of the orientation-preserving automorphism group is 6(b2+bc +c2).

Corollary

The truncation of {3,6}b,c has abounding Hamilton cycle ⇐⇒ at least one of b andc is odd.

Altshuler (1972)proved that all these graphs are hamiltonian.

=⇒ Ifb andc are even, then all Hamilton cycles arenon-bounding.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 30 / 32

(48)

## Truncations of Coxeter triangulations of the torus

Coxeter and Moser classified regular toroidal triangulations as{3,6}b,c where b andc are non-negative integer parameters. The size of the orientation-preserving automorphism group is 6(b2+bc +c2).

Corollary

The truncation of {3,6}b,c has abounding Hamilton cycle ⇐⇒

at least one of b andc is odd.

Altshuler (1972)proved that all these graphs are hamiltonian.

=⇒ Ifb andc are even, then all Hamilton cycles arenon-bounding.

(49)

## Truncations of Coxeter triangulations of the torus

Coxeter and Moser classified regular toroidal triangulations as{3,6}b,c where b andc are non-negative integer parameters. The size of the orientation-preserving automorphism group is 6(b2+bc +c2).

Corollary

The truncation of {3,6}b,c has abounding Hamilton cycle ⇐⇒

at least one of b andc is odd.

Altshuler (1972)proved that all these graphs are hamiltonian.

=⇒ Ifb andc are even, then all Hamilton cycles arenon-bounding.

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 30 / 32

(50)

## Hamiltonicity of three-involution cubic Cayley graphs

Theorem

Let K =Cay(H;x,y,z) be a cubic Cayley graph, where H =hx,y,z |x2=y2=z2 = 1,(xy)3 = (yz)3 = 1, . . .i.

Then K admits abounding Hamilton cycle with respect to the natural associated embedding ⇐⇒ |H| ≡2 (mod 4)or |xz|is even.

Furthemore, if K has a bounding Hamilton cycle (with respect to the natural embedding), then it has a contractible one.

(51)

Thank you!

Roman Nedela and Martin ˇSkoviera Hamilton cycles 15/02/2016 32 / 32

References

Related documents

An investigation was undertaken into the performance of the granular activated carbon (GAC) filters used at the Hamilton Drinking Water Treatment Station (HDWTS)

1) VapC Rv0617 is a toxic protein that exhibits an in vivo bacteriostatic effect when conditionally expressed in M. Their activity appears to be

For n ⫽ 2 we go further and consider all cases where the Hamilton–Jacobi equation admits a second-order constant of the motion, not necessarily associated with orthogonal

We discuss related results along two strands: the problem of finding decompositions of large graphs with high minimum degree and the problem of decomposing bipartite graphs

There is an algorithm run which takes as input a pair (M, x) and activates the algorithm M on input x ; and if it halts, returns the output of that computation.. The universal

A Borel structure M is Borel categorical if any two Borel presentation of it are Borel isomorphic. More generally, one can define the Borel dimension of a Borel structure M to be

We conjecture that: (a) if a group cancels with every countable group, then it cancels with every groups, and so the index set is Π 1 2 ; and (b) the class is Π 1 2 m-hard, i.e.,

At last, in Section 9, we introduce the notion of a partial 3-tree, which is a tree associated with a matroid M; some of whose vertices are labelled by members of a partition of

The easier direction, that the traditional tree-width of a graph G is not smaller than the tree-width of the cycle matroid M ( G ) of G, has been rigorously proved in [2, Lemmas 5.1

We show for each positive integer a that, if M is a minor-closed class of matroids not containing all rank-(a + 1) uni- form matroids, then there exists an integer c such that

It was also shown that if a Banach space X admits an equivalent weak mid-point locally uniformly rotund norm, and every weakly continuous function acting from an α-favourable space

Given the sets {0, 1} and ω in CountSet, assume the exponential object {0, 1} ω exists. The category G-Set is a topos. If Y X is an object in G-Set then a G-action has to be

Given the sets {0, 1} and ω in CountSet, assume the exponential object {0, 1} ω exists. The category G-Set is a topos. If Y X is an object in G-Set then a G-action has to be defined

If the Jacobian is positive everywhere, then a right handed set will be transformed into another right handed set, and the transformation is said to

Moreover, if Rota’s conjecture holds, then representability over a finite field can be finitely axiomatized using sentences in M -logic (Corollary 3.3).. Theorem 1.3 shows this is

'Nice' tangential A&gt;blocks are ones which are supersolvable or at least contain modular hyperplanes.. Lemma 3.2 and Theorem 3.3 show that these properties are inherited

the uniquely defined outer border cycle of M separates one (infinite) background component and a finite number of improper holes from M any inner border cycle of M separates a

Case 1. At the stage we discover this, we will, for simplicity, automatically delete the outcomes whose hypothesis must be wrong. That is if we discover m &lt; A x then we

There is a large body of work regarding the existence of Hamilton cycles in cubic graphs, in particular what combinations of graph-theoretical properties guarantee that a cubic

Obviously, if one of the standard density outcomes is true, then R is satisﬁed, and if one of the gadget outcomes is true, then we will not have a conﬁrmed y for cycle (m, n), but

Then the measure of an angle, m(uvw ), is one more than the number of intervening vertices in the cyclic order at v, either clockwise or counterclockwise, whichever is less.

Work limitations four years following mild traumatic brain injury: A Cohort Study Alice Theadom, PhD, Suzanne Barker-Collo, PhD, Kelly Jones, PhD, Michael Kahan, MD, Braden Te Ao,

In this paper we provide a thorough investigation of total correctness 1 operation re- finement (that is the degenerate case of data refinement in which simulations are