An experience in proving regular networks of processes by modular model checking