refactoring
added multi-threaded operational semantics, strong low bisimulation and theorem "union of all strong low bisimulation is a strong low bisimulation"