YES Termination proof of rt3-4.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 FlatCCProof (⇔, 0 ms)
↳2 RelTRS
↳3 RootLabelingProof (⇔, 0 ms)
↳4 RelTRS
↳5 RelTRSRRRProof (⇔, 528 ms)
↳6 RelTRS
↳7 RelTRSRRRProof (⇔, 0 ms)
↳8 RelTRS
↳9 RelTRSRRRProof (⇔, 1 ms)
↳10 RelTRS
↳11 RelTRSRRRProof (⇔, 0 ms)
↳12 RelTRS
↳13 RelTRSRRRProof (⇔, 8 ms)
↳14 RelTRS
↳15 RelTRSRRRProof (⇔, 0 ms)
↳16 RelTRS
↳17 RIsEmptyProof (⇔, 0 ms)
↳18 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f(a, g(y), z) → f(b, g(y), g(y))
f(b, g(y), z) → f(a, y, z)
a → b

The relative TRS consists of the following S rules:

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

(1) FlatCCProof (EQUIVALENT transformation)

We used flat context closure [ROOTLAB]

(2) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f(a, g(y), z) → f(b, g(y), g(y))
f(b, g(y), z) → f(a, y, z)
f(a, z1, z2) → f(b, z1, z2)
f(z0, a, z2) → f(z0, b, z2)
f(z0, z1, a) → f(z0, z1, b)
g(a) → g(b)

The relative TRS consists of the following S rules:

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

(3) RootLabelingProof (EQUIVALENT transformation)

We used plain root labeling [ROOTLAB] with the following heuristic: LabelAll: All function symbols get labeled

(4) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f_{a,g_1,f_3}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,a}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,g_1}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,b}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,f_3}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,a}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,g_1}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,b}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,f_3}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,a}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,g_1}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,b}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,f_3}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{a,g_1,a}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{a,g_1,g_1}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{a,g_1,b}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{b,g_1,f_3}(b, g_{f_3}(y), z) → f_{a,f_3,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{f_3}(y), z) → f_{a,f_3,a}(a, y, z)
f_{b,g_1,g_1}(b, g_{f_3}(y), z) → f_{a,f_3,g_1}(a, y, z)
f_{b,g_1,b}(b, g_{f_3}(y), z) → f_{a,f_3,b}(a, y, z)
f_{b,g_1,f_3}(b, g_{a}(y), z) → f_{a,a,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{a}(y), z) → f_{a,a,a}(a, y, z)
f_{b,g_1,g_1}(b, g_{a}(y), z) → f_{a,a,g_1}(a, y, z)
f_{b,g_1,b}(b, g_{a}(y), z) → f_{a,a,b}(a, y, z)
f_{b,g_1,f_3}(b, g_{g_1}(y), z) → f_{a,g_1,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{g_1}(y), z) → f_{a,g_1,a}(a, y, z)
f_{b,g_1,g_1}(b, g_{g_1}(y), z) → f_{a,g_1,g_1}(a, y, z)
f_{b,g_1,b}(b, g_{g_1}(y), z) → f_{a,g_1,b}(a, y, z)
f_{b,g_1,f_3}(b, g_{b}(y), z) → f_{a,b,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{b}(y), z) → f_{a,b,a}(a, y, z)
f_{b,g_1,g_1}(b, g_{b}(y), z) → f_{a,b,g_1}(a, y, z)
f_{b,g_1,b}(b, g_{b}(y), z) → f_{a,b,b}(a, y, z)
f_{a,f_3,f_3}(a, z1, z2) → f_{b,f_3,f_3}(b, z1, z2)
f_{a,f_3,a}(a, z1, z2) → f_{b,f_3,a}(b, z1, z2)
f_{a,f_3,g_1}(a, z1, z2) → f_{b,f_3,g_1}(b, z1, z2)
f_{a,f_3,b}(a, z1, z2) → f_{b,f_3,b}(b, z1, z2)
f_{a,a,f_3}(a, z1, z2) → f_{b,a,f_3}(b, z1, z2)
f_{a,a,a}(a, z1, z2) → f_{b,a,a}(b, z1, z2)
f_{a,a,g_1}(a, z1, z2) → f_{b,a,g_1}(b, z1, z2)
f_{a,a,b}(a, z1, z2) → f_{b,a,b}(b, z1, z2)
f_{a,g_1,f_3}(a, z1, z2) → f_{b,g_1,f_3}(b, z1, z2)
f_{a,g_1,a}(a, z1, z2) → f_{b,g_1,a}(b, z1, z2)
f_{a,g_1,g_1}(a, z1, z2) → f_{b,g_1,g_1}(b, z1, z2)
f_{a,g_1,b}(a, z1, z2) → f_{b,g_1,b}(b, z1, z2)
f_{a,b,f_3}(a, z1, z2) → f_{b,b,f_3}(b, z1, z2)
f_{a,b,a}(a, z1, z2) → f_{b,b,a}(b, z1, z2)
f_{a,b,g_1}(a, z1, z2) → f_{b,b,g_1}(b, z1, z2)
f_{a,b,b}(a, z1, z2) → f_{b,b,b}(b, z1, z2)
f_{f_3,a,f_3}(z0, a, z2) → f_{f_3,b,f_3}(z0, b, z2)
f_{f_3,a,a}(z0, a, z2) → f_{f_3,b,a}(z0, b, z2)
f_{f_3,a,g_1}(z0, a, z2) → f_{f_3,b,g_1}(z0, b, z2)
f_{f_3,a,b}(z0, a, z2) → f_{f_3,b,b}(z0, b, z2)
f_{a,a,f_3}(z0, a, z2) → f_{a,b,f_3}(z0, b, z2)
f_{a,a,a}(z0, a, z2) → f_{a,b,a}(z0, b, z2)
f_{a,a,g_1}(z0, a, z2) → f_{a,b,g_1}(z0, b, z2)
f_{a,a,b}(z0, a, z2) → f_{a,b,b}(z0, b, z2)
f_{g_1,a,f_3}(z0, a, z2) → f_{g_1,b,f_3}(z0, b, z2)
f_{g_1,a,a}(z0, a, z2) → f_{g_1,b,a}(z0, b, z2)
f_{g_1,a,g_1}(z0, a, z2) → f_{g_1,b,g_1}(z0, b, z2)
f_{g_1,a,b}(z0, a, z2) → f_{g_1,b,b}(z0, b, z2)
f_{b,a,f_3}(z0, a, z2) → f_{b,b,f_3}(z0, b, z2)
f_{b,a,a}(z0, a, z2) → f_{b,b,a}(z0, b, z2)
f_{b,a,g_1}(z0, a, z2) → f_{b,b,g_1}(z0, b, z2)
f_{b,a,b}(z0, a, z2) → f_{b,b,b}(z0, b, z2)
f_{f_3,f_3,a}(z0, z1, a) → f_{f_3,f_3,b}(z0, z1, b)
f_{f_3,a,a}(z0, z1, a) → f_{f_3,a,b}(z0, z1, b)
f_{f_3,g_1,a}(z0, z1, a) → f_{f_3,g_1,b}(z0, z1, b)
f_{f_3,b,a}(z0, z1, a) → f_{f_3,b,b}(z0, z1, b)
f_{a,f_3,a}(z0, z1, a) → f_{a,f_3,b}(z0, z1, b)
f_{a,a,a}(z0, z1, a) → f_{a,a,b}(z0, z1, b)
f_{a,g_1,a}(z0, z1, a) → f_{a,g_1,b}(z0, z1, b)
f_{a,b,a}(z0, z1, a) → f_{a,b,b}(z0, z1, b)
f_{g_1,f_3,a}(z0, z1, a) → f_{g_1,f_3,b}(z0, z1, b)
f_{g_1,a,a}(z0, z1, a) → f_{g_1,a,b}(z0, z1, b)
f_{g_1,g_1,a}(z0, z1, a) → f_{g_1,g_1,b}(z0, z1, b)
f_{g_1,b,a}(z0, z1, a) → f_{g_1,b,b}(z0, z1, b)
f_{b,f_3,a}(z0, z1, a) → f_{b,f_3,b}(z0, z1, b)
f_{b,a,a}(z0, z1, a) → f_{b,a,b}(z0, z1, b)
f_{b,g_1,a}(z0, z1, a) → f_{b,g_1,b}(z0, z1, b)
f_{b,b,a}(z0, z1, a) → f_{b,b,b}(z0, z1, b)
g_{a}(a) → g_{b}(b)

