YES
Problem:
f(j(x,y),y) -> g(f(x,k(y)))
f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) -> y
i(h2(s(x),y,h1(x,z))) -> z
k(h(x)) -> h1(0(),x)
k(h1(x,y)) -> h1(s(x),y)
Proof:
Bounds Processor:
bound: 2
enrichment: match
automaton:
final states: {12,11,3,1,2}
transitions:
f0(2,12) -> 1*
f0(3,1) -> 1*
f0(3,3) -> 1*
f0(3,11) -> 1*
f0(11,2) -> 1*
f0(1,2) -> 1*
f0(11,12) -> 1*
f0(1,12) -> 1*
f0(12,1) -> 1*
f0(2,1) -> 1*
f0(12,3) -> 1*
f0(2,3) -> 1*
f0(12,11) -> 1*
f0(2,11) -> 1*
f0(3,2) -> 1*
f0(3,12) -> 1*
f0(11,1) -> 1*
f0(1,1) -> 1*
f0(11,3) -> 1*
f0(1,3) -> 1*
f0(11,11) -> 1*
f0(1,11) -> 1*
f0(12,2) -> 1*
f0(2,2) -> 1*
f0(12,12) -> 1*
j0(2,12) -> 1,11*
j0(3,1) -> 11*,1,2
j0(3,3) -> 11*,1,2
j0(3,11) -> 1,11*
j0(11,2) -> 1,11*
j0(1,2) -> 11*,1,2
j0(11,12) -> 1,11*
j0(1,12) -> 1,11*
j0(12,1) -> 1,11*
j0(2,1) -> 11*,1,2
j0(12,3) -> 1,11*
j0(2,3) -> 11*,1,2
j0(12,11) -> 1,11*
j0(2,11) -> 1,11*
j0(3,2) -> 11*,1,2
j0(3,12) -> 1,11*
j0(11,1) -> 1,11*
j0(1,1) -> 11*,1,2
j0(11,3) -> 1,11*
j0(1,3) -> 11*,1,2
j0(11,11) -> 1,11*
j0(1,11) -> 1,11*
j0(12,2) -> 1,11*
j0(2,2) -> 11*,1,2
j0(12,12) -> 1,11*
g0(12) -> 1*
g0(2) -> 1*
g0(11) -> 1*
g0(1) -> 1*
g0(3) -> 1*
k0(12) -> 1*
k0(2) -> 1*
k0(11) -> 1*
k0(1) -> 1*
k0(3) -> 1*
h10(2,12) -> 1*
h10(3,1) -> 1*
h10(3,3) -> 1*
h10(3,11) -> 1*
h10(11,2) -> 1*
h10(1,2) -> 1*
h10(11,12) -> 1*
h10(1,12) -> 1*
h10(12,1) -> 1*
h10(2,1) -> 1*
h10(12,3) -> 1*
h10(2,3) -> 1*
h10(12,11) -> 1*
h10(2,11) -> 1*
h10(3,2) -> 1*
h10(3,12) -> 1*
h10(11,1) -> 1*
h10(1,1) -> 1*
h10(11,3) -> 1*
h10(1,3) -> 1*
h10(11,11) -> 1*
h10(1,11) -> 1*
h10(12,2) -> 1*
h10(2,2) -> 1*
h10(12,12) -> 1*
h20(3,2,2) -> 1*
h20(3,2,11) -> 1*
h20(3,12,2) -> 1*
h20(3,12,11) -> 1*
h20(11,1,1) -> 1*
h20(1,1,1) -> 1*
h20(11,3,1) -> 1*
h20(1,3,1) -> 1*
h20(11,11,1) -> 1*
h20(1,11,1) -> 1*
h20(11,2,3) -> 1*
h20(1,2,3) -> 1*
h20(11,2,12) -> 1*
h20(12,2,1) -> 1*
h20(1,2,12) -> 1*
h20(2,2,1) -> 1*
h20(11,12,3) -> 1*
h20(1,12,3) -> 1*
h20(11,12,12) -> 1*
h20(12,12,1) -> 1*
h20(1,12,12) -> 1*
h20(2,12,1) -> 1*
h20(12,1,3) -> 1*
h20(2,1,3) -> 1*
h20(12,3,3) -> 1*
h20(2,3,3) -> 1*
h20(12,1,12) -> 1*
h20(11,1,2) -> 1*
h20(12,3,12) -> 1*
h20(2,1,12) -> 1*
h20(3,1,1) -> 1*
h20(1,1,2) -> 1*
h20(11,3,2) -> 1*
h20(2,3,12) -> 1*
h20(3,3,1) -> 1*
h20(1,3,2) -> 1*
h20(11,1,11) -> 1*
h20(12,11,3) -> 1*
h20(11,3,11) -> 1*
h20(1,1,11) -> 1*
h20(2,11,3) -> 1*
h20(1,3,11) -> 1*
h20(12,11,12) -> 1*
h20(11,11,2) -> 1*
h20(2,11,12) -> 1*
h20(3,11,1) -> 1*
h20(1,11,2) -> 1*
h20(11,11,11) -> 1*
h20(1,11,11) -> 1*
h20(3,2,3) -> 1*
h20(12,2,2) -> 1*
h20(3,2,12) -> 1*
h20(2,2,2) -> 1*
h20(12,2,11) -> 1*
h20(2,2,11) -> 1*
h20(3,12,3) -> 1*
h20(12,12,2) -> 1*
h20(3,12,12) -> 1*
h20(2,12,2) -> 1*
h20(12,12,11) -> 1*
h20(2,12,11) -> 1*
h20(3,1,2) -> 1*
h20(3,3,2) -> 1*
h20(3,1,11) -> 1*
h20(3,3,11) -> 1*
h20(3,11,2) -> 1*
h20(3,11,11) -> 1*
h20(11,2,1) -> 1*
h20(1,2,1) -> 1*
h20(11,12,1) -> 1*
h20(1,12,1) -> 1*
h20(11,1,3) -> 1*
h20(1,1,3) -> 1*
h20(11,3,3) -> 1*
h20(1,3,3) -> 1*
h20(11,1,12) -> 1*
h20(12,1,1) -> 1*
h20(11,3,12) -> 1*
h20(1,1,12) -> 1*
h20(2,1,1) -> 1*
h20(12,3,1) -> 1*
h20(1,3,12) -> 1*
h20(2,3,1) -> 1*
h20(11,11,3) -> 1*
h20(1,11,3) -> 1*
h20(11,11,12) -> 1*
h20(12,11,1) -> 1*
h20(1,11,12) -> 1*
h20(2,11,1) -> 1*
h20(12,2,3) -> 1*
h20(2,2,3) -> 1*
h20(12,2,12) -> 1*
h20(11,2,2) -> 1*
h20(2,2,12) -> 1*
h20(3,2,1) -> 1*
h20(1,2,2) -> 1*
h20(11,2,11) -> 1*
h20(12,12,3) -> 1*
h20(1,2,11) -> 1*
h20(2,12,3) -> 1*
h20(12,12,12) -> 1*
h20(11,12,2) -> 1*
h20(2,12,12) -> 1*
h20(3,12,1) -> 1*
h20(1,12,2) -> 1*
h20(11,12,11) -> 1*
h20(3,1,3) -> 1*
h20(1,12,11) -> 1*
h20(3,3,3) -> 1*
h20(12,1,2) -> 1*
h20(3,1,12) -> 1*
h20(2,1,2) -> 1*
h20(12,3,2) -> 1*
h20(3,3,12) -> 1*
h20(2,3,2) -> 1*
h20(12,1,11) -> 1*
h20(2,1,11) -> 1*
h20(12,3,11) -> 1*
h20(3,11,3) -> 1*
h20(2,3,11) -> 1*
h20(12,11,2) -> 1*
h20(3,11,12) -> 1*
h20(2,11,2) -> 1*
h20(12,11,11) -> 1*
h20(2,11,11) -> 1*
00() -> 1*
s0(12) -> 1*
s0(2) -> 1*
s0(11) -> 1*
s0(1) -> 1*
s0(3) -> 1*
i0(12) -> 1*
i0(2) -> 1*
i0(11) -> 1*
i0(1) -> 1*
i0(3) -> 1*
h0(12) -> 1,12*
h0(2) -> 12*,1,3
h0(11) -> 1,12*
h0(1) -> 12*,1,3
h0(3) -> 12*,1,3
h11(12,12) -> 1*
h11(2,12) -> 1*
h11(3,1) -> 1*
h11(3,3) -> 1*
h11(3,11) -> 1*
h11(11,2) -> 1*
h11(1,2) -> 1*
h11(11,12) -> 1*
h11(1,12) -> 1*
h11(12,1) -> 1*
h11(2,1) -> 1*
h11(12,3) -> 1*
h11(2,3) -> 1*
h11(12,11) -> 1*
h11(2,11) -> 1*
h11(3,2) -> 1*
h11(3,12) -> 1*
h11(11,1) -> 1*
h11(1,1) -> 1*
h11(11,3) -> 1*
h11(1,3) -> 1*
h11(11,11) -> 1*
h11(1,11) -> 1*
h11(12,2) -> 1*
h11(2,2) -> 1*
s1(12) -> 1*
s1(2) -> 1*
s1(11) -> 1*
s1(1) -> 1*
s1(3) -> 1*
01() -> 1*
h21(11,1,1) -> 1*
h21(1,1,1) -> 1*
h21(11,3,1) -> 1*
h21(1,3,1) -> 1*
h21(11,11,1) -> 1*
h21(1,11,1) -> 1*
h21(11,2,12) -> 1*
h21(12,2,1) -> 1*
h21(1,2,12) -> 1*
h21(11,12,12) -> 1*
h21(12,12,1) -> 1*
h21(1,12,12) -> 1*
h21(12,1,12) -> 1*
h21(12,3,12) -> 1*
h21(11,1,11) -> 1*
h21(11,3,11) -> 1*
h21(1,1,11) -> 1*
h21(1,3,11) -> 1*
h21(12,11,12) -> 1*
h21(11,11,11) -> 1*
h21(1,11,11) -> 1*
h21(12,2,11) -> 1*
h21(12,12,11) -> 1*
h21(11,2,1) -> 1*
h21(1,2,1) -> 1*
h21(11,12,1) -> 1*
h21(1,12,1) -> 1*
h21(11,1,12) -> 1*
h21(12,1,1) -> 1*
h21(11,3,12) -> 1*
h21(1,1,12) -> 1*
h21(12,3,1) -> 1*
h21(1,3,12) -> 1*
h21(11,11,12) -> 1*
h21(12,11,1) -> 1*
h21(1,11,12) -> 1*
h21(12,2,12) -> 1*
h21(11,2,11) -> 1*
h21(1,2,11) -> 1*
h21(12,12,12) -> 1*
h21(11,12,11) -> 1*
h21(1,12,11) -> 1*
h21(12,1,11) -> 1*
h21(12,3,11) -> 1*
h21(12,11,11) -> 1*
g1(12) -> 1*
g1(11) -> 1*
g1(1) -> 1*
f1(12,12) -> 1*
f1(2,12) -> 1*
f1(3,1) -> 1*
f1(3,11) -> 1*
f1(11,12) -> 1*
f1(1,12) -> 1*
f1(12,1) -> 1*
f1(2,1) -> 1*
f1(12,11) -> 1*
f1(2,11) -> 1*
f1(3,12) -> 1*
f1(11,1) -> 1*
f1(1,1) -> 1*
f1(11,11) -> 1*
f1(1,11) -> 1*
k1(12) -> 1*
k1(2) -> 1*
k1(11) -> 1*
k1(1) -> 1*
k1(3) -> 1*
h12(12,12) -> 1*
h12(11,2) -> 1*
h12(11,12) -> 1*
h12(1,12) -> 1*
h12(12,1) -> 1*
h12(12,3) -> 1*
h12(12,11) -> 1*
h12(2,11) -> 1*
h12(3,12) -> 1*
h12(11,1) -> 1*
h12(1,1) -> 1*
h12(11,3) -> 1*
h12(1,3) -> 1*
h12(11,11) -> 1*
h12(1,11) -> 1*
h12(12,2) -> 1*
h12(2,2) -> 1*
s2(12) -> 1*
s2(11) -> 1*
s2(1) -> 1*
h22(11,1,1) -> 1*
h22(1,1,1) -> 1*
h22(11,11,1) -> 1*
h22(1,11,1) -> 1*
h22(11,12,12) -> 1*
h22(12,12,1) -> 1*
h22(1,12,12) -> 1*
h22(12,1,12) -> 1*
h22(11,1,11) -> 1*
h22(1,1,11) -> 1*
h22(12,11,12) -> 1*
h22(11,11,11) -> 1*
h22(1,11,11) -> 1*
h22(12,12,11) -> 1*
h22(11,12,1) -> 1*
h22(1,12,1) -> 1*
h22(11,1,12) -> 1*
h22(12,1,1) -> 1*
h22(1,1,12) -> 1*
h22(11,11,12) -> 1*
h22(12,11,1) -> 1*
h22(1,11,12) -> 1*
h22(12,12,12) -> 1*
h22(11,12,11) -> 1*
h22(1,12,11) -> 1*
h22(12,1,11) -> 1*
h22(12,11,11) -> 1*
02() -> 1*
2 -> 1*
3 -> 1*
11 -> 1*
12 -> 1*
problem:
Qed