YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(b)
(f 1, 2)
(i 1)
(a)
(fSNonEmpty)
(g 1)
(j 1, 2)
)
(RULES
b -> a
f(i(x),g(a)) -> f(j(x,x),g(b))
i(x) -> j(x,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:
(b)
(f 1 2)
(i 1)
(a)
(fSNonEmpty)
(g 1)
(j 1 2)

New Replacement Map:
(b)
(f 1 2)
(i)
(a)
(fSNonEmpty)
(g 1)
(j)

New problem:

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(b)
(f 1, 2)
(i)
(a)
(fSNonEmpty)
(g 1)
(j)
)
(RULES
b -> a
f(i(x),g(a)) -> f(j(x,x),g(b))
i(x) -> j(x,x)
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 
Termination Procedure:
Terminating?
YES

Problem 1: 

(VAR vu95NonEmpty vNonEmpty x)
(STRATEGY CONTEXTSENSITIVE
(b)
(f 1 2)
(i)
(a)
(fSNonEmpty)
(g 1)
(j)
)
(RULES
b -> a
f(i(x),g(a)) -> f(j(x,x),g(b))
i(x) -> j(x,x)
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 F(i(x),g(a)) -> B
 F(i(x),g(a)) -> F(j(x,x),g(b))
-> Rules:
 b -> a
 f(i(x),g(a)) -> f(j(x,x),g(b))
 i(x) -> j(x,x)
-> Unhiding Rules:
 Empty

Problem 1: 

SCC Processor:
-> Pairs:
 F(i(x),g(a)) -> B
 F(i(x),g(a)) -> F(j(x,x),g(b))
-> Rules:
 b -> a
 f(i(x),g(a)) -> f(j(x,x),g(b))
 i(x) -> j(x,x)
-> Unhiding rules:
 Empty
->Strongly Connected Components:
 There is no strongly connected component

The problem is finite.


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(b)
(f 1, 2)
(i)
(a)
(fSNonEmpty)
(g 1)
(j)
)
(RULES
b -> a
f(i(x),g(a)) -> f(j(x,x),g(b))
i(x) -> j(x,x)
)
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

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

-> Rlps:
 (rule: b -> a, id: 1, possubterms: b->[])
 (rule: f(i(x),g(a)) -> f(j(x,x),g(b)), id: 2, possubterms: f(i(x),g(a))->[], i(x)->[1], g(a)->[2], a->[2, 1])
 (rule: i(x) -> j(x,x), id: 3, possubterms: i(x)->[])

-> Unifications:
(R2 unifies with R3 at p: [1], l: f(i(x),g(a)), lp: i(x), sig: {x -> x'}, l': i(x'), r: f(j(x,x),g(b)), r': j(x',x'))

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

-> Problem conclusions:
 Left linear, Not right linear, Not 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

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

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

The problem is confluent.