The relative TRS consists of the following S rules:

f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{f_3}(z))
f_{f_3,f_3,a}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{a}(z))
f_{f_3,f_3,g_1}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{g_1}(z))
f_{f_3,f_3,b}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{b}(z))
f_{f_3,a,f_3}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{f_3}(z))
f_{f_3,a,a}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{a}(z))
f_{f_3,a,g_1}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{g_1}(z))
f_{f_3,a,b}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{b}(z))
f_{f_3,g_1,f_3}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{f_3}(z))
f_{f_3,g_1,a}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{a}(z))
f_{f_3,g_1,g_1}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{g_1}(z))
f_{f_3,g_1,b}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{b}(z))
f_{f_3,b,f_3}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{f_3}(z))
f_{f_3,b,a}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{a}(z))
f_{f_3,b,g_1}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{g_1}(z))
f_{f_3,b,b}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{b}(z))
f_{a,f_3,f_3}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{f_3}(z))
f_{a,f_3,a}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{a}(z))
f_{a,f_3,g_1}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{g_1}(z))
f_{a,f_3,b}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{b}(z))
f_{a,a,f_3}(x, y, z) → f_{a,a,g_1}(x, y, g_{f_3}(z))
f_{a,a,a}(x, y, z) → f_{a,a,g_1}(x, y, g_{a}(z))
f_{a,a,g_1}(x, y, z) → f_{a,a,g_1}(x, y, g_{g_1}(z))
f_{a,a,b}(x, y, z) → f_{a,a,g_1}(x, y, g_{b}(z))
f_{a,g_1,f_3}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{f_3}(z))
f_{a,g_1,a}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{a}(z))
f_{a,g_1,g_1}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{g_1}(z))
f_{a,g_1,b}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{b}(z))
f_{a,b,f_3}(x, y, z) → f_{a,b,g_1}(x, y, g_{f_3}(z))
f_{a,b,a}(x, y, z) → f_{a,b,g_1}(x, y, g_{a}(z))
f_{a,b,g_1}(x, y, z) → f_{a,b,g_1}(x, y, g_{g_1}(z))
f_{a,b,b}(x, y, z) → f_{a,b,g_1}(x, y, g_{b}(z))
f_{g_1,f_3,f_3}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{f_3}(z))
f_{g_1,f_3,a}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{a}(z))
f_{g_1,f_3,g_1}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,b}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{b}(z))
f_{g_1,a,f_3}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{f_3}(z))
f_{g_1,a,a}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{a}(z))
f_{g_1,a,g_1}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{g_1}(z))
f_{g_1,a,b}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{b}(z))
f_{g_1,g_1,f_3}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{f_3}(z))
f_{g_1,g_1,a}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{a}(z))
f_{g_1,g_1,g_1}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{g_1}(z))
f_{g_1,g_1,b}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{b}(z))
f_{g_1,b,f_3}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{f_3}(z))
f_{g_1,b,a}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{a}(z))
f_{g_1,b,g_1}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{g_1}(z))
f_{g_1,b,b}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{b}(z))
f_{b,f_3,f_3}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{f_3}(z))
f_{b,f_3,a}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{a}(z))
f_{b,f_3,g_1}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{g_1}(z))
f_{b,f_3,b}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{b}(z))
f_{b,a,f_3}(x, y, z) → f_{b,a,g_1}(x, y, g_{f_3}(z))
f_{b,a,a}(x, y, z) → f_{b,a,g_1}(x, y, g_{a}(z))
f_{b,a,g_1}(x, y, z) → f_{b,a,g_1}(x, y, g_{g_1}(z))
f_{b,a,b}(x, y, z) → f_{b,a,g_1}(x, y, g_{b}(z))
f_{b,g_1,f_3}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{f_3}(z))
f_{b,g_1,a}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{a}(z))
f_{b,g_1,g_1}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,b}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{b}(z))
f_{b,b,f_3}(x, y, z) → f_{b,b,g_1}(x, y, g_{f_3}(z))
f_{b,b,a}(x, y, z) → f_{b,b,g_1}(x, y, g_{a}(z))
f_{b,b,g_1}(x, y, z) → f_{b,b,g_1}(x, y, g_{g_1}(z))
f_{b,b,b}(x, y, z) → f_{b,b,g_1}(x, y, g_{b}(z))

(5) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :

