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

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

Problem:
 sigma(pair_2(0(pair_0()),lambda(app(pair_2(F,diamond()))))) -> 0(pair_0())
 sigma(pair_2(s(N),lambda(app(pair_2(F,diamond()))))) ->
 +(pair_2(app(pair_2(F,s(N))),sigma(pair_2(N,lambda(app(pair_2(F,diamond())))))))
 id(X) -> X
 app(pair_2(id(pair_0()),X)) -> id(X)
 app(pair_2(pair_0(),X)) -> X
 sigma(pair_2(0(pair_0()),lambda(diamond()))) -> 0(pair_0())
 sigma(pair_2(s(N),lambda(diamond()))) -> +(pair_2(s(N),sigma(pair_2(N,lambda(diamond())))))

Proof:
 LPO Processor:
  precedence:
   sigma > pair_2 > id ~ + ~ s ~ lambda ~ app ~ diamond ~ 0 ~ pair_0
  problem:
   
  Qed
terminating
check each BCP has alpha-equivalent normal forms or not
BCPs:
(0 on 0): 
   { a#F_1 |- < (0 <>) <= (sigma <(0 <>),[a](app <[]F_1,a>)>) => (0 <>) >,
     b#F_1,a#F_1 |- < (0 <>) <= (sigma <(0 <>),[b](app <[]F_1,b>)>) => (0 <>) > }
(1 on 1): 
   { a#F_1 |- < (+ <(app <[]F_1,(s []N_1)>),(sigma <[]N_1,[a](app <[]F_1,a>)>)>) <= (sigma <(s []N_1),[a](app <[]F_1,a>)>) => (+ <(app <[]F_1,(s []N_1)>),(sigma <[]N_1,[a](app <[]F_1,a>)>)>) >,
     b#F_1,a#F_1 |- < (+ <(app <[(a b)]F_1,(s []N_1)>),(sigma <[]N_1,[a](app <[(a b)]F_1,a>)>)>) <= (sigma <(s []N_1),[b](app <[]F_1,b>)>) => (+ <(app <[]F_1,(s []N_1)>),(sigma <[]N_1,[b](app <[]F_1,b>)>)>) > }
(2 on 2): 
   {  |- < []X_1 <= (id []X_1) => []X_1 > }
(2 on 3): 
   {  |- < (app <<>,[]X_1>) <= (app <(id <>),[]X_1>) => (id []X_1) > }
(3 on 0): 
   {  |- < (sigma <(0 <>),[b](id b)>) <= (sigma <(0 <>),[b](app <(id <>),b>)>) => (0 <>) > }
(3 on 1): 
   {  |- < (sigma <(s []N_1),[b](id b)>) <= (sigma <(s []N_1),[b](app <(id <>),b>)>) => (+ <(app <(id <>),(s []N_1)>),(sigma <[]N_1,[b](app <(id <>),b>)>)>) > }
(3 on 3): 
   {  |- < (id []X_1) <= (app <(id <>),[]X_1>) => (id []X_1) > }
(4 on 0): 
   {  |- < (sigma <(0 <>),[b]b>) <= (sigma <(0 <>),[b](app <<>,b>)>) => (0 <>) > }
(4 on 1): 
   {  |- < (sigma <(s []N_1),[b]b>) <= (sigma <(s []N_1),[b](app <<>,b>)>) => (+ <(app <<>,(s []N_1)>),(sigma <[]N_1,[b](app <<>,b>)>)>) > }
(4 on 4): 
   {  |- < []X_1 <= (app <<>,[]X_1>) => []X_1 > }
(5 on 5): 
   {  |- < (0 <>) <= (sigma <(0 <>),[b]b>) => (0 <>) > }
(6 on 6): 
   {  |- < (+ <(s []N_1),(sigma <[]N_1,[a]a>)>) <= (sigma <(s []N_1),[a]a>) => (+ <(s []N_1),(sigma <[]N_1,[a]a>)>) >,
      |- < (+ <(s []N_1),(sigma <[]N_1,[a]a>)>) <= (sigma <(s []N_1),[b]b>) => (+ <(s []N_1),(sigma <[]N_1,[b]b>)>) > }
BCP:  |- <  (app <<>,[]X_1>),   (id []X_1)  >
===> nf(lhs):[]X_1 and nf(rhs):[]X_1 are aeq
BCP:  |- <  (sigma <(0 <>),[b](id b)>),   (0 <>)  >
===> nf(lhs):(0 <>) and nf(rhs):(0 <>) are aeq
BCP:  |- <  (sigma <(s []N_1),[b](id b)>),   (+ <(app <(id <>),(s []N_1)>),(sigma <[]N_1,[b](app <(id <>),b>)>)>)  >
===> nf(lhs):(+ <(s []N_1),(sigma <[]N_1,[c]c>)>) and nf(rhs):(+ <(s []N_1),(sigma <[]N_1,[b]b>)>) are aeq
BCP:  |- <  (sigma <(0 <>),[b]b>),   (0 <>)  >
===> nf(lhs):(0 <>) and nf(rhs):(0 <>) are aeq
BCP:  |- <  (sigma <(s []N_1),[b]b>),   (+ <(app <<>,(s []N_1)>),(sigma <[]N_1,[b](app <<>,b>)>)>)  >
===> nf(lhs):(+ <(s []N_1),(sigma <[]N_1,[c]c>)>) and nf(rhs):(+ <(s []N_1),(sigma <[]N_1,[b]b>)>) are aeq
all BCPs are joinable
result: YES
time: 19 msec.