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

NRS:
   [ (0): a#X |- (lam [a](app <[]X,a>)) -> []X,
     (1):  |- (app <(bot <>),[]Y>) -> (bot <>),
     (2):  |- (lam [a](bot <>)) -> (bot <>) ]
Check confluence by orthogonality
abstract skeleton preserving
left-linear
check proper overlapping
a proper overlap exists
1-0
 |- < (lam [b](bot <>)) <= (lam [b](app <(bot <>),b>)) => (bot <>) >
found proper overlaps
result: MAYBE
time: 0 msec.