Fixed small mistakes.
Proven equivalence between one step of operational and one step of labelled.