DEFABBREV : IF IF is a unique form It provides lazy evaluation In the theorem prover it causes a case split Symbolic simulation is a unique application Specify state of control variables Derive behavior of data variables IF statements can cause problems for symbolic simulation