Structural Operational Semantics with transitivity rules and execution time

We define an structural operational semantics of the core of an imperative language. It has a measure in the transitions corresponding to the number of steps of evaluation that takes place in the transition (from the point of view of usual complexity theory) and transitivity rules that allow to prove in the theory what is usually proved in the meta-theory.