This document is a survey of the four papers [H], [Sch], [Com], [FandH]. It gives the relevant background and shows how the papers fit together to form a whole. Material from those papers is repeated only when necessary. As it stands the document is not intended for publication. However, if there is sufficient interest then I may rewrite it to include [H], [Sch], [Com], [FandH] and so form a self contained developement. This material has been around and available in some form for quite a while. This version was slightly modified after attending the Leeds meeting on Proof Theory in July 2009. I have added one or two extra comments in the light of my current knowledge. Contents