YES
ignored inputs:
(COMMENT structural substitution for lambda-mu-terms [ Parigot05 , doi:10.1007/BFb0013061 ] )

NRS:
   [ (0):  |- (ssub <[a]b,c,[]X>) -> b,
     (1): b#X |- (ssub <[a](lam [b][]Y),c,[]X>) -> (lam [b](ssub <[a][]Y,c,[]X>)),
     (2):  |- (ssub <[a](app <[]Y,[]Z>),b,[]X>) -> (app <(ssub <[a][]Y,b,[]X>),(ssub <[a][]Z,b,[]X>)>),
     (3): b#X |- (ssub <[a](mu [b][]Y),c,[]X>) -> (mu [b](ssub <[a][]Y,c,[]X>)),
     (4):  |- (ssub <[a](ind <a,[]Y>),b,[]X>) -> (ind <b,(app <(ssub <[a][]Y,b,[]X>),[]X>)>),
     (5):  |- (ssub <[a](ind <b,[]Y>),c,[]X>) -> (ind <b,(ssub <[a][]Y,c,[]X>)>) ]
Check confluence by parallel closed criterion
left-linear
uniform
BCPs:
(0 on 0(out)): 
   {  |- < b <= (ssub <[a]b,c,[]X_1>) => b >,
      |- < b <= (ssub <[d]b,c,[]X_1>) => b > }
(1 on 1(out)): 
   { b#X_1 |- < (lam [b](ssub <[a][]Y_1,c,[]X_1>)) <= (ssub <[a](lam [b][]Y_1),c,[]X_1>) => (lam [b](ssub <[a][]Y_1,c,[]X_1>)) >,
     b#X_1,d#X_1,b#Y_1 |- < (lam [b](ssub <[a][(b d)]Y_1,c,[]X_1>)) <= (ssub <[a](lam [d][]Y_1),c,[]X_1>) => (lam [d](ssub <[a][]Y_1,c,[]X_1>)) >,
     a#X_1,b#X_1 |- < (lam [b](ssub <[a][(a b)]Y_1,c,[]X_1>)) <= (ssub <[b](lam [a][]Y_1),c,[]X_1>) => (lam [a](ssub <[b][]Y_1,c,[]X_1>)) >,
     b#X_1,a#Y_1 |- < (lam [b](ssub <[a][(a d)]Y_1,c,[]X_1>)) <= (ssub <[d](lam [b][]Y_1),c,[]X_1>) => (lam [b](ssub <[d][]Y_1,c,[]X_1>)) >,
     b#X_1,a#X_1,b#Y_1 |- < (lam [b](ssub <[a][(d a)(a b)]Y_1,c,[]X_1>)) <= (ssub <[d](lam [a][]Y_1),c,[]X_1>) => (lam [a](ssub <[d][]Y_1,c,[]X_1>)) >,
     a#Y_1,d#X_1,b#X_1 |- < (lam [b](ssub <[a][(b a)(a d)]Y_1,c,[]X_1>)) <= (ssub <[b](lam [d][]Y_1),c,[]X_1>) => (lam [d](ssub <[b][]Y_1,c,[]X_1>)) >,
     b#X_1,e#X_1,a#Y_1,b#Y_1 |- < (lam [b](ssub <[a][(b e)(a d)]Y_1,c,[]X_1>)) <= (ssub <[d](lam [e][]Y_1),c,[]X_1>) => (lam [e](ssub <[d][]Y_1,c,[]X_1>)) > }
(2 on 2(out)): 
   {  |- < (app <(ssub <[a][]Y_1,b,[]X_1>),(ssub <[a][]Z_1,b,[]X_1>)>) <= (ssub <[a](app <[]Y_1,[]Z_1>),b,[]X_1>) => (app <(ssub <[a][]Y_1,b,[]X_1>),(ssub <[a][]Z_1,b,[]X_1>)>) >,
     a#Y_1,a#Z_1 |- < (app <(ssub <[a][(a c)]Y_1,b,[]X_1>),(ssub <[a][(a c)]Z_1,b,[]X_1>)>) <= (ssub <[c](app <[]Y_1,[]Z_1>),b,[]X_1>) => (app <(ssub <[c][]Y_1,b,[]X_1>),(ssub <[c][]Z_1,b,[]X_1>)>) > }
(3 on 3(out)): 
   { b#X_1 |- < (mu [b](ssub <[a][]Y_1,c,[]X_1>)) <= (ssub <[a](mu [b][]Y_1),c,[]X_1>) => (mu [b](ssub <[a][]Y_1,c,[]X_1>)) >,
     b#X_1,d#X_1,b#Y_1 |- < (mu [b](ssub <[a][(b d)]Y_1,c,[]X_1>)) <= (ssub <[a](mu [d][]Y_1),c,[]X_1>) => (mu [d](ssub <[a][]Y_1,c,[]X_1>)) >,
     a#X_1,b#X_1 |- < (mu [b](ssub <[a][(a b)]Y_1,c,[]X_1>)) <= (ssub <[b](mu [a][]Y_1),c,[]X_1>) => (mu [a](ssub <[b][]Y_1,c,[]X_1>)) >,
     b#X_1,a#Y_1 |- < (mu [b](ssub <[a][(a d)]Y_1,c,[]X_1>)) <= (ssub <[d](mu [b][]Y_1),c,[]X_1>) => (mu [b](ssub <[d][]Y_1,c,[]X_1>)) >,
     b#X_1,a#X_1,b#Y_1 |- < (mu [b](ssub <[a][(d a)(a b)]Y_1,c,[]X_1>)) <= (ssub <[d](mu [a][]Y_1),c,[]X_1>) => (mu [a](ssub <[d][]Y_1,c,[]X_1>)) >,
     a#Y_1,d#X_1,b#X_1 |- < (mu [b](ssub <[a][(b a)(a d)]Y_1,c,[]X_1>)) <= (ssub <[b](mu [d][]Y_1),c,[]X_1>) => (mu [d](ssub <[b][]Y_1,c,[]X_1>)) >,
     b#X_1,e#X_1,a#Y_1,b#Y_1 |- < (mu [b](ssub <[a][(b e)(a d)]Y_1,c,[]X_1>)) <= (ssub <[d](mu [e][]Y_1),c,[]X_1>) => (mu [e](ssub <[d][]Y_1,c,[]X_1>)) > }
(4 on 4(out)): 
   {  |- < (ind <b,(app <(ssub <[a][]Y_1,b,[]X_1>),[]X_1>)>) <= (ssub <[a](ind <a,[]Y_1>),b,[]X_1>) => (ind <b,(app <(ssub <[a][]Y_1,b,[]X_1>),[]X_1>)>) >,
     a#Y_1 |- < (ind <b,(app <(ssub <[a][(a c)]Y_1,b,[]X_1>),[]X_1>)>) <= (ssub <[c](ind <c,[]Y_1>),b,[]X_1>) => (ind <b,(app <(ssub <[c][]Y_1,b,[]X_1>),[]X_1>)>) > }
(5 on 5(out)): 
   {  |- < (ind <b,(ssub <[a][]Y_1,c,[]X_1>)>) <= (ssub <[a](ind <b,[]Y_1>),c,[]X_1>) => (ind <b,(ssub <[a][]Y_1,c,[]X_1>)>) >,
     a#Y_1 |- < (ind <b,(ssub <[a][(a d)]Y_1,c,[]X_1>)>) <= (ssub <[d](ind <b,[]Y_1>),c,[]X_1>) => (ind <b,(ssub <[d][]Y_1,c,[]X_1>)>) > }
all BCPs are parallel closed
result: YES
time: 18 msec.