added congruence simulation and fixed some bugs in traslation to lts