Contraction based proof methods for a delay-insensitive algebra

We define a metric for delay insensitive processes. We derive metric properties of operators in a delay insensitive algebra, and use these properties to formalize the notion of "input guardedness".We also derive a method to verify whether a function composed of operators is contracting with regard to its process arguments. We define two relations on processes, and use these relations to derive proof methods for proving equality and refinement. Both proof methods can be used in linear derivations. We present the proof methods in a simple format, that can easily be implemented in proof verification tools. We give an example of the proof method for proving equality by the derivation of a component based design of an n-place delay-insensitive buffer.