NO

Problem 1: 


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


Problem 1: 

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

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

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

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

-> Unifications:
(R1 unifies with R4 at p: [1], l: +(s(x),y), lp: s(x), sig: {x -> s(x')}, l': s(s(x')), r: s(+(x,y)), r': x')
(R3 unifies with R1 at p: [], l: +(x,+(y,z)), lp: +(x,+(y,z)), sig: {x -> s(x'),y' -> +(y,z)}, l': +(s(x'),y'), r: +(+(z,y),x), r': s(+(x',y')))
(R3 unifies with R2 at p: [], l: +(x,+(y,z)), lp: +(x,+(y,z)), sig: {x -> 0,y' -> +(y,z)}, l': +(0,y'), r: +(+(z,y),x), r': y')
(R3 unifies with R1 at p: [2], l: +(x,+(y,z)), lp: +(y,z), sig: {y -> s(x'),z -> y'}, l': +(s(x'),y'), r: +(+(z,y),x), r': s(+(x',y')))
(R3 unifies with R2 at p: [2], l: +(x,+(y,z)), lp: +(y,z), sig: {y -> 0,z -> y'}, l': +(0,y'), r: +(+(z,y),x), r': y')
(R3 unifies with R3 at p: [2], l: +(x,+(y,z)), lp: +(y,z), sig: {y -> x',z -> +(y',z')}, l': +(x',+(y',z')), r: +(+(z,y),x), r': +(+(z',y'),x'))
(R4 unifies with R4 at p: [1], l: s(s(x)), lp: s(x), sig: {x -> s(x')}, l': s(s(x')), r: x, r': x')

-> Critical pairs info:
<+(x,y'),+(+(y',0),x)>   =>  Not trivial, Not overlay, Proper, NW0, N1
<+(x,+(+(z',y'),x')),+(+(+(y',z'),x'),x)>   =>  Not trivial, Not overlay, Proper, NW0, N2
<+(y,z),+(+(z,y),0)>   =>  Not trivial, Overlay, Proper, NW0, N3
<+(x',y),s(+(s(x'),y))>   =>  Not trivial, Not overlay, Proper, NW0, N4
<+(x,s(+(x',y'))),+(+(y',s(x')),x)>   =>  Not trivial, Not overlay, Proper, NW0, N5
<s(+(x',+(y,z))),+(+(z,y),s(x'))>   =>  Not trivial, Overlay, Proper, NW0, N6
<s(x'),s(x')>   =>  Trivial, Not overlay, Proper, NW0, N7

-> 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 


Problem 1: 
No Convergence Brute Force Procedure:
-> Rewritings:
s: +(x,y')
Nodes: [0]
Edges: []
ID: 0 => ('+(x,y')', D0)
t: +(+(y',0),x)
Nodes: [0]
Edges: []
ID: 0 => ('+(+(y',0),x)', D0)
+(x,y') ->* no union *<- +(+(y',0),x)
"Not joinable"

The problem is not confluent.