Update instructions and basic rules are defined as in 3.1, except that terms may have free variables, and guards are defined as above. In addition, we have the following third rule constructor.