POL(f_{a,g_1,f_3}(x1, x2, x3)) =
/2\
\3/
 +
/30\
\22/
·x1 +
/33\
\03/
·x2 +
/33\
\33/
·x3

POL(a) =
/3\
\3/

POL(g_{f_3}(x1)) =
/0\
\2/
 +
/10\
\02/
·x1

POL(f_{b,g_1,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/12\
\00/
·x1 +
/11\
\00/
·x2 +
/20\
\00/
·x3

POL(b) =
/3\
\3/

POL(f_{a,g_1,a}(x1, x2, x3)) =
/2\
\1/
 +
/32\
\23/
·x1 +
/32\
\23/
·x2 +
/23\
\33/
·x3

POL(f_{a,g_1,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/30\
\00/
·x1 +
/32\
\00/
·x2 +
/20\
\00/
·x3

POL(f_{a,g_1,b}(x1, x2, x3)) =
/0\
\0/
 +
/30\
\10/
·x1 +
/32\
\12/
·x2 +
/21\
\11/
·x3

POL(g_{a}(x1)) =
/0\
\3/
 +
/10\
\12/
·x1

POL(g_{g_1}(x1)) =
/0\
\1/
 +
/10\
\32/
·x1

POL(g_{b}(x1)) =
/0\
\3/
 +
/10\
\00/
·x1

POL(f_{b,g_1,f_3}(x1, x2, x3)) =
/0\
\0/
 +
/12\
\23/
·x1 +
/12\
\03/
·x2 +
/33\
\33/
·x3

POL(f_{a,f_3,f_3}(x1, x2, x3)) =
/2\
\2/
 +
/12\
\11/
·x1 +
/12\
\00/
·x2 +
/33\
\33/
·x3

POL(f_{b,g_1,a}(x1, x2, x3)) =
/1\
\2/
 +
/32\
\22/
·x1 +
/31\
\22/
·x2 +
/23\
\33/
·x3

POL(f_{a,f_3,a}(x1, x2, x3)) =
/2\
\2/
 +
/12\
\11/
·x1 +
/20\
\00/
·x2 +
/20\
\02/
·x3

POL(f_{a,f_3,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/10\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{b,g_1,b}(x1, x2, x3)) =
/0\
\2/
 +
/12\
\00/
·x1 +
/31\
\11/
·x2 +
/21\
\11/
·x3

POL(f_{a,f_3,b}(x1, x2, x3)) =
/1\
\0/
 +
/12\
\10/
·x1 +
/10\
\00/
·x2 +
/10\
\10/
·x3

POL(f_{a,a,f_3}(x1, x2, x3)) =
/2\
\0/
 +
/31\
\30/
·x1 +
/10\
\01/
·x2 +
/33\
\33/
·x3

POL(f_{a,a,a}(x1, x2, x3)) =
/0\
\0/
 +
/32\
\01/
·x1 +
/30\
\22/
·x2 +
/23\
\23/
·x3

POL(f_{a,a,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/21\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{a,a,b}(x1, x2, x3)) =
/0\
\2/
 +
/31\
\00/
·x1 +
/20\
\20/
·x2 +
/21\
\00/
·x3

POL(f_{a,b,f_3}(x1, x2, x3)) =
/2\
\0/
 +
/20\
\30/
·x1 +
/10\
\00/
·x2 +
/33\
\33/
·x3

POL(f_{a,b,a}(x1, x2, x3)) =
/0\
\3/
 +
/31\
\00/
·x1 +
/20\
\00/
·x2 +
/23\
\13/
·x3

POL(f_{a,b,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/20\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{a,b,b}(x1, x2, x3)) =
/0\
\2/
 +
/21\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{b,f_3,f_3}(x1, x2, x3)) =
/2\
\2/
 +
/21\
\00/
·x1 +
/12\
\00/
·x2 +
/13\
\00/
·x3

POL(f_{b,f_3,a}(x1, x2, x3)) =
/3\
\2/
 +
/20\
\00/
·x1 +
/10\
\00/
·x2 +
/20\
\02/
·x3

POL(f_{b,f_3,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/10\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{b,f_3,b}(x1, x2, x3)) =
/1\
\2/
 +
/20\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{b,a,f_3}(x1, x2, x3)) =
/2\
\2/
 +
/31\
\00/
·x1 +
/10\
\00/
·x2 +
/33\
\33/
·x3

POL(f_{b,a,a}(x1, x2, x3)) =
/3\
\3/
 +
/31\
\00/
·x1 +
/10\
\21/
·x2 +
/20\
\12/
·x3

POL(f_{b,a,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/30\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{b,a,b}(x1, x2, x3)) =
/2\
\2/
 +
/30\
\00/
·x1 +
/10\
\20/
·x2 +
/10\
\00/
·x3

POL(f_{b,b,f_3}(x1, x2, x3)) =
/2\
\0/
 +
/11\
\00/
·x1 +
/10\
\00/
·x2 +
/33\
\33/
·x3

POL(f_{b,b,a}(x1, x2, x3)) =
/2\
\3/
 +
/30\
\00/
·x1 +
/10\
\00/
·x2 +
/20\
\12/
·x3

POL(f_{b,b,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/10\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{b,b,b}(x1, x2, x3)) =
/0\
\0/
 +
/30\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{f_3,a,f_3}(x1, x2, x3)) =
/2\
\3/
 +
/23\
\33/
·x1 +
/10\
\32/
·x2 +
/33\
\33/
·x3

POL(f_{f_3,b,f_3}(x1, x2, x3)) =
/2\
\2/
 +
/22\
\21/
·x1 +
/10\
\01/
·x2 +
/31\
\33/
·x3

POL(f_{f_3,a,a}(x1, x2, x3)) =
/0\
\3/
 +
/33\
\33/
·x1 +
/20\
\01/
·x2 +
/32\
\10/
·x3

POL(f_{f_3,b,a}(x1, x2, x3)) =
/0\
\3/
 +
/33\
\02/
·x1 +
/10\
\00/
·x2 +
/22\
\10/
·x3

POL(f_{f_3,a,g_1}(x1, x2, x3)) =
/0\
\1/
 +
/12\
\33/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{f_3,b,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/11\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{f_3,a,b}(x1, x2, x3)) =
/0\
\1/
 +
/33\
\33/
·x1 +
/20\
\01/
·x2 +
/23\
\00/
·x3

POL(f_{f_3,b,b}(x1, x2, x3)) =
/3\
\2/
 +
/12\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{g_1,a,f_3}(x1, x2, x3)) =
/3\
\3/
 +
/33\
\33/
·x1 +
/10\
\32/
·x2 +
/33\
\33/
·x3

POL(f_{g_1,b,f_3}(x1, x2, x3)) =
/3\
\2/
 +
/22\
\30/
·x1 +
/10\
\01/
·x2 +
/10\
\31/
·x3

POL(f_{g_1,a,a}(x1, x2, x3)) =
/1\
\2/
 +
/33\
\33/
·x1 +
/32\
\32/
·x2 +
/30\
\02/
·x3

POL(f_{g_1,b,a}(x1, x2, x3)) =
/3\
\3/
 +
/33\
\20/
·x1 +
/10\
\01/
·x2 +
/30\
\02/
·x3

POL(f_{g_1,a,g_1}(x1, x2, x3)) =
/1\
\0/
 +
/30\
\00/
·x1 +
/10\
\31/
·x2 +
/10\
\00/
·x3

POL(f_{g_1,b,g_1}(x1, x2, x3)) =
/1\
\0/
 +
/20\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{g_1,a,b}(x1, x2, x3)) =
/1\
\2/
 +
/33\
\20/
·x1 +
/10\
\32/
·x2 +
/10\
\10/
·x3

POL(f_{g_1,b,b}(x1, x2, x3)) =
/1\
\2/
 +
/33\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{f_3,f_3,a}(x1, x2, x3)) =
/3\
\3/
 +
/23\
\23/
·x1 +
/32\
\22/
·x2 +
/21\
\10/
·x3

POL(f_{f_3,f_3,b}(x1, x2, x3)) =
/1\
\3/
 +
/20\
\02/
·x1 +
/20\
\22/
·x2 +
/30\
\01/
·x3

POL(f_{f_3,g_1,a}(x1, x2, x3)) =
/2\
\3/
 +
/33\
\32/
·x1 +
/23\
\22/
·x2 +
/30\
\12/
·x3

POL(f_{f_3,g_1,b}(x1, x2, x3)) =
/0\
\0/
 +
/30\
\32/
·x1 +
/22\
\22/
·x2 +
/10\
\00/
·x3

POL(f_{g_1,f_3,a}(x1, x2, x3)) =
/0\
\3/
 +
/32\
\22/
·x1 +
/33\
\33/
·x2 +
/10\
\01/
·x3

POL(f_{g_1,f_3,b}(x1, x2, x3)) =
/0\
\2/
 +
/30\
\00/
·x1 +
/10\
\33/
·x2 +
/10\
\10/
·x3

POL(f_{g_1,g_1,a}(x1, x2, x3)) =
/0\
\1/
 +
/32\
\32/
·x1 +
/33\
\23/
·x2 +
/33\
\12/
·x3

POL(f_{g_1,g_1,b}(x1, x2, x3)) =
/0\
\0/
 +
/32\
\22/
·x1 +
/32\
\00/
·x2 +
/10\
\02/
·x3

POL(f_{f_3,f_3,f_3}(x1, x2, x3)) =
/1\
\0/
 +
/30\
\30/
·x1 +
/30\
\02/
·x2 +
/10\
\21/
·x3

POL(f_{f_3,f_3,g_1}(x1, x2, x3)) =
/1\
\0/
 +
/20\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{f_3,g_1,f_3}(x1, x2, x3)) =
/0\
\1/
 +
/20\
\01/
·x1 +
/20\
\10/
·x2 +
/11\
\01/
·x3

POL(f_{f_3,g_1,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/10\
\00/
·x1 +
/20\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{g_1,f_3,f_3}(x1, x2, x3)) =
/0\
\0/
 +
/32\
\00/
·x1 +
/10\
\00/
·x2 +
/12\
\01/
·x3

POL(f_{g_1,f_3,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/10\
\00/
·x1 +
/10\
\00/
·x2 +
/10\
\00/
·x3

POL(f_{g_1,g_1,f_3}(x1, x2, x3)) =
/0\
\0/
 +
/30\
\20/
·x1 +
/20\
\00/
·x2 +
/11\
\01/
·x3

POL(f_{g_1,g_1,g_1}(x1, x2, x3)) =
/0\
\0/
 +
/30\
\00/
·x1 +
/20\
\00/
·x2 +
/10\
\00/
·x3
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

f_{a,g_1,f_3}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,a}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,g_1}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,b}(a, g_{f_3}(y), z) → f_{b,g_1,g_1}(b, g_{f_3}(y), g_{f_3}(y))
f_{a,g_1,f_3}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,a}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,g_1}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,b}(a, g_{a}(y), z) → f_{b,g_1,g_1}(b, g_{a}(y), g_{a}(y))
f_{a,g_1,f_3}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,a}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,g_1}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,b}(a, g_{g_1}(y), z) → f_{b,g_1,g_1}(b, g_{g_1}(y), g_{g_1}(y))
f_{a,g_1,f_3}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{a,g_1,a}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{a,g_1,g_1}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{a,g_1,b}(a, g_{b}(y), z) → f_{b,g_1,g_1}(b, g_{b}(y), g_{b}(y))
f_{b,g_1,f_3}(b, g_{f_3}(y), z) → f_{a,f_3,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{f_3}(y), z) → f_{a,f_3,a}(a, y, z)
f_{b,g_1,g_1}(b, g_{f_3}(y), z) → f_{a,f_3,g_1}(a, y, z)
f_{b,g_1,b}(b, g_{f_3}(y), z) → f_{a,f_3,b}(a, y, z)
f_{b,g_1,f_3}(b, g_{a}(y), z) → f_{a,a,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{a}(y), z) → f_{a,a,a}(a, y, z)
f_{b,g_1,g_1}(b, g_{a}(y), z) → f_{a,a,g_1}(a, y, z)
f_{b,g_1,g_1}(b, g_{g_1}(y), z) → f_{a,g_1,g_1}(a, y, z)
f_{b,g_1,b}(b, g_{g_1}(y), z) → f_{a,g_1,b}(a, y, z)
f_{b,g_1,f_3}(b, g_{b}(y), z) → f_{a,b,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{b}(y), z) → f_{a,b,a}(a, y, z)
f_{b,g_1,g_1}(b, g_{b}(y), z) → f_{a,b,g_1}(a, y, z)
f_{b,g_1,b}(b, g_{b}(y), z) → f_{a,b,b}(a, y, z)
f_{a,f_3,a}(a, z1, z2) → f_{b,f_3,a}(b, z1, z2)
f_{a,f_3,b}(a, z1, z2) → f_{b,f_3,b}(b, z1, z2)
f_{a,a,b}(a, z1, z2) → f_{b,a,b}(b, z1, z2)
f_{a,g_1,f_3}(a, z1, z2) → f_{b,g_1,f_3}(b, z1, z2)
f_{a,g_1,a}(a, z1, z2) → f_{b,g_1,a}(b, z1, z2)
f_{a,b,a}(a, z1, z2) → f_{b,b,a}(b, z1, z2)
f_{a,b,g_1}(a, z1, z2) → f_{b,b,g_1}(b, z1, z2)
f_{f_3,a,a}(z0, a, z2) → f_{f_3,b,a}(z0, b, z2)
f_{a,a,a}(z0, a, z2) → f_{a,b,a}(z0, b, z2)
f_{a,a,b}(z0, a, z2) → f_{a,b,b}(z0, b, z2)
f_{g_1,a,a}(z0, a, z2) → f_{g_1,b,a}(z0, b, z2)
f_{b,a,a}(z0, a, z2) → f_{b,b,a}(z0, b, z2)
f_{b,a,b}(z0, a, z2) → f_{b,b,b}(z0, b, z2)
f_{f_3,f_3,a}(z0, z1, a) → f_{f_3,f_3,b}(z0, z1, b)
f_{f_3,g_1,a}(z0, z1, a) → f_{f_3,g_1,b}(z0, z1, b)
f_{f_3,b,a}(z0, z1, a) → f_{f_3,b,b}(z0, z1, b)
f_{a,f_3,a}(z0, z1, a) → f_{a,f_3,b}(z0, z1, b)
f_{a,a,a}(z0, z1, a) → f_{a,a,b}(z0, z1, b)
f_{a,g_1,a}(z0, z1, a) → f_{a,g_1,b}(z0, z1, b)
f_{a,b,a}(z0, z1, a) → f_{a,b,b}(z0, z1, b)
f_{g_1,a,a}(z0, z1, a) → f_{g_1,a,b}(z0, z1, b)
f_{g_1,g_1,a}(z0, z1, a) → f_{g_1,g_1,b}(z0, z1, b)
f_{g_1,b,a}(z0, z1, a) → f_{g_1,b,b}(z0, z1, b)
f_{b,f_3,a}(z0, z1, a) → f_{b,f_3,b}(z0, z1, b)
f_{b,a,a}(z0, z1, a) → f_{b,a,b}(z0, z1, b)
f_{b,g_1,a}(z0, z1, a) → f_{b,g_1,b}(z0, z1, b)
f_{b,b,a}(z0, z1, a) → f_{b,b,b}(z0, z1, b)
Rules from S:

