Their grammar's a bit off, since they have: <bool> ::= T | F | IsZero <num> <num> ::= O <arith> ::= Succ <num> | Pred <num> Here `<num>` can on

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