Added a labelled operational semantics and some sketched theorem regarding it