Verification of AMBA Using a Combination of Model Checking and Theorem Proving