MAYBE
ignored inputs:
(COMMENT 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) ]
Check confluence by strongly closed criterion
not linear
result: MAYBE
time: 0 msec.