Finite and infinite implementation of transition systems

A system T is defined as implementing a system S if every infinite execution of T leads to the same observations as some infinite execution of S. System T implements S finitely if every finite execution of T leads to the same observations as some finite execution of S. It is proved that, under certain conditions on the implemented system, finite implementation implies implementation. The proof uses König's lemma. It is shown that the conditions are essential.