Application and Verification of Local Nonsemantic-Preserving Transformations in System Design