YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(a 1)
(b 1)
(c 1)
(fSNonEmpty)
)
(RULES
a(a(x)) -> a(b(a(x)))
b(a(b(x))) -> a(c(a(x)))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

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

Problem 1: 
CSR Converter From Canonical u-Replacement Map Procedure [CSUR20]:

Original Replacement Map:
(a 1)
(b 1)
(c 1)
(fSNonEmpty)

New Replacement Map:
(a 1)
(b 1)
(c)
(fSNonEmpty)

New problem:

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(a 1)
(b 1)
(c)
(fSNonEmpty)
)
(RULES
a(a(x)) -> a(b(a(x)))
b(a(b(x))) -> a(c(a(x)))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 
Termination Procedure:
Terminating?
YES

Problem 1: 

(VAR vu95NonEmpty vNonEmpty x)
(STRATEGY CONTEXTSENSITIVE
(a 1)
(b 1)
(c)
(fSNonEmpty)
)
(RULES
a(a(x)) -> a(b(a(x)))
b(a(b(x))) -> a(c(a(x)))
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 A(a(x)) -> A(b(a(x)))
 A(a(x)) -> B(a(x))
-> Rules:
 a(a(x)) -> a(b(a(x)))
 b(a(b(x))) -> a(c(a(x)))
-> Unhiding Rules:
 Empty

Problem 1: 

SCC Processor:
-> Pairs:
 A(a(x)) -> A(b(a(x)))
 A(a(x)) -> B(a(x))
-> Rules:
 a(a(x)) -> a(b(a(x)))
 b(a(b(x))) -> a(c(a(x)))
-> Unhiding rules:
 Empty
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 A(a(x)) -> A(b(a(x)))
->->-> Rules:
 a(a(x)) -> a(b(a(x)))
 b(a(b(x))) -> a(c(a(x)))
->->-> Unhiding rules:
 Empty

Problem 1: 

Reduction Triple Processor:
-> Pairs:
 A(a(x)) -> A(b(a(x)))
-> Rules:
 a(a(x)) -> a(b(a(x)))
 b(a(b(x))) -> a(c(a(x)))
-> Unhiding rules:
 Empty
-> Usable rules:
 a(a(x)) -> a(b(a(x)))
 b(a(b(x))) -> a(c(a(x)))
->Interpretation type:
 Linear
->Coefficients:
 All rationals
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[a](X) = 2.X + 2
[b](X) = 1/2.X + 1/2
[c](X) = 0
[fSNonEmpty] = 0
[A](X) = 1/2.X
[B](X) = 0

Problem 1: 

Basic Processor:
-> Pairs:
 Empty
-> Rules:
 a(a(x)) -> a(b(a(x)))
 b(a(b(x))) -> a(c(a(x)))
-> Unhiding rules:
 Empty
-> Result:
 Set P is empty

The problem is finite.


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(a 1)
(b 1)
(c)
(fSNonEmpty)
)
(RULES
a(a(x)) -> a(b(a(x)))
b(a(b(x))) -> a(c(a(x)))
)
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy NW Procedure:
-> Rules:
 a(a(x)) -> a(b(a(x)))
 b(a(b(x))) -> a(c(a(x)))
-> Vars:
 x, x
-> UVars:
 (UV-RuleId: 1, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: [])
 (UV-RuleId: 2, UV-LActive: [x], UV-RActive: [x], UV-LFrozen: [], UV-RFrozen: [])

-> Rlps:
 (rule: a(a(x)) -> a(b(a(x))), id: 1, possubterms: a(a(x))->[], a(x)->[1])
 (rule: b(a(b(x))) -> a(c(a(x))), id: 2, possubterms: b(a(b(x)))->[], a(b(x))->[1], b(x)->[1, 1])

-> Unifications:
(R1 unifies with R1 at p: [1], l: a(a(x)), lp: a(x), sig: {x -> a(x')}, l': a(a(x')), r: a(b(a(x))), r': a(b(a(x'))))
(R2 unifies with R2 at p: [1,1], l: b(a(b(x))), lp: b(x), sig: {x -> a(b(x'))}, l': b(a(b(x'))), r: a(c(a(x))), r': a(c(a(x'))))

-> Critical pairs info:
<b(a(a(c(a(x'))))),a(c(a(a(b(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
<a(a(b(a(x')))),a(b(a(a(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N2

-> 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 CS-TRS, Left-homogeneous u-replacing variables



The problem is decomposed in 2 subproblems.

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(a 1)
(b 1)
(c)
(fSNonEmpty)
)
(RULES
a(a(x)) -> a(b(a(x)))
b(a(b(x))) -> a(c(a(x)))
)
Critical Pairs:
<b(a(a(c(a(x'))))),a(c(a(a(b(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N1
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: b(a(a(c(a(x')))))
Nodes: [0,1,2,3]
Edges: [(0,1),(1,2),(2,3)]
ID: 0 => ('b(a(a(c(a(x')))))', D0)
ID: 1 => ('b(a(b(a(c(a(x'))))))', D1, R1, P[1], S{x4 -> c(a(x'))}), NR: 'a(b(a(c(a(x')))))'
ID: 2 => ('a(c(a(a(c(a(x'))))))', D2, R2, P[], S{x5 -> a(c(a(x')))}), NR: 'a(c(a(a(c(a(x'))))))'
ID: 3 => ('a(c(a(b(a(c(a(x')))))))', D3, R1, P[1, 1], S{x4 -> c(a(x'))}), NR: 'a(b(a(c(a(x')))))'
t: a(c(a(a(b(x')))))
Nodes: [0,1,2,3]
Edges: [(0,1),(1,2),(2,3)]
ID: 0 => ('a(c(a(a(b(x')))))', D0)
ID: 1 => ('a(c(a(b(a(b(x'))))))', D1, R1, P[1, 1], S{x4 -> b(x')}), NR: 'a(b(a(b(x'))))'
ID: 2 => ('a(c(a(a(c(a(x'))))))', D2, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'a(c(a(x')))'
ID: 3 => ('a(c(a(b(a(c(a(x')))))))', D3, R1, P[1, 1], S{x4 -> c(a(x'))}), NR: 'a(b(a(c(a(x')))))'
SNodesPath: b(a(a(c(a(x'))))) -> b(a(b(a(c(a(x')))))) -> a(c(a(a(c(a(x'))))))
TNodesPath: a(c(a(a(b(x'))))) -> a(c(a(b(a(b(x')))))) -> a(c(a(a(c(a(x'))))))
b(a(a(c(a(x'))))) ->* a(c(a(a(c(a(x')))))) *<- a(c(a(a(b(x')))))
"Joinable"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(a 1)
(b 1)
(c)
(fSNonEmpty)
)
(RULES
a(a(x)) -> a(b(a(x)))
b(a(b(x))) -> a(c(a(x)))
)
Critical Pairs:
<a(a(b(a(x')))),a(b(a(a(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N2
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: a(a(b(a(x'))))
Nodes: [0,1,2,3,4,5]
Edges: [(0,1),(1,2),(2,3),(2,4),(3,5),(4,5)]
ID: 0 => ('a(a(b(a(x'))))', D0)
ID: 1 => ('a(b(a(b(a(x')))))', D1, R1, P[], S{x4 -> b(a(x'))}), NR: 'a(b(a(b(a(x')))))'
ID: 2 => ('a(a(c(a(a(x')))))', D2, R2, P[1], S{x5 -> a(x')}), NR: 'a(c(a(a(x'))))'
ID: 3 => ('a(b(a(c(a(a(x'))))))', D3, R1, P[], S{x4 -> c(a(a(x')))}), NR: 'a(b(a(c(a(a(x'))))))'
ID: 4 => ('a(a(c(a(b(a(x'))))))', D3, R1, P[1, 1, 1], S{x4 -> x'}), NR: 'a(b(a(x')))'
ID: 5 => ('a(b(a(c(a(b(a(x')))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> x'}), NR: 'a(b(a(x')))'
t: a(b(a(a(x'))))
Nodes: [0,1,2,3,4,5]
Edges: [(0,1),(1,2),(2,3),(2,4),(3,5),(4,5)]
ID: 0 => ('a(b(a(a(x'))))', D0)
ID: 1 => ('a(b(a(b(a(x')))))', D1, R1, P[1, 1], S{x4 -> x'}), NR: 'a(b(a(x')))'
ID: 2 => ('a(a(c(a(a(x')))))', D2, R2, P[1], S{x5 -> a(x')}), NR: 'a(c(a(a(x'))))'
ID: 3 => ('a(b(a(c(a(a(x'))))))', D3, R1, P[], S{x4 -> c(a(a(x')))}), NR: 'a(b(a(c(a(a(x'))))))'
ID: 4 => ('a(a(c(a(b(a(x'))))))', D3, R1, P[1, 1, 1], S{x4 -> x'}), NR: 'a(b(a(x')))'
ID: 5 => ('a(b(a(c(a(b(a(x')))))))', D4, R1, P[1, 1, 1, 1], S{x4 -> x'}), NR: 'a(b(a(x')))'
SNodesPath: a(a(b(a(x')))) -> a(b(a(b(a(x')))))
TNodesPath: a(b(a(a(x')))) -> a(b(a(b(a(x')))))
a(a(b(a(x')))) ->* a(b(a(b(a(x'))))) *<- a(b(a(a(x'))))
"Joinable"

The problem is confluent.