NO
ignored inputs:
(COMMENT 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) ]
Check confluence by Knuth-Bendix criterion
uniform

writing to temporary file...
./run_snprover.sh ./SMLNJ-dZTJIB.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)

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) > }
BCP:  |- <  (app <<>,[]X_1>),   (id []X_1)  >
===> nf(lhs):(app <<>,[]X_1>) and nf(rhs):[]X_1 are not aeq
some BCP is not joinable
result: NO
time: 9 msec.