f_{f_3,f_3,a}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{a}(z))
f_{f_3,a,f_3}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{f_3}(z))
f_{f_3,g_1,a}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{a}(z))
f_{f_3,b,f_3}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{f_3}(z))
f_{f_3,b,b}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{b}(z))
f_{a,f_3,f_3}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{f_3}(z))
f_{a,f_3,a}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{a}(z))
f_{a,f_3,b}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{b}(z))
f_{a,a,f_3}(x, y, z) → f_{a,a,g_1}(x, y, g_{f_3}(z))
f_{a,g_1,f_3}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{f_3}(z))
f_{a,g_1,a}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{a}(z))
f_{a,b,f_3}(x, y, z) → f_{a,b,g_1}(x, y, g_{f_3}(z))
f_{g_1,a,f_3}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{f_3}(z))
f_{g_1,b,f_3}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{f_3}(z))
f_{g_1,b,a}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{a}(z))
f_{b,f_3,f_3}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{f_3}(z))
f_{b,f_3,a}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{a}(z))
f_{b,f_3,b}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{b}(z))
f_{b,a,f_3}(x, y, z) → f_{b,a,g_1}(x, y, g_{f_3}(z))
f_{b,a,a}(x, y, z) → f_{b,a,g_1}(x, y, g_{a}(z))
f_{b,a,b}(x, y, z) → f_{b,a,g_1}(x, y, g_{b}(z))
f_{b,g_1,a}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{a}(z))
f_{b,b,f_3}(x, y, z) → f_{b,b,g_1}(x, y, g_{f_3}(z))
f_{b,b,a}(x, y, z) → f_{b,b,g_1}(x, y, g_{a}(z))


