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 orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
a proper overlap exists
2-3
 |- < (app <<>,[]X_1>) <= (app <(id <>),[]X_1>) => (id []X_1) >
found proper overlaps
result: MAYBE
time: 3 msec.