YES
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 Knuth-Bendix criterion
uniform

writing to temporary file...
./run_snprover.sh ./SMLNJ-V2JD2n.trs
YES

Problem:
 lam(lambda(app(pair_2(X,diamond())))) -> X
 app(pair_2(bot(pair_0()),Y)) -> bot(pair_0())
 lam(lambda(bot(pair_0()))) -> bot(pair_0())

Proof:
 DP Processor:
  DPs:
   
  TRS:
   lam(lambda(app(pair_2(X,diamond())))) -> X
   app(pair_2(bot(pair_0()),Y)) -> bot(pair_0())
   lam(lambda(bot(pair_0()))) -> bot(pair_0())
  Qed
terminating
check each BCP has alpha-equivalent normal forms or not
BCPs:
(0 on 0): 
   { a#X_1 |- < []X_1 <= (lam [a](app <[]X_1,a>)) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (lam [b](app <[]X_1,b>)) => []X_1 > }
(1 on 0): 
   {  |- < (lam [b](bot <>)) <= (lam [b](app <(bot <>),b>)) => (bot <>) > }
(1 on 1): 
   {  |- < (bot <>) <= (app <(bot <>),[]Y_1>) => (bot <>) > }
(2 on 2): 
   {  |- < (bot <>) <= (lam [b](bot <>)) => (bot <>) > }
BCP:  |- <  (lam [b](bot <>)),   (bot <>)  >
===> nf(lhs):(bot <>) and nf(rhs):(bot <>) are aeq
all BCPs are joinable
result: YES
time: 4 msec.