YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(- 1, 2)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
-(0,x) -> 0
-(s(x),s(y)) -> -(x,y)
-(x,0) -> x
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
Linearity Procedure:
Linear?
YES

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(- 1, 2)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
-(0,x) -> 0
-(s(x),s(y)) -> -(x,y)
-(x,0) -> x
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 -(0,x) -> 0
 -(s(x),s(y)) -> -(x,y)
 -(x,0) -> x
-> Vars:
 x, x, y, x

-> Rlps:
 (rule: -(0,x) -> 0, id: 1, possubterms: -(0,x)->[], 0->[1])
 (rule: -(s(x),s(y)) -> -(x,y), id: 2, possubterms: -(s(x),s(y))->[], s(x)->[1], s(y)->[2])
 (rule: -(x,0) -> x, id: 3, possubterms: -(x,0)->[], 0->[2])

-> Unifications:
(R3 unifies with R1 at p: [], l: -(x,0), lp: -(x,0), sig: {x -> 0,x' -> 0}, l': -(0,x'), r: x, r': 0)

-> Critical pairs info:
<0,0>   =>  Trivial, Overlay, Proper, NW0, N1

-> Problem conclusions:
 Left linear, Right linear, Linear
 Weakly orthogonal, Almost orthogonal, Not orthogonal
 Huet-Levy confluent, Not Newman confluent
 R is a TRS 


The problem is confluent.