With the natural semantics in mind, let's see an example.
To complete the derivation tree, we still need to evaluate where :