YES
ignored inputs:
(COMMENT Example 4.7 of [ Suzuki et al. , PPL 2014 ] )

NRS:
   [ (0): a#X |- (f []X) -> [a][]X ]
Check confluence by strongly closed criterion
linear
uniform
BCPs:
(0 on 0): 
   { a#X_1 |- < [a][]X_1 <= (f []X_1) => [a][]X_1 >,
     a#X_1,b#X_1 |- < [a][]X_1 <= (f []X_1) => [b][]X_1 > }
all BCPs are strongly closed
result: YES
time: 0 msec.