trace refinements

[fra...@gmail.com]

Hello,

I have a machine  M1 that evolves by perfoming  the two operations Op1, Op2 in sequence.
And I have a machine M2 that evolves by perfoming, in sequence the operations Op1, Internal1,Internal2, Op2.

Is thwre a way to verify that M2 is a trace refiniment of M1 if we ignore the internal operations  Internal1, Internal2 ?

Regards
  Franco