YES ignored inputs: (COMMENT Example 4.7 of [ Suzuki et al. , PPL 2014 ] ) NRS: [ (0): a#X |- (f []X) -> [a][]X ] Check confluence by parallel closed criterion left-linear uniform BCPs: (0 on 0(out)): { 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 parallel closed result: YES time: 0 msec.