(6) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f_{b,g_1,b}(b, g_{a}(y), z) → f_{a,a,b}(a, y, z)
f_{b,g_1,f_3}(b, g_{g_1}(y), z) → f_{a,g_1,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{g_1}(y), z) → f_{a,g_1,a}(a, y, z)
f_{a,f_3,f_3}(a, z1, z2) → f_{b,f_3,f_3}(b, z1, z2)
f_{a,f_3,g_1}(a, z1, z2) → f_{b,f_3,g_1}(b, z1, z2)
f_{a,a,f_3}(a, z1, z2) → f_{b,a,f_3}(b, z1, z2)
f_{a,a,a}(a, z1, z2) → f_{b,a,a}(b, z1, z2)
f_{a,a,g_1}(a, z1, z2) → f_{b,a,g_1}(b, z1, z2)
f_{a,g_1,g_1}(a, z1, z2) → f_{b,g_1,g_1}(b, z1, z2)
f_{a,g_1,b}(a, z1, z2) → f_{b,g_1,b}(b, z1, z2)
f_{a,b,f_3}(a, z1, z2) → f_{b,b,f_3}(b, z1, z2)
f_{a,b,b}(a, z1, z2) → f_{b,b,b}(b, z1, z2)
f_{f_3,a,f_3}(z0, a, z2) → f_{f_3,b,f_3}(z0, b, z2)
f_{f_3,a,g_1}(z0, a, z2) → f_{f_3,b,g_1}(z0, b, z2)
f_{f_3,a,b}(z0, a, z2) → f_{f_3,b,b}(z0, b, z2)
f_{a,a,f_3}(z0, a, z2) → f_{a,b,f_3}(z0, b, z2)
f_{a,a,g_1}(z0, a, z2) → f_{a,b,g_1}(z0, b, z2)
f_{g_1,a,f_3}(z0, a, z2) → f_{g_1,b,f_3}(z0, b, z2)
f_{g_1,a,g_1}(z0, a, z2) → f_{g_1,b,g_1}(z0, b, z2)
f_{g_1,a,b}(z0, a, z2) → f_{g_1,b,b}(z0, b, z2)
f_{b,a,f_3}(z0, a, z2) → f_{b,b,f_3}(z0, b, z2)
f_{b,a,g_1}(z0, a, z2) → f_{b,b,g_1}(z0, b, z2)
f_{f_3,a,a}(z0, z1, a) → f_{f_3,a,b}(z0, z1, b)
f_{g_1,f_3,a}(z0, z1, a) → f_{g_1,f_3,b}(z0, z1, b)
g_{a}(a) → g_{b}(b)

