YES
ignored inputs:
(COMMENT alpha reduction rule of the lambda calculus )

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