Their grammar's a bit off, since they have:<p><pre><code> <bool> ::= T | F | IsZero <num>
<num> ::= O
<arith> ::= Succ <num> | Pred <num>
</code></pre>
Here `<num>` can only ever be `O`, so that's the only valid argument for `IsZero`, `Succ` and `Pred`. I would put `O` into `<arith>`, get rid of `<num>` and replace all references to it with `<arith>`.<p>That doesn't affect the actual implementation, since (as they say right after) "For simplicity, we merge all them together in a single Term."