The relative TRS consists of the following S rules:

f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{f_3}(z))
f_{f_3,f_3,g_1}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{g_1}(z))
f_{f_3,f_3,b}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{b}(z))
f_{f_3,a,a}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{a}(z))
f_{f_3,a,g_1}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{g_1}(z))
f_{f_3,a,b}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{b}(z))
f_{f_3,g_1,f_3}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{f_3}(z))
f_{f_3,g_1,g_1}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{g_1}(z))
f_{f_3,g_1,b}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{b}(z))
f_{f_3,b,a}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{a}(z))
f_{f_3,b,g_1}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{g_1}(z))
f_{a,f_3,g_1}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{g_1}(z))
f_{a,a,a}(x, y, z) → f_{a,a,g_1}(x, y, g_{a}(z))
f_{a,a,g_1}(x, y, z) → f_{a,a,g_1}(x, y, g_{g_1}(z))
f_{a,a,b}(x, y, z) → f_{a,a,g_1}(x, y, g_{b}(z))
f_{a,g_1,g_1}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{g_1}(z))
f_{a,g_1,b}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{b}(z))
f_{a,b,a}(x, y, z) → f_{a,b,g_1}(x, y, g_{a}(z))
f_{a,b,g_1}(x, y, z) → f_{a,b,g_1}(x, y, g_{g_1}(z))
f_{a,b,b}(x, y, z) → f_{a,b,g_1}(x, y, g_{b}(z))
f_{g_1,f_3,f_3}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{f_3}(z))
f_{g_1,f_3,a}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{a}(z))
f_{g_1,f_3,g_1}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,b}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{b}(z))
f_{g_1,a,a}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{a}(z))
f_{g_1,a,g_1}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{g_1}(z))
f_{g_1,a,b}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{b}(z))
f_{g_1,g_1,f_3}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{f_3}(z))
f_{g_1,g_1,a}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{a}(z))
f_{g_1,g_1,g_1}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{g_1}(z))
f_{g_1,g_1,b}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{b}(z))
f_{g_1,b,g_1}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{g_1}(z))
f_{g_1,b,b}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{b}(z))
f_{b,f_3,g_1}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{g_1}(z))
f_{b,a,g_1}(x, y, z) → f_{b,a,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,f_3}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{f_3}(z))
f_{b,g_1,g_1}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,b}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{b}(z))
f_{b,b,g_1}(x, y, z) → f_{b,b,g_1}(x, y, g_{g_1}(z))
f_{b,b,b}(x, y, z) → f_{b,b,g_1}(x, y, g_{b}(z))

(7) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(a) = 0   
POL(b) = 0   
POL(f_{a,a,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,a,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,a,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,b,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,b,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,b,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,f_3,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,f_3,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,g_1,a}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,g_1,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,g_1,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,g_1,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{b,a,a}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,a,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{b,b,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,f_3,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{b,g_1,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{b,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,a,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,a,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,b,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,b,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,b,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,f_3,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,f_3,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,g_1,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,g_1,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,a,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,a,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,a,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,a,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,b,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,b,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,f_3,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,f_3,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,f_3,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,g_1,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,g_1,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,g_1,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(g_{a}(x1)) = x1   
POL(g_{b}(x1)) = x1   
POL(g_{f_3}(x1)) = x1   
POL(g_{g_1}(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

f_{b,g_1,f_3}(b, g_{g_1}(y), z) → f_{a,g_1,f_3}(a, y, z)
f_{b,g_1,a}(b, g_{g_1}(y), z) → f_{a,g_1,a}(a, y, z)
f_{a,f_3,f_3}(a, z1, z2) → f_{b,f_3,f_3}(b, z1, z2)
f_{a,f_3,g_1}(a, z1, z2) → f_{b,f_3,g_1}(b, z1, z2)
f_{a,a,f_3}(a, z1, z2) → f_{b,a,f_3}(b, z1, z2)
f_{a,a,a}(a, z1, z2) → f_{b,a,a}(b, z1, z2)
f_{a,g_1,g_1}(a, z1, z2) → f_{b,g_1,g_1}(b, z1, z2)
f_{a,g_1,b}(a, z1, z2) → f_{b,g_1,b}(b, z1, z2)
f_{a,b,f_3}(a, z1, z2) → f_{b,b,f_3}(b, z1, z2)
f_{f_3,a,f_3}(z0, a, z2) → f_{f_3,b,f_3}(z0, b, z2)
f_{f_3,a,b}(z0, a, z2) → f_{f_3,b,b}(z0, b, z2)
f_{g_1,a,f_3}(z0, a, z2) → f_{g_1,b,f_3}(z0, b, z2)
f_{g_1,a,g_1}(z0, a, z2) → f_{g_1,b,g_1}(z0, b, z2)
f_{g_1,f_3,a}(z0, z1, a) → f_{g_1,f_3,b}(z0, z1, b)
Rules from S:

f_{f_3,f_3,f_3}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{f_3}(z))
f_{f_3,f_3,b}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{b}(z))
f_{f_3,a,a}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{a}(z))
f_{f_3,a,b}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{b}(z))
f_{f_3,g_1,f_3}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{f_3}(z))
f_{f_3,g_1,b}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{b}(z))
f_{f_3,b,a}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{a}(z))
f_{a,a,a}(x, y, z) → f_{a,a,g_1}(x, y, g_{a}(z))
f_{a,b,a}(x, y, z) → f_{a,b,g_1}(x, y, g_{a}(z))
f_{a,b,b}(x, y, z) → f_{a,b,g_1}(x, y, g_{b}(z))
f_{g_1,f_3,f_3}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{f_3}(z))
f_{g_1,f_3,a}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{a}(z))
f_{g_1,g_1,f_3}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{f_3}(z))
f_{g_1,g_1,a}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{a}(z))
f_{g_1,g_1,b}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{b}(z))
f_{g_1,b,b}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{b}(z))
f_{b,g_1,f_3}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{f_3}(z))
f_{b,b,b}(x, y, z) → f_{b,b,g_1}(x, y, g_{b}(z))


