Certification Problem

Input (TPDB TRS_Relative/Relative_05/rt3-4)

The relative rewrite relation R/S is considered where R is the following TRS

f(a,g(y),z) → f(b,g(y),g(y)) (1)
f(b,g(y),z) → f(a,y,z) (2)
a → b (3)

and S is the following TRS.

f(x,y,z) → f(x,y,g(z)) (4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{f(☐,z1,z2), f(z0,☐,z2), f(z0,z1,☐), g(☐)}

We obtain the transformed TRS
f(a,g(y),z) → f(b,g(y),g(y)) (1)
f(b,g(y),z) → f(a,y,z) (2)
f(a,z1,z2) → f(b,z1,z2) (5)
f(z0,a,z2) → f(z0,b,z2) (6)
f(z0,z1,a) → f(z0,z1,b) (7)
g(a) → g(b) (8)
f(x,y,z) → f(x,y,g(z)) (4)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

There are 145 ruless (increase limit for explicit display).

1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[fagf(x1, x2, x3)] =
0
2
+
3 1
2 1
· x1 +
2 1
0 2
· x2 +
3 0
3 3
· x3
[a] =
0
0
[gf(x1)] =
0
0
+
1 0
1 0
· x1
[fbgg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 1
0 0
· x2 +
1 0
0 0
· x3
[b] =
0
0
[faga(x1, x2, x3)] =
0
2
+
2 0
0 0
· x1 +
3 1
0 0
· x2 +
2 0
0 0
· x3
[fagg(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 1
0 0
· x2 +
1 0
0 0
· x3
[fagb(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
3 1
0 0
· x2 +
2 0
0 0
· x3
[ga(x1)] =
0
0
+
1 0
1 0
· x1
[gg(x1)] =
0
3
+
1 0
1 1
· x1
[gb(x1)] =
0
0
+
1 0
0 2
· x1
[fbgf(x1, x2, x3)] =
0
2
+
1 2
2 2
· x1 +
2 1
0 2
· x2 +
3 0
3 3
· x3
[faff(x1, x2, x3)] =
0
2
+
3 2
2 2
· x1 +
3 0
2 0
· x2 +
3 0
3 3
· x3
[fbga(x1, x2, x3)] =
0
2
+
2 0
0 0
· x1 +
3 1
0 0
· x2 +
2 0
0 0
· x3
[fafa(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
3 0
0 0
· x2 +
2 0
0 0
· x3
[fafg(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
1 0
0 0
· x3
[fbgb(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 1
0 0
· x2 +
2 0
0 0
· x3
[fafb(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
3 0
0 0
· x2 +
2 0
0 0
· x3
[faaf(x1, x2, x3)] =
0
2
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
3 0
3 3
· x3
[faaa(x1, x2, x3)] =
0
2
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[faag(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
1 0
0 0
· x3
[faab(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fabf(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
3 0
3 3
· x3
[faba(x1, x2, x3)] =
0
2
+
1 0
0 0
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fabg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fabb(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fbff(x1, x2, x3)] =
0
0
+
2 2
2 2
· x1 +
3 0
1 0
· x2 +
3 0
3 3
· x3
[fbfa(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
3 0
0 0
· x2 +
2 0
0 0
· x3
[fbfg(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
1 0
0 0
· x3
[fbfb(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
3 0
0 0
· x2 +
2 0
0 0
· x3
[fbaf(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
1 0
0 0
· x2 +
3 0
3 3
· x3
[fbaa(x1, x2, x3)] =
0
2
+
2 0
0 0
· x1 +
1 0
0 0
· x2 +
2 0
0 0
· x3
[fbag(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbab(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
1 0
0 0
· x2 +
2 0
0 0
· x3
[fbbf(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
3 0
3 3
· x3
[fbba(x1, x2, x3)] =
0
1
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fbbg(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbbb(x1, x2, x3)] =
0
0
+
2 0
0 0
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[ffaf(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
3 1
2 2
· x2 +
3 3
3 3
· x3
[ffbf(x1, x2, x3)] =
0
0
+
3 1
3 3
· x1 +
2 1
2 2
· x2 +
3 3
3 3
· x3
[ffaa(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[ffba(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[ffag(x1, x2, x3)] =
0
0
+
3 2
2 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[ffbg(x1, x2, x3)] =
0
0
+
1 1
1 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[ffab(x1, x2, x3)] =
0
0
+
3 2
2 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[ffbb(x1, x2, x3)] =
0
0
+
1 2
2 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fgaf(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
2 1
2 2
· x2 +
3 3
3 3
· x3
[fgbf(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
3 1
2 2
· x2 +
3 0
3 3
· x3
[fgaa(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fgba(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fgag(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fgbg(x1, x2, x3)] =
0
0
+
3 2
1 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fgab(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fgbb(x1, x2, x3)] =
0
0
+
3 2
2 3
· x1 +
2 0
0 0
· x2 +
2 0
0 0
· x3
[fffa(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 2
1 0
· x3
[fffb(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 1
1 0
· x3
[ffga(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 2
1 0
· x3
[ffgb(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 0
1 2
· x3
[fgfa(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 0
2 2
· x3
[fgfb(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 1
1 2
· x3
[fgga(x1, x2, x3)] =
0
2
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 0
1 2
· x3
[fggb(x1, x2, x3)] =
0
0
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
2 0
1 0
· x3
[ffff(x1, x2, x3)] =
3
1
+
3 3
3 2
· x1 +
3 3
3 3
· x2 +
3 1
1 1
· x3
[fffg(x1, x2, x3)] =
0
0
+
3 3
3 2
· x1 +
3 3
3 2
· x2 +
2 0
0 0
· x3
[ffgf(x1, x2, x3)] =
1
1
+
3 3
3 2
· x1 +
3 2
3 3
· x2 +
1 1
1 3
· x3
[ffgg(x1, x2, x3)] =
0
0
+
3 3
3 2
· x1 +
3 2
3 2
· x2 +
1 0
0 0
· x3
[fgff(x1, x2, x3)] =
3
1
+
3 2
3 3
· x1 +
3 3
2 3
· x2 +
1 3
1 1
· x3
[fgfg(x1, x2, x3)] =
0
0
+
2 2
3 3
· x1 +
2 3
2 3
· x2 +
1 0
0 0
· x3
[fggf(x1, x2, x3)] =
3
1
+
3 3
3 3
· x1 +
3 3
3 3
· x2 +
1 1
1 1
· x3
[fggg(x1, x2, x3)] =
0
0
+
3 2
2 3
· x1 +
3 3
3 3
· x2 +
1 0
0 0
· x3
all of the following rules can be deleted.
fbgf(b,gg(y),z) → fagf(a,y,z) (33)
fbga(b,gg(y),z) → faga(a,y,z) (34)
fbgg(b,gg(y),z) → fagg(a,y,z) (35)
fbgb(b,gg(y),z) → fagb(a,y,z) (36)
ffff(x,y,z) → fffg(x,y,gf(z)) (90)
ffgf(x,y,z) → ffgg(x,y,gf(z)) (98)
fgff(x,y,z) → fgfg(x,y,gf(z)) (122)
fggf(x,y,z) → fggg(x,y,gf(z)) (130)

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[fagf(x1, x2, x3)] =
0
1
+
1 0
1 1
· x1 +
1 1
0 0
· x2 +
1 1
1 1
· x3
[a] =
0
1
[gf(x1)] =
0
1
+
1 0
1 1
· x1
[fbgg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[b] =
0
0
[faga(x1, x2, x3)] =
0
1
+
1 0
1 1
· x1 +
1 1
0 0
· x2 +
1 0
1 0
· x3
[fagg(x1, x2, x3)] =
0
1
+
1 0
1 1
· x1 +
1 1
0 0
· x2 +
1 0
1 0
· x3
[fagb(x1, x2, x3)] =
0
1
+
1 0
1 1
· x1 +
1 1
0 0
· x2 +
1 1
1 1
· x3
[ga(x1)] =
0
0
+
1 0
1 0
· x1
[gg(x1)] =
0
0
+
1 0
1 1
· x1
[gb(x1)] =
0
0
+
1 0
1 0
· x1
[fbgf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[faff(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbga(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fafa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fafg(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbgb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fafb(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[faaf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[faaa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[faag(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[faab(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fabf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[faba(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fabg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fabb(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbff(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbfa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbfg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbfb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbaf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbaa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbag(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbab(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbbf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbbg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbbb(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[ffaf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 1
· x2 +
1 1
1 1
· x3
[ffbf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ffaa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[ffba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[ffag(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[ffbg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[ffab(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[ffbb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgaf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 1
· x2 +
1 1
1 1
· x3
[fgbf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 0
· x3
[fgaa(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[fgba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fgag(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[fgbg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[fgab(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[fgbb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fffa(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fffb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ffga(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[ffgb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgfa(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fgfb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgga(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fggb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fffg(x1, x2, x3)] =
0
1
+
1 1
0 0
· x1 +
1 0
0 0
· x2 +
1 0
1 0
· x3
[ffgg(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 0
· x2 +
1 0
1 0
· x3
[fgfg(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[fggg(x1, x2, x3)] =
0
1
+
1 1
1 0
· x1 +
1 0
1 1
· x2 +
1 0
1 0
· x3
all of the following rules can be deleted.
fagf(a,gf(y),z) → fbgg(b,gf(y),gf(y)) (9)
faga(a,gf(y),z) → fbgg(b,gf(y),gf(y)) (10)
fagg(a,gf(y),z) → fbgg(b,gf(y),gf(y)) (11)
fagb(a,gf(y),z) → fbgg(b,gf(y),gf(y)) (12)

1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[fagf(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 1
0 0
· x2 +
1 1
1 1
· x3
[a] =
0
1
[ga(x1)] =
0
0
+
1 0
1 0
· x1
[fbgg(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[b] =
0
1
[faga(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 1
0 0
· x2 +
1 0
1 0
· x3
[fagg(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 1
0 0
· x2 +
1 0
1 0
· x3
[fagb(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 1
0 0
· x2 +
1 0
1 0
· x3
[gg(x1)] =
0
0
+
1 0
1 1
· x1
[gb(x1)] =
0
0
+
1 0
1 0
· x1
[fbgf(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[gf(x1)] =
0
0
+
1 1
1 1
· x1
[faff(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 1
1 1
· x3
[fbga(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fafa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 0
0 0
· x3
[fafg(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 0
0 0
· x3
[fbgb(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fafb(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 0
0 0
· x3
[faaf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[faaa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[faag(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[faab(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fabf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[faba(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fabg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fabb(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbff(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 1
1 1
· x3
[fbfa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 0
0 0
· x3
[fbfg(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 0
0 0
· x3
[fbfb(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 0
0 0
· x3
[fbaf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbaa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbag(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbab(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbbf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 1
0 1
· x3
[fbba(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbbg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[fbbb(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[ffaf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 1
· x2 +
1 1
1 1
· x3
[ffbf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[ffaa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[ffba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[ffag(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[ffbg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[ffab(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[ffbb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[fgaf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[fgbf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[fgaa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[fgba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[fgag(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[fgbg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[fgab(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[fgbb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[fffa(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fffb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[ffga(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[ffgb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fgfa(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fgfb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fgga(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fggb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fffg(x1, x2, x3)] =
0
1
+
1 1
1 0
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[ffgg(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
0 1
· x2 +
1 0
1 0
· x3
[fgfg(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[fggg(x1, x2, x3)] =
0
1
+
1 0
1 1
· x1 +
1 0
1 1
· x2 +
1 0
1 0
· x3
all of the following rules can be deleted.
fbgf(b,gf(y),z) → faff(a,y,z) (25)
fbga(b,gf(y),z) → fafa(a,y,z) (26)
fbgg(b,gf(y),z) → fafg(a,y,z) (27)
fbgb(b,gf(y),z) → fafb(a,y,z) (28)
fbgf(b,ga(y),z) → faaf(a,y,z) (29)
fbga(b,ga(y),z) → faaa(a,y,z) (30)
fbgg(b,ga(y),z) → faag(a,y,z) (31)
fbgb(b,ga(y),z) → faab(a,y,z) (32)
fbgf(b,gb(y),z) → fabf(a,y,z) (37)
fbga(b,gb(y),z) → faba(a,y,z) (38)
fbgg(b,gb(y),z) → fabg(a,y,z) (39)
fbgb(b,gb(y),z) → fabb(a,y,z) (40)

1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[fagf(x1, x2, x3)] =
0
1
+
1 0
1 1
· x1 +
1 1
0 0
· x2 +
1 1
1 1
· x3
[a] =
0
1
[ga(x1)] =
0
1
+
1 0
1 0
· x1
[fbgg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
0 0
· x2 +
1 0
0 0
· x3
[b] =
0
0
[faga(x1, x2, x3)] =
0
1
+
1 0
1 0
· x1 +
1 1
0 1
· x2 +
1 0
1 0
· x3
[fagg(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
0 0
· x2 +
1 0
1 0
· x3
[fagb(x1, x2, x3)] =
0
1
+
1 0
1 0
· x1 +
1 1
0 1
· x2 +
1 1
1 1
· x3
[gg(x1)] =
0
1
+
1 0
1 1
· x1
[gb(x1)] =
0
1
+
1 0
1 0
· x1
[faff(x1, x2, x3)] =
0
1
+
1 0
1 0
· x1 +
1 0
1 1
· x2 +
1 1
1 1
· x3
[fbff(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 1
· x2 +
1 1
1 1
· x3
[fafa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fbfa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fafg(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
1 1
· x2 +
1 0
1 0
· x3
[fbfg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 1
· x2 +
1 0
1 0
· x3
[fafb(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fbfb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[faaf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[fbaf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[faaa(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[fbaa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[faag(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
1 0
· x3
[fbag(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
1 0
· x3
[faab(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[fbab(x1, x2, x3)] =
0
0
+
1 0
0 1
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbgf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
0 0
· x2 +
1 1
1 1
· x3
[fbga(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
0 1
· x2 +
1 0
1 0
· x3
[fbgb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
0 1
· x2 +
1 1
1 1
· x3
[fabf(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fbbf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[faba(x1, x2, x3)] =
0
0
+
1 0
1 0
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[fbba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[fabg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
1 0
· x3
[fbbg(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
1 0
· x3
[fabb(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 1
· x2 +
1 1
1 1
· x3
[fbbb(x1, x2, x3)] =
0
0
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 0
1 1
· x3
[ffaf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[ffbf(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ffaa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[ffba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[ffag(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[ffbg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[ffab(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[ffbb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgaf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 1
· x2 +
1 1
1 1
· x3
[fgbf(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgaa(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 1
· x3
[fgba(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fgag(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[fgbg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[fgab(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 0
1 0
· x2 +
1 1
1 1
· x3
[fgbb(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fffa(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fffb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ffga(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[ffgb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgfa(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fgfb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgga(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[fggb(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fffg(x1, x2, x3)] =
0
1
+
1 1
1 0
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[gf(x1)] =
0
1
+
1 1
1 1
· x1
[ffgg(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 0
1 0
· x3
[fgfg(x1, x2, x3)] =
0
1
+
1 1
0 1
· x1 +
1 0
1 0
· x2 +
1 0
1 0
· x3
[fggg(x1, x2, x3)] =
0
1
+
1 1
1 1
· x1 +
1 0
1 1
· x2 +
1 0
1 0
· x3
all of the following rules can be deleted.
fagf(a,ga(y),z) → fbgg(b,ga(y),ga(y)) (13)
faga(a,ga(y),z) → fbgg(b,ga(y),ga(y)) (14)
fagg(a,ga(y),z) → fbgg(b,ga(y),ga(y)) (15)
fagb(a,ga(y),z) → fbgg(b,ga(y),ga(y)) (16)
fagf(a,gg(y),z) → fbgg(b,gg(y),gg(y)) (17)
faga(a,gg(y),z) → fbgg(b,gg(y),gg(y)) (18)
fagg(a,gg(y),z) → fbgg(b,gg(y),gg(y)) (19)
fagb(a,gg(y),z) → fbgg(b,gg(y),gg(y)) (20)
fagf(a,gb(y),z) → fbgg(b,gb(y),gb(y)) (21)
faga(a,gb(y),z) → fbgg(b,gb(y),gb(y)) (22)
fagg(a,gb(y),z) → fbgg(b,gb(y),gb(y)) (23)
fagb(a,gb(y),z) → fbgg(b,gb(y),gb(y)) (24)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 0
[fafa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbfa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbfb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[faaf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbaf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[faaa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbaa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faab(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbab(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fagf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbgf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[faga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbgb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fabf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbbf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[faba(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbba(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fbbb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffaf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffbf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffaa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffba(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffab(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffbb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgaf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgbf(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgaa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgba(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgab(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgbb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffa(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fffb(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgfa(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfb(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgga(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggb(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 · x1
[gb(x1)] = 1 · x1
[fffg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[gg(x1)] = 1 · x1
[gf(x1)] = 1 · x1
[ffgg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
fafa(a,z1,z2) → fbfa(b,z1,z2) (42)
fafg(a,z1,z2) → fbfg(b,z1,z2) (43)
fafb(a,z1,z2) → fbfb(b,z1,z2) (44)
faaf(a,z1,z2) → fbaf(b,z1,z2) (45)
faaa(a,z1,z2) → fbaa(b,z1,z2) (46)
faag(a,z1,z2) → fbag(b,z1,z2) (47)
faab(a,z1,z2) → fbab(b,z1,z2) (48)
fagf(a,z1,z2) → fbgf(b,z1,z2) (49)
faga(a,z1,z2) → fbga(b,z1,z2) (50)
fagg(a,z1,z2) → fbgg(b,z1,z2) (51)
fagb(a,z1,z2) → fbgb(b,z1,z2) (52)
fabf(a,z1,z2) → fbbf(b,z1,z2) (53)
faba(a,z1,z2) → fbba(b,z1,z2) (54)
fabg(a,z1,z2) → fbbg(b,z1,z2) (55)
fabb(a,z1,z2) → fbbb(b,z1,z2) (56)
ffaf(z0,a,z2) → ffbf(z0,b,z2) (57)
ffaa(z0,a,z2) → ffba(z0,b,z2) (58)
ffag(z0,a,z2) → ffbg(z0,b,z2) (59)
ffab(z0,a,z2) → ffbb(z0,b,z2) (60)
faaf(z0,a,z2) → fabf(z0,b,z2) (61)
faaa(z0,a,z2) → faba(z0,b,z2) (62)
faag(z0,a,z2) → fabg(z0,b,z2) (63)
faab(z0,a,z2) → fabb(z0,b,z2) (64)
fgaf(z0,a,z2) → fgbf(z0,b,z2) (65)
fgaa(z0,a,z2) → fgba(z0,b,z2) (66)
fgag(z0,a,z2) → fgbg(z0,b,z2) (67)
fgab(z0,a,z2) → fgbb(z0,b,z2) (68)
fbaf(z0,a,z2) → fbbf(z0,b,z2) (69)
fbaa(z0,a,z2) → fbba(z0,b,z2) (70)
fbag(z0,a,z2) → fbbg(z0,b,z2) (71)
fbab(z0,a,z2) → fbbb(z0,b,z2) (72)
fffa(z0,z1,a) → fffb(z0,z1,b) (73)
ffaa(z0,z1,a) → ffab(z0,z1,b) (74)
ffga(z0,z1,a) → ffgb(z0,z1,b) (75)
ffba(z0,z1,a) → ffbb(z0,z1,b) (76)
fafa(z0,z1,a) → fafb(z0,z1,b) (77)
faaa(z0,z1,a) → faab(z0,z1,b) (78)
faga(z0,z1,a) → fagb(z0,z1,b) (79)
faba(z0,z1,a) → fabb(z0,z1,b) (80)
fgfa(z0,z1,a) → fgfb(z0,z1,b) (81)
fgaa(z0,z1,a) → fgab(z0,z1,b) (82)
fgga(z0,z1,a) → fggb(z0,z1,b) (83)
fgba(z0,z1,a) → fgbb(z0,z1,b) (84)
fbfa(z0,z1,a) → fbfb(z0,z1,b) (85)
fbaa(z0,z1,a) → fbab(z0,z1,b) (86)
fbga(z0,z1,a) → fbgb(z0,z1,b) (87)
fbba(z0,z1,a) → fbbb(z0,z1,b) (88)
ga(a) → gb(b) (89)
ffaf(x,y,z) → ffag(x,y,gf(z)) (94)
ffaa(x,y,z) → ffag(x,y,ga(z)) (95)
ffab(x,y,z) → ffag(x,y,gb(z)) (97)
ffbf(x,y,z) → ffbg(x,y,gf(z)) (102)
ffba(x,y,z) → ffbg(x,y,ga(z)) (103)
ffbb(x,y,z) → ffbg(x,y,gb(z)) (105)
fafa(x,y,z) → fafg(x,y,ga(z)) (107)
fafb(x,y,z) → fafg(x,y,gb(z)) (109)
faaf(x,y,z) → faag(x,y,gf(z)) (110)
faaa(x,y,z) → faag(x,y,ga(z)) (111)
faab(x,y,z) → faag(x,y,gb(z)) (113)
fagf(x,y,z) → fagg(x,y,gf(z)) (114)
faga(x,y,z) → fagg(x,y,ga(z)) (115)
fagb(x,y,z) → fagg(x,y,gb(z)) (117)
fabf(x,y,z) → fabg(x,y,gf(z)) (118)
faba(x,y,z) → fabg(x,y,ga(z)) (119)
fabb(x,y,z) → fabg(x,y,gb(z)) (121)
fgaf(x,y,z) → fgag(x,y,gf(z)) (126)
fgaa(x,y,z) → fgag(x,y,ga(z)) (127)
fgab(x,y,z) → fgag(x,y,gb(z)) (129)
fgbf(x,y,z) → fgbg(x,y,gf(z)) (134)
fgba(x,y,z) → fgbg(x,y,ga(z)) (135)
fgbb(x,y,z) → fgbg(x,y,gb(z)) (137)
fbff(x,y,z) → fbfg(x,y,gf(z)) (138)
fbfa(x,y,z) → fbfg(x,y,ga(z)) (139)
fbfb(x,y,z) → fbfg(x,y,gb(z)) (141)
fbaf(x,y,z) → fbag(x,y,gf(z)) (142)
fbaa(x,y,z) → fbag(x,y,ga(z)) (143)
fbab(x,y,z) → fbag(x,y,gb(z)) (145)
fbgf(x,y,z) → fbgg(x,y,gf(z)) (146)
fbga(x,y,z) → fbgg(x,y,ga(z)) (147)
fbgb(x,y,z) → fbgg(x,y,gb(z)) (149)
fbbf(x,y,z) → fbbg(x,y,gf(z)) (150)
fbba(x,y,z) → fbbg(x,y,ga(z)) (151)
fbbb(x,y,z) → fbbg(x,y,gb(z)) (153)

1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[faff(x1, x2, x3)] =
1
1
+
1 1
1 0
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[a] =
1
1
[fbff(x1, x2, x3)] =
1
1
+
1 1
1 0
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[b] =
1
1
[fffa(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fffg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ga(x1)] =
1
0
+
1 0
0 1
· x1
[gg(x1)] =
0
0
+
1 0
0 1
· x1
[fffb(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[gb(x1)] =
0
1
+
1 0
0 1
· x1
[ffag(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[ffga(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ffgg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ffgb(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[ffbg(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fafg(x1, x2, x3)] =
0
0
+
1 1
1 0
· x1 +
1 1
1 1
· x2 +
1 0
1 1
· x3
[gf(x1)] =
0
1
+
1 1
0 0
· x1
[faag(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fagg(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fabg(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fgfa(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgfg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgfb(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgag(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fgga(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fggg(x1, x2, x3)] =
0
0
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fggb(x1, x2, x3)] =
1
1
+
1 1
1 1
· x1 +
1 1
1 1
· x2 +
1 1
1 1
· x3
[fgbg(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbfg(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbag(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbgg(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
[fbbg(x1, x2, x3)] =
1
1
+
1 0
0 0
· x1 +
1 0
0 0
· x2 +
1 1
1 1
· x3
all of the following rules can be deleted.
faff(x,y,z) → fafg(x,y,gf(z)) (106)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 · x1
[gg(x1)] = 1 · x1
[fffb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[gb(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfb(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fggb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
fgfa(x,y,z) → fgfg(x,y,ga(z)) (123)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 · x1
[gg(x1)] = 1 · x1
[fffb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[gb(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgfb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fggb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
fffb(x,y,z) → fffg(x,y,gb(z)) (93)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 + 1 · x1
[gg(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffgb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[gb(x1)] = 1 · x1
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgfb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggb(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
ffgb(x,y,z) → ffgg(x,y,gb(z)) (101)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 + 1 · x1
[gg(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgfb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[gb(x1)] = 1 · x1
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
fggb(x,y,z) → fggg(x,y,gb(z)) (133)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 · x1
[gg(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[gb(x1)] = 1 + 1 · x1
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
fgga(x,y,z) → fggg(x,y,ga(z)) (131)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 + 1 · x1
[gg(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfb(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[gb(x1)] = 1 · x1
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
fgfb(x,y,z) → fgfg(x,y,gb(z)) (125)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 · x1
[gg(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffga(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
ffga(x,y,z) → ffgg(x,y,ga(z)) (99)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffa(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[fffg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ga(x1)] = 1 · x1
[gg(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
fffa(x,y,z) → fffg(x,y,ga(z)) (91)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[faff(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[a] = 1
[fbff(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[b] = 1
[fffg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[gg(x1)] = 1 · x1
[ffag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ffbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fafg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[faag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fagg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fabg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fggg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fgbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbfg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbag(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbgg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[fbbg(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
all of the following rules can be deleted.
faff(a,z1,z2) → fbff(b,z1,z2) (41)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.