NO

Problem 1: 


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

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

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

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

-> Critical pairs info:
<s(s(+(+(y,z),x'))),+(+(z,y),s(s(x')))>   =>  Not trivial, Overlay, Proper, NW0, N1
<+(x,y'),+(+(y',0),x)>   =>  Not trivial, Not overlay, Proper, NW0, N2
<+(x,s(y')),+(+(y',s(0)),x)>   =>  Not trivial, Not overlay, Proper, NW0, N3
<+(y,z),+(+(z,y),0)>   =>  Not trivial, Overlay, Proper, NW0, N4
<+(x,+(+(z',y'),x')),+(+(+(y',z'),x'),x)>   =>  Not trivial, Not overlay, Proper, NW0, N5
<+(x,s(s(+(y',x')))),+(+(y',s(s(x'))),x)>   =>  Not trivial, Not overlay, Proper, NW0, N6
<s(+(y,z)),+(+(z,y),s(0))>   =>  Not trivial, 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: s(s(+(+(y,z),x')))
Nodes: [0]
Edges: []
ID: 0 => ('s(s(+(+(y,z),x')))', D0)
t: +(+(z,y),s(s(x')))
Nodes: [0]
Edges: []
ID: 0 => ('+(+(z,y),s(s(x')))', D0)
s(s(+(+(y,z),x'))) ->* no union *<- +(+(z,y),s(s(x')))
"Not joinable"

The problem is not confluent.