(8) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f_{b,g_1,b}(b, g_{a}(y), z) → f_{a,a,b}(a, y, z)
f_{a,a,g_1}(a, z1, z2) → f_{b,a,g_1}(b, z1, z2)
f_{a,b,b}(a, z1, z2) → f_{b,b,b}(b, z1, z2)
f_{f_3,a,g_1}(z0, a, z2) → f_{f_3,b,g_1}(z0, b, z2)
f_{a,a,f_3}(z0, a, z2) → f_{a,b,f_3}(z0, b, z2)
f_{a,a,g_1}(z0, a, z2) → f_{a,b,g_1}(z0, b, z2)
f_{g_1,a,b}(z0, a, z2) → f_{g_1,b,b}(z0, b, z2)
f_{b,a,f_3}(z0, a, z2) → f_{b,b,f_3}(z0, b, z2)
f_{b,a,g_1}(z0, a, z2) → f_{b,b,g_1}(z0, b, z2)
f_{f_3,a,a}(z0, z1, a) → f_{f_3,a,b}(z0, z1, b)
g_{a}(a) → g_{b}(b)

The relative TRS consists of the following S rules:

f_{f_3,f_3,g_1}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{g_1}(z))
f_{f_3,a,g_1}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{g_1}(z))
f_{f_3,g_1,g_1}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{g_1}(z))
f_{f_3,b,g_1}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{g_1}(z))
f_{a,f_3,g_1}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{g_1}(z))
f_{a,a,g_1}(x, y, z) → f_{a,a,g_1}(x, y, g_{g_1}(z))
f_{a,a,b}(x, y, z) → f_{a,a,g_1}(x, y, g_{b}(z))
f_{a,g_1,g_1}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{g_1}(z))
f_{a,g_1,b}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{b}(z))
f_{a,b,g_1}(x, y, z) → f_{a,b,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,g_1}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,b}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{b}(z))
f_{g_1,a,a}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{a}(z))
f_{g_1,a,g_1}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{g_1}(z))
f_{g_1,a,b}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{b}(z))
f_{g_1,g_1,g_1}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{g_1}(z))
f_{g_1,b,g_1}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{g_1}(z))
f_{b,f_3,g_1}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{g_1}(z))
f_{b,a,g_1}(x, y, z) → f_{b,a,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,g_1}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,b}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{b}(z))
f_{b,b,g_1}(x, y, z) → f_{b,b,g_1}(x, y, g_{g_1}(z))

(9) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(a) = 1   
POL(b) = 1   
POL(f_{a,a,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,a,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,b,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,b,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,g_1,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,a,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{b,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,a}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,b,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,a,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,a,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,b,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,f_3,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{g_1,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(g_{a}(x1)) = x1   
POL(g_{b}(x1)) = x1   
POL(g_{g_1}(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

f_{g_1,a,b}(z0, a, z2) → f_{g_1,b,b}(z0, b, z2)
f_{b,a,f_3}(z0, a, z2) → f_{b,b,f_3}(z0, b, z2)
Rules from S:

f_{a,g_1,b}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{b}(z))
f_{g_1,f_3,b}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{b}(z))
f_{g_1,a,a}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{a}(z))
f_{g_1,a,b}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{b}(z))


(10) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f_{b,g_1,b}(b, g_{a}(y), z) → f_{a,a,b}(a, y, z)
f_{a,a,g_1}(a, z1, z2) → f_{b,a,g_1}(b, z1, z2)
f_{a,b,b}(a, z1, z2) → f_{b,b,b}(b, z1, z2)
f_{f_3,a,g_1}(z0, a, z2) → f_{f_3,b,g_1}(z0, b, z2)
f_{a,a,f_3}(z0, a, z2) → f_{a,b,f_3}(z0, b, z2)
f_{a,a,g_1}(z0, a, z2) → f_{a,b,g_1}(z0, b, z2)
f_{b,a,g_1}(z0, a, z2) → f_{b,b,g_1}(z0, b, z2)
f_{f_3,a,a}(z0, z1, a) → f_{f_3,a,b}(z0, z1, b)
g_{a}(a) → g_{b}(b)

The relative TRS consists of the following S rules:

f_{f_3,f_3,g_1}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{g_1}(z))
f_{f_3,a,g_1}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{g_1}(z))
f_{f_3,g_1,g_1}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{g_1}(z))
f_{f_3,b,g_1}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{g_1}(z))
f_{a,f_3,g_1}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{g_1}(z))
f_{a,a,g_1}(x, y, z) → f_{a,a,g_1}(x, y, g_{g_1}(z))
f_{a,a,b}(x, y, z) → f_{a,a,g_1}(x, y, g_{b}(z))
f_{a,g_1,g_1}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{g_1}(z))
f_{a,b,g_1}(x, y, z) → f_{a,b,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,g_1}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{g_1}(z))
f_{g_1,a,g_1}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{g_1}(z))
f_{g_1,g_1,g_1}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{g_1}(z))
f_{g_1,b,g_1}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{g_1}(z))
f_{b,f_3,g_1}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{g_1}(z))
f_{b,a,g_1}(x, y, z) → f_{b,a,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,g_1}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,b}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{b}(z))
f_{b,b,g_1}(x, y, z) → f_{b,b,g_1}(x, y, g_{g_1}(z))

