YES
ignored inputs:
(COMMENT an explicit substitution calculus for lambda terms )
(COMMENT Example 43 of [ FG07 , doi:10.1016/j.ic.2006.12.002 ] )

NRS:
   [ (0):  |- (sub <[a](app <[]X,[]Y>),[]Z>) -> (app <(sub <[a][]X,[]Z>),(sub <[a][]Y,[]Z>)>),
     (1):  |- (sub <[a]a,[]X>) -> []X,
     (2): a#X |- (sub <[a][]X,[]Y>) -> []X,
     (3): b#Y |- (sub <[a](lam [b][]X),[]Y>) -> (lam [b](sub <[a][]X,[]Y>)) ]
Check confluence by Knuth-Bendix criterion
uniform

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

Problem:
 sub(pair_2(lambda(app(pair_2(X,Y))),Z)) ->
 app(pair_2(sub(pair_2(lambda(X),Z)),sub(pair_2(lambda(Y),Z))))
 sub(pair_2(lambda(diamond()),X)) -> X
 sub(pair_2(lambda(X),Y)) -> X
 sub(pair_2(lambda(lam(lambda(X))),Y)) -> lam(lambda(sub(pair_2(lambda(X),Y))))

Proof:
 LPO Processor:
  precedence:
   sub > lam ~ diamond ~ lambda ~ app ~ pair_2
  problem:
   
  Qed
terminating
check each BCP has alpha-equivalent normal forms or not
BCPs:
(0 on 0): 
   {  |- < (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) <= (sub <[a](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
     a#Y_1,a#X_1 |- < (app <(sub <[a][(a b)]X_1,[]Z_1>),(sub <[a][(a b)]Y_1,[]Z_1>)>) <= (sub <[b](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[b][]X_1,[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(0 on 2): 
   { a#X,a#Y |- < (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>) <= (sub <[a](app <[]X,[]Y>),[]Y_1>) => (app <[]X,[]Y>) >,
     a#Y,a#X,b#Y,b#X |- < (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>) <= (sub <[b](app <[(a b)]X,[(a b)]Y>),[]Y_1>) => (app <[(a b)]X,[(a b)]Y>) > }
(1 on 1): 
   {  |- < []X_1 <= (sub <[b]b,[]X_1>) => []X_1 > }
(2 on 0): 
   { a#X_1,a#Y_1 |- < (app <[]X_1,[]Y_1>) <= (sub <[a](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>) >,
     b#Y_1,a#X_1,a#Y_1,b#X_1 |- < (app <[(a b)]X_1,[(a b)]Y_1>) <= (sub <[b](app <[]X_1,[]Y_1>),[]Z_1>) => (app <(sub <[b][]X_1,[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>) > }
(2 on 2): 
   { a#X_1 |- < []X_1 <= (sub <[a][]X_1,[]Y_1>) => []X_1 >,
     b#X_1,a#X_1 |- < [(a b)]X_1 <= (sub <[b][]X_1,[]Y_1>) => []X_1 > }
(2 on 3): 
   { a#X_1,c#Y_1 |- < (lam [c][]X_1) <= (sub <[a](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[a][]X_1,[]Y_1>)) >,
     a#Y_1,c#X_1 |- < (lam [c][(a c)]X_1) <= (sub <[c](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[c][]X_1,[]Y_1>)) >,
     d#Y_1,c#X_1,a#X_1 |- < (lam [d][(a c)]X_1) <= (sub <[c](lam [d][]X_1),[]Y_1>) => (lam [d](sub <[c][]X_1,[]Y_1>)) > }
(3 on 2): 
   { a#X,b#Y_1 |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[a](lam [b][]X),[]Y_1>) => (lam [b][]X) >,
     a#X,b#Y_1 |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[b](lam [a][(a b)]X),[]Y_1>) => (lam [a][(a b)]X) >,
     c#X,b#Y_1,a#X |- < (lam [b](sub <[a][]X,[]Y_1>)) <= (sub <[c](lam [b][(a c)]X),[]Y_1>) => (lam [b][(a c)]X) > }
(3 on 3): 
   { b#Y_1 |- < (lam [b](sub <[a][]X_1,[]Y_1>)) <= (sub <[a](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[a][]X_1,[]Y_1>)) >,
     b#X_1,b#Y_1,c#Y_1 |- < (lam [b](sub <[a][(b c)]X_1,[]Y_1>)) <= (sub <[a](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[a][]X_1,[]Y_1>)) >,
     a#Y_1,b#Y_1 |- < (lam [b](sub <[a][(a b)]X_1,[]Y_1>)) <= (sub <[b](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[b][]X_1,[]Y_1>)) >,
     a#X_1,b#Y_1 |- < (lam [b](sub <[a][(a c)]X_1,[]Y_1>)) <= (sub <[c](lam [b][]X_1),[]Y_1>) => (lam [b](sub <[c][]X_1,[]Y_1>)) >,
     b#Y_1,a#Y_1,b#X_1 |- < (lam [b](sub <[a][(c a)(a b)]X_1,[]Y_1>)) <= (sub <[c](lam [a][]X_1),[]Y_1>) => (lam [a](sub <[c][]X_1,[]Y_1>)) >,
     a#X_1,c#Y_1,b#Y_1 |- < (lam [b](sub <[a][(b a)(a c)]X_1,[]Y_1>)) <= (sub <[b](lam [c][]X_1),[]Y_1>) => (lam [c](sub <[b][]X_1,[]Y_1>)) >,
     a#X_1,b#Y_1,d#Y_1,b#X_1 |- < (lam [b](sub <[a][(b d)(a c)]X_1,[]Y_1>)) <= (sub <[c](lam [d][]X_1),[]Y_1>) => (lam [d](sub <[c][]X_1,[]Y_1>)) > }
BCP: a#X,a#Y |- <  (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>),   (app <[]X,[]Y>)  >
===> nf(lhs):(app <[]X,[]Y>) and nf(rhs):(app <[]X,[]Y>) are aeq
BCP: a#Y,a#X,b#Y,b#X |- <  (app <(sub <[a][]X,[]Y_1>),(sub <[a][]Y,[]Y_1>)>),   (app <[(a b)]X,[(a b)]Y>)  >
===> nf(lhs):(app <[(a b)]X,[(a b)]Y>) and nf(rhs):(app <[(a b)]X,[(a b)]Y>) are aeq
BCP: a#X_1,a#Y_1 |- <  (app <[]X_1,[]Y_1>),   (app <(sub <[a][]X_1,[]Z_1>),(sub <[a][]Y_1,[]Z_1>)>)  >
===> nf(lhs):(app <[]X_1,[]Y_1>) and nf(rhs):(app <[]X_1,[]Y_1>) are aeq
BCP: b#Y_1,a#X_1,a#Y_1,b#X_1 |- <  (app <[(a b)]X_1,[(a b)]Y_1>),   (app <(sub <[b][]X_1,[]Z_1>),(sub <[b][]Y_1,[]Z_1>)>)  >
===> nf(lhs):(app <[(a b)]X_1,[(a b)]Y_1>) and nf(rhs):(app <[(a b)]X_1,[(a b)]Y_1>) are aeq
BCP: a#X_1,c#Y_1 |- <  (lam [c][]X_1),   (lam [c](sub <[a][]X_1,[]Y_1>))  >
===> nf(lhs):(lam [c][]X_1) and nf(rhs):(lam [c][]X_1) are aeq
BCP: a#Y_1,c#X_1 |- <  (lam [c][(a c)]X_1),   (lam [a](sub <[c][]X_1,[]Y_1>))  >
===> nf(lhs):(lam [c][(a c)]X_1) and nf(rhs):(lam [a][]X_1) are aeq
BCP: d#Y_1,c#X_1,a#X_1 |- <  (lam [d][(a c)]X_1),   (lam [d](sub <[c][]X_1,[]Y_1>))  >
===> nf(lhs):(lam [d][(a c)]X_1) and nf(rhs):(lam [d][(a c)]X_1) are aeq
BCP: a#X,b#Y_1 |- <  (lam [b](sub <[a][]X,[]Y_1>)),   (lam [b][]X)  >
===> nf(lhs):(lam [b][]X) and nf(rhs):(lam [b][]X) are aeq
BCP: a#X,b#Y_1 |- <  (lam [b](sub <[a][]X,[]Y_1>)),   (lam [a][(a b)]X)  >
===> nf(lhs):(lam [b][]X) and nf(rhs):(lam [a][(a b)]X) are aeq
BCP: c#X,b#Y_1,a#X |- <  (lam [b](sub <[a][]X,[]Y_1>)),   (lam [b][(a c)]X)  >
===> nf(lhs):(lam [b][]X) and nf(rhs):(lam [b][(a c)]X) are aeq
all BCPs are joinable
result: YES
time: 29 msec.