Their grammar's a bit off, since they have:

    <bool>  ::= T | F | IsZero <num>
    <num>   ::= O
    <arith> ::= Succ <num> | Pred <num>

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>`.

That doesn't affect the actual implementation, since (as they say right after) "For simplicity, we merge all them together in a single Term."