Integrating Module Checking and Deduction in a Formal Proof for the Perlman Spanning Tree Protocol (STP)