YES

Problem 1: 


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

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

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

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

-> Critical pairs info:
<y',max(y',0)>   =>  Not trivial, Overlay, Proper, NW0, N1
<0,0>   =>  Trivial, Overlay, Proper, NW0, N2
<x',max(0,x')>   =>  Not trivial, Overlay, Proper, NW0, N3
<s(max(x',y')),max(s(y'),s(x'))>   =>  Not trivial, Overlay, Proper, NW0, N4

-> 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
(max 1, 2)
(0)
(fSNonEmpty)
(s 1)
)
(RULES
max(0,y) -> y
max(s(x),s(y)) -> s(max(x,y))
max(x,0) -> x
max(x,y) -> max(y,x)
)
Critical Pairs:
<y',max(y',0)>   =>  Not trivial, Overlay, Proper, NW0, N1
Linear:YES
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

The problem is confluent.

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

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

The problem is confluent.

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

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

The problem is confluent.