YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x y)
(REPLACEMENT-MAP
(- 1, 2)
(d 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
-(d(x),y) -> -(x,s(y))
-(0,0) -> 0
-(s(x),0) -> s(x)
-(s(x),s(y)) -> -(x,y)
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> 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)
(d 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
-(d(x),y) -> -(x,s(y))
-(0,0) -> 0
-(s(x),0) -> s(x)
-(s(x),s(y)) -> -(x,y)
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> x
)
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

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

-> Unifications:
(R1 unifies with R6 at p: [1], l: -(d(x),y), lp: d(x), sig: {x -> s(x')}, l': d(s(x')), r: -(x,s(y)), r': x')
(R5 unifies with R1 at p: [], l: -(x,s(y)), lp: -(x,s(y)), sig: {x -> d(x'),y' -> s(y)}, l': -(d(x'),y'), r: -(d(x),y), r': -(x',s(y')))
(R5 unifies with R4 at p: [], l: -(x,s(y)), lp: -(x,s(y)), sig: {x -> s(x'),y -> y'}, l': -(s(x'),s(y')), r: -(d(x),y), r': -(x',y'))

-> Critical pairs info:
<-(x',s(s(y))),-(d(d(x')),y)>   =>  Not trivial, Overlay, Proper, NW0, N1
<-(x',y),-(s(x'),s(y))>   =>  Not trivial, Not overlay, Proper, NW0, N2
<-(x',y'),-(d(s(x')),y')>   =>  Not trivial, Overlay, Proper, NW0, N3

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



The problem is decomposed in 3 subproblems.

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y x' y')
(REPLACEMENT-MAP
(- 1, 2)
(d 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
-(d(x),y) -> -(x,s(y))
-(0,0) -> 0
-(s(x),0) -> s(x)
-(s(x),s(y)) -> -(x,y)
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> x
)
Critical Pairs:
<-(x',s(s(y))),-(d(d(x')),y)>   =>  Not trivial, Overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: -(x',s(s(y)))
Nodes: [0,1,2]
Edges: [(0,1),(1,0),(1,2),(2,1)]
ID: 0 => ('-(x',s(s(y)))', D0)
ID: 1 => ('-(d(x'),s(y))', D1, R5, P[], S{x11 -> x', x12 -> s(y)}), NR: '-(d(x'),s(y))'
ID: 2 => ('-(d(d(x')),y)', D2, R5, P[], S{x11 -> d(x'), x12 -> y}), NR: '-(d(d(x')),y)'
t: -(d(d(x')),y)
Nodes: [0,1,2]
Edges: [(0,1),(1,0),(1,2),(2,1)]
ID: 0 => ('-(d(d(x')),y)', D0)
ID: 1 => ('-(d(x'),s(y))', D1, R1, P[], S{x6 -> d(x'), x7 -> y}), NR: '-(d(x'),s(y))'
ID: 2 => ('-(x',s(s(y)))', D2, R1, P[], S{x6 -> x', x7 -> s(y)}), NR: '-(x',s(s(y)))'
SNodesPath1: -(x',s(s(y)))
TNodesPath1: -(d(d(x')),y) -> -(d(x'),s(y)) -> -(x',s(s(y)))
SNodesPath2: -(x',s(s(y))) -> -(d(x'),s(y)) -> -(d(d(x')),y)
TNodesPath2: -(d(d(x')),y)
-(x',s(s(y))) ->= -(x',s(s(y))) *<- -(d(d(x')),y)
-(d(d(x')),y) ->= -(d(d(x')),y) *<- -(x',s(s(y)))
"Strongly closed critical pair"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y x' y')
(REPLACEMENT-MAP
(- 1, 2)
(d 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
-(d(x),y) -> -(x,s(y))
-(0,0) -> 0
-(s(x),0) -> s(x)
-(s(x),s(y)) -> -(x,y)
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> x
)
Critical Pairs:
<-(x',y),-(s(x'),s(y))>   =>  Not trivial, Not overlay, Proper, NW0, N2
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: -(x',y)
Nodes: [0]
Edges: []
ID: 0 => ('-(x',y)', D0)
t: -(s(x'),s(y))
Nodes: [0,1,2]
Edges: [(0,1),(0,2),(2,0),(2,1)]
ID: 0 => ('-(s(x'),s(y))', D0)
ID: 1 => ('-(x',y)', D1, R4, P[], S{x9 -> x', x10 -> y}), NR: '-(x',y)'
ID: 2 => ('-(d(s(x')),y)', D1, R5, P[], S{x11 -> s(x'), x12 -> y}), NR: '-(d(s(x')),y)'
SNodesPath1: -(x',y)
TNodesPath1: -(s(x'),s(y)) -> -(x',y)
SNodesPath2: -(x',y)
TNodesPath2: -(s(x'),s(y)) -> -(x',y)
-(x',y) ->= -(x',y) *<- -(s(x'),s(y))
-(s(x'),s(y)) ->= -(x',y) *<- -(x',y)
"Strongly closed critical pair"

The problem is confluent.

Problem 1.3: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y x' y')
(REPLACEMENT-MAP
(- 1, 2)
(d 1)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
-(d(x),y) -> -(x,s(y))
-(0,0) -> 0
-(s(x),0) -> s(x)
-(s(x),s(y)) -> -(x,y)
-(x,s(y)) -> -(d(x),y)
d(s(x)) -> x
)
Critical Pairs:
<-(x',y'),-(d(s(x')),y')>   =>  Not trivial, Overlay, Proper, NW0, N3
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Strong Confluence Procedure:
-> Rewritings:
s: -(x',y')
Nodes: [0]
Edges: []
ID: 0 => ('-(x',y')', D0)
t: -(d(s(x')),y')
Nodes: [0,1,2]
Edges: [(0,1),(0,2),(1,0),(1,2)]
ID: 0 => ('-(d(s(x')),y')', D0)
ID: 1 => ('-(s(x'),s(y'))', D1, R1, P[], S{x6 -> s(x'), x7 -> y'}), NR: '-(s(x'),s(y'))'
ID: 2 => ('-(x',y')', D1, R6, P[1], S{x13 -> x'}), NR: 'x''
SNodesPath1: -(x',y')
TNodesPath1: -(d(s(x')),y') -> -(s(x'),s(y')) -> -(x',y')
SNodesPath2: -(x',y')
TNodesPath2: -(d(s(x')),y') -> -(s(x'),s(y')) -> -(x',y')
-(x',y') ->= -(x',y') *<- -(d(s(x')),y')
-(d(s(x')),y') ->= -(x',y') *<- -(x',y')
"Strongly closed critical pair"

The problem is confluent.