Mechanical verification support is desirable for most correctness proofs arising in compiler development. The emphasis of ProCoS II is on timing. The main effort in proofs for compiler correctness concerns the correctness of the code-generator specification. Since this essentially depends on the semantic model, a proof support system is only suitable, if the model can be easily formalised in the system. We will investigate appropriate tools concerning their applicability. [13][12] describe how transition systems that are used for structural operational semantics definitions can be embedded into term rewriting systems in general and the Larch-based LP proof system in particular.