Bisimulation proof methods for mobile ambients