Vorobyov, S.(1998). The undecidability of the first-order theories of one step rewriting in linear canonical systems (MPI-I-1998-2-009). Saarbrücken: Max-Planck-Institut für Informatik.