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

NRS:
   [ (0): a#X |- (f []X) -> [a][]X ]
Check confluence by orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
no proper overlaps
result: YES
time: 0 msec.