MAYBE
ignored inputs:
(COMMENT completed version of Example 6 of [ FR12 , doi:10.1007/978-3-642-31585-5_21 ] )

NRS:
   [ (0): a#F |- (sigma <(0 <>),[a](app <[]F,a>)>) -> (0 <>),
     (1): a#F |- (sigma <(s []N),[a](app <[]F,a>)>) -> (+ <(app <[]F,(s []N)>),(sigma <[]N,[a](app <[]F,a>)>)>),
     (2):  |- (id []X) -> []X,
     (3):  |- (app <(id <>),[]X>) -> (id []X),
     (4):  |- (app <<>,[]X>) -> []X,
     (5):  |- (sigma <(0 <>),[a]a>) -> (0 <>),
     (6):  |- (sigma <(s []N),[a]a>) -> (+ <(s []N),(sigma <[]N,[a]a>)>) ]
Check confluence by parallel closed criterion
left-linear
uniform
BCPs:
(0 on 0(out)): 
   { a#F_1 |- < (0 <>) <= (sigma <(0 <>),[a](app <[]F_1,a>)>) => (0 <>) >,
     b#F_1,a#F_1 |- < (0 <>) <= (sigma <(0 <>),[b](app <[]F_1,b>)>) => (0 <>) > }
(1 on 1(out)): 
   { a#F_1 |- < (+ <(app <[]F_1,(s []N_1)>),(sigma <[]N_1,[a](app <[]F_1,a>)>)>) <= (sigma <(s []N_1),[a](app <[]F_1,a>)>) => (+ <(app <[]F_1,(s []N_1)>),(sigma <[]N_1,[a](app <[]F_1,a>)>)>) >,
     b#F_1,a#F_1 |- < (+ <(app <[(a b)]F_1,(s []N_1)>),(sigma <[]N_1,[a](app <[(a b)]F_1,a>)>)>) <= (sigma <(s []N_1),[b](app <[]F_1,b>)>) => (+ <(app <[]F_1,(s []N_1)>),(sigma <[]N_1,[b](app <[]F_1,b>)>)>) > }
(2 on 2(out)): 
   {  |- < []X_1 <= (id []X_1) => []X_1 > }
(2 on 3(in)): 
   {  |- < (app <<>,[]X_1>) <= (app <(id <>),[]X_1>) => (id []X_1) > }
(3 on 0(in)): 
   {  |- < (sigma <(0 <>),[a](id a)>) <= (sigma <(0 <>),[a](app <(id <>),a>)>) => (0 <>) >,
      |- < (sigma <(0 <>),[b](id b)>) <= (sigma <(0 <>),[b](app <(id <>),b>)>) => (0 <>) > }
(3 on 1(in)): 
   {  |- < (sigma <(s []N_1),[a](id a)>) <= (sigma <(s []N_1),[a](app <(id <>),a>)>) => (+ <(app <(id <>),(s []N_1)>),(sigma <[]N_1,[a](app <(id <>),a>)>)>) >,
      |- < (sigma <(s []N_1),[b](id b)>) <= (sigma <(s []N_1),[b](app <(id <>),b>)>) => (+ <(app <(id <>),(s []N_1)>),(sigma <[]N_1,[b](app <(id <>),b>)>)>) > }
(3 on 3(out)): 
   {  |- < (id []X_1) <= (app <(id <>),[]X_1>) => (id []X_1) > }
(4 on 0(in)): 
   {  |- < (sigma <(0 <>),[a]a>) <= (sigma <(0 <>),[a](app <<>,a>)>) => (0 <>) >,
      |- < (sigma <(0 <>),[b]b>) <= (sigma <(0 <>),[b](app <<>,b>)>) => (0 <>) > }
(4 on 1(in)): 
   {  |- < (sigma <(s []N_1),[a]a>) <= (sigma <(s []N_1),[a](app <<>,a>)>) => (+ <(app <<>,(s []N_1)>),(sigma <[]N_1,[a](app <<>,a>)>)>) >,
      |- < (sigma <(s []N_1),[b]b>) <= (sigma <(s []N_1),[b](app <<>,b>)>) => (+ <(app <<>,(s []N_1)>),(sigma <[]N_1,[b](app <<>,b>)>)>) > }
(4 on 4(out)): 
   {  |- < []X_1 <= (app <<>,[]X_1>) => []X_1 > }
(5 on 5(out)): 
   {  |- < (0 <>) <= (sigma <(0 <>),[a]a>) => (0 <>) >,
      |- < (0 <>) <= (sigma <(0 <>),[b]b>) => (0 <>) > }
(6 on 6(out)): 
   {  |- < (+ <(s []N_1),(sigma <[]N_1,[a]a>)>) <= (sigma <(s []N_1),[a]a>) => (+ <(s []N_1),(sigma <[]N_1,[a]a>)>) >,
      |- < (+ <(s []N_1),(sigma <[]N_1,[a]a>)>) <= (sigma <(s []N_1),[b]b>) => (+ <(s []N_1),(sigma <[]N_1,[b]b>)>) > }
inBCP:  |- <  (app <<>,[]X_1>),   (id []X_1)  > is not closed
failed to show all BCPs are parallel closed
result: MAYBE
time: 13 msec.