Context-free grammar for unary addition