YES

Problem 1: 


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


Problem 1: 

Problem 1: 

Modular Confluence Combinations Decomposition Procedure:
TRS combination:
{+(x,0) -> x
 +(x,s(y)) -> s(+(x,y))}
{-(0,x) -> 0
 -(s(x),s(y)) -> -(x,y)
 -(x,0) -> x}
Not disjoint
Constructor-sharing
Not composable
Left linear
Not layer-preserving
TRS1
Just (VAR x y)
(STRATEGY CONTEXTSENSITIVE
(+ 1 2)
(0)
(s 1)
)
(RULES
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
)

TRS2
Just (VAR x y)
(STRATEGY CONTEXTSENSITIVE
(- 1 2)
(0)
(s 1)
)
(RULES
-(0,x) -> 0
-(s(x),s(y)) -> -(x,y)
-(x,0) -> x
)


The problem is decomposed in 2 subproblems.

Problem 1.1: 


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


Problem 1.1: 

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

Problem 1.1: 
Linearity Procedure:
Linear?
YES

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

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

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

-> Unifications:


-> Critical pairs info:


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


The problem is confluent.

Problem 1.2: 


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


Problem 1.2: 

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

Problem 1.2: 
Linearity Procedure:
Linear?
YES

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x y)
(REPLACEMENT-MAP
(- 1, 2)
(0)
(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.