YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(f_1)
(i_1)
(a_0)
(h_0 1)
)
(RULES
f_1(i_1(x)) -> a_0
f_1(h_0(x)) -> f_1(i_1(x))
i_1(x) -> h_0(x)
)

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 

Problem 1: 
Left-Homogeneous u-Replacing Variables Procedure:
R satisfies LHRV condition

Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x)
(REPLACEMENT-MAP
(f_1)
(i_1)
(a_0)
(h_0 1)
)
(RULES
f_1(i_1(x)) -> a_0
f_1(h_0(x)) -> f_1(i_1(x))
i_1(x) -> h_0(x)
)

:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy Procedure:
-> Rules:
 f_1(i_1(x)) -> a_0
 f_1(h_0(x)) -> f_1(i_1(x))
 i_1(x) -> h_0(x)
-> Vars:
 x, x, x
-> UVars:
 (UV-RuleId: 1, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: [])
 (UV-RuleId: 2, UV-LActive: [], UV-RActive: [], UV-LFrozen: [x], UV-RFrozen: [x])
 (UV-RuleId: 3, UV-LActive: [], UV-RActive: [x], UV-LFrozen: [x], UV-RFrozen: [])

-> Rlps:
 (rule: f_1(i_1(x)) -> a_0, id: 1, possubterms: f_1(i_1(x))->[])
 (rule: f_1(h_0(x)) -> f_1(i_1(x)), id: 2, possubterms: f_1(h_0(x))->[])
 (rule: i_1(x) -> h_0(x), id: 3, possubterms: i_1(x)->[])

-> Unifications:


-> Critical pairs info:


-> Problem conclusions:
 Left linear, Right linear, Linear
 Weakly orthogonal, Almost orthogonal, Orthogonal, Not strongly orthogonal
 Huet-Levy confluent, Not Newman confluent
 R is a CS-TRS, Left-homogeneous u-replacing variables
 Confluent


The problem is confluent.