(11) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(a) = 1   
POL(b) = 1   
POL(f_{a,a,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,a,f_3}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,a,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,b,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,b,f_3}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,a,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{b,b,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,a}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,a,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{f_3,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(g_{a}(x1)) = 1 + x1   
POL(g_{b}(x1)) = x1   
POL(g_{g_1}(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

f_{a,b,b}(a, z1, z2) → f_{b,b,b}(b, z1, z2)
f_{f_3,a,g_1}(z0, a, z2) → f_{f_3,b,g_1}(z0, b, z2)
f_{a,a,f_3}(z0, a, z2) → f_{a,b,f_3}(z0, b, z2)
f_{a,a,g_1}(z0, a, z2) → f_{a,b,g_1}(z0, b, z2)
f_{b,a,g_1}(z0, a, z2) → f_{b,b,g_1}(z0, b, z2)
f_{f_3,a,a}(z0, z1, a) → f_{f_3,a,b}(z0, z1, b)
g_{a}(a) → g_{b}(b)
Rules from S:
none


(12) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f_{b,g_1,b}(b, g_{a}(y), z) → f_{a,a,b}(a, y, z)
f_{a,a,g_1}(a, z1, z2) → f_{b,a,g_1}(b, z1, z2)

The relative TRS consists of the following S rules:

f_{f_3,f_3,g_1}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{g_1}(z))
f_{f_3,a,g_1}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{g_1}(z))
f_{f_3,g_1,g_1}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{g_1}(z))
f_{f_3,b,g_1}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{g_1}(z))
f_{a,f_3,g_1}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{g_1}(z))
f_{a,a,g_1}(x, y, z) → f_{a,a,g_1}(x, y, g_{g_1}(z))
f_{a,a,b}(x, y, z) → f_{a,a,g_1}(x, y, g_{b}(z))
f_{a,g_1,g_1}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{g_1}(z))
f_{a,b,g_1}(x, y, z) → f_{a,b,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,g_1}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{g_1}(z))
f_{g_1,a,g_1}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{g_1}(z))
f_{g_1,g_1,g_1}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{g_1}(z))
f_{g_1,b,g_1}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{g_1}(z))
f_{b,f_3,g_1}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{g_1}(z))
f_{b,a,g_1}(x, y, z) → f_{b,a,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,g_1}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,b}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{b}(z))
f_{b,b,g_1}(x, y, z) → f_{b,b,g_1}(x, y, g_{g_1}(z))

(13) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(a) = 0   
POL(b) = 0   
POL(f_{a,a,b}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{b,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(g_{a}(x1)) = 1 + x1   
POL(g_{b}(x1)) = x1   
POL(g_{g_1}(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

f_{b,g_1,b}(b, g_{a}(y), z) → f_{a,a,b}(a, y, z)
Rules from S:

f_{b,g_1,b}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{b}(z))


(14) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f_{a,a,g_1}(a, z1, z2) → f_{b,a,g_1}(b, z1, z2)

The relative TRS consists of the following S rules:

f_{f_3,f_3,g_1}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{g_1}(z))
f_{f_3,a,g_1}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{g_1}(z))
f_{f_3,g_1,g_1}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{g_1}(z))
f_{f_3,b,g_1}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{g_1}(z))
f_{a,f_3,g_1}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{g_1}(z))
f_{a,a,g_1}(x, y, z) → f_{a,a,g_1}(x, y, g_{g_1}(z))
f_{a,a,b}(x, y, z) → f_{a,a,g_1}(x, y, g_{b}(z))
f_{a,g_1,g_1}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{g_1}(z))
f_{a,b,g_1}(x, y, z) → f_{a,b,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,g_1}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{g_1}(z))
f_{g_1,a,g_1}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{g_1}(z))
f_{g_1,g_1,g_1}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{g_1}(z))
f_{g_1,b,g_1}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{g_1}(z))
f_{b,f_3,g_1}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{g_1}(z))
f_{b,a,g_1}(x, y, z) → f_{b,a,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,g_1}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{g_1}(z))
f_{b,b,g_1}(x, y, z) → f_{b,b,g_1}(x, y, g_{g_1}(z))

(15) RelTRSRRRProof (EQUIVALENT transformation)

We used the following monotonic ordering for rule removal:
Polynomial interpretation [POLO]:

POL(a) = 1   
POL(b) = 0   
POL(f_{a,a,b}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,a,g_1}(x1, x2, x3)) = 1 + x1 + x2 + x3   
POL(f_{a,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{a,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{b,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{f_3,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,a,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,b,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,f_3,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(f_{g_1,g_1,g_1}(x1, x2, x3)) = x1 + x2 + x3   
POL(g_{b}(x1)) = x1   
POL(g_{g_1}(x1)) = x1   
With this ordering the following rules can be removed [MATRO] because they are oriented strictly:
Rules from R:

f_{a,a,g_1}(a, z1, z2) → f_{b,a,g_1}(b, z1, z2)
Rules from S:
none


(16) Obligation:

Relative term rewrite system:
R is empty.
The relative TRS consists of the following S rules:

f_{f_3,f_3,g_1}(x, y, z) → f_{f_3,f_3,g_1}(x, y, g_{g_1}(z))
f_{f_3,a,g_1}(x, y, z) → f_{f_3,a,g_1}(x, y, g_{g_1}(z))
f_{f_3,g_1,g_1}(x, y, z) → f_{f_3,g_1,g_1}(x, y, g_{g_1}(z))
f_{f_3,b,g_1}(x, y, z) → f_{f_3,b,g_1}(x, y, g_{g_1}(z))
f_{a,f_3,g_1}(x, y, z) → f_{a,f_3,g_1}(x, y, g_{g_1}(z))
f_{a,a,g_1}(x, y, z) → f_{a,a,g_1}(x, y, g_{g_1}(z))
f_{a,a,b}(x, y, z) → f_{a,a,g_1}(x, y, g_{b}(z))
f_{a,g_1,g_1}(x, y, z) → f_{a,g_1,g_1}(x, y, g_{g_1}(z))
f_{a,b,g_1}(x, y, z) → f_{a,b,g_1}(x, y, g_{g_1}(z))
f_{g_1,f_3,g_1}(x, y, z) → f_{g_1,f_3,g_1}(x, y, g_{g_1}(z))
f_{g_1,a,g_1}(x, y, z) → f_{g_1,a,g_1}(x, y, g_{g_1}(z))
f_{g_1,g_1,g_1}(x, y, z) → f_{g_1,g_1,g_1}(x, y, g_{g_1}(z))
f_{g_1,b,g_1}(x, y, z) → f_{g_1,b,g_1}(x, y, g_{g_1}(z))
f_{b,f_3,g_1}(x, y, z) → f_{b,f_3,g_1}(x, y, g_{g_1}(z))
f_{b,a,g_1}(x, y, z) → f_{b,a,g_1}(x, y, g_{g_1}(z))
f_{b,g_1,g_1}(x, y, z) → f_{b,g_1,g_1}(x, y, g_{g_1}(z))
f_{b,b,g_1}(x, y, z) → f_{b,b,g_1}(x, y, g_{g_1}(z))

(17) RIsEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(18) YES