Incremental Specification
Step 2 and Step 3: Enumeration part and elimination part are specified