The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

i(x, x) → i(a, b)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

I(z0, z0) → c1(I(a, b))
G(z0, z0) → c2(G(a, b))
G(a, g(z0, g(b, g(a, g(z0, z1))))) → c3(G(a, g(a, g(a, g(z0, g(b, g(b, z1)))))), G(a, g(a, g(z0, g(b, g(b, z1))))), G(a, g(z0, g(b, g(b, z1)))), G(z0, g(b, g(b, z1))), G(b, g(b, z1)), G(b, z1))
H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))

S tuples:

I(z0, z0) → c1(I(a, b))
G(z0, z0) → c2(G(a, b))
G(a, g(z0, g(b, g(a, g(z0, z1))))) → c3(G(a, g(a, g(a, g(z0, g(b, g(b, z1)))))), G(a, g(a, g(z0, g(b, g(b, z1))))), G(a, g(z0, g(b, g(b, z1)))), G(z0, g(b, g(b, z1))), G(b, g(b, z1)), G(b, z1))
H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

I, G, H, F

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7, c8

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

I(z0, z0) → c1(I(a, b))
G(z0, z0) → c2(G(a, b))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

G(a, g(z0, g(b, g(a, g(z0, z1))))) → c3(G(a, g(a, g(a, g(z0, g(b, g(b, z1)))))), G(a, g(a, g(z0, g(b, g(b, z1))))), G(a, g(z0, g(b, g(b, z1)))), G(z0, g(b, g(b, z1))), G(b, g(b, z1)), G(b, z1))
H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))

S tuples:

G(a, g(z0, g(b, g(a, g(z0, z1))))) → c3(G(a, g(a, g(a, g(z0, g(b, g(b, z1)))))), G(a, g(a, g(z0, g(b, g(b, z1))))), G(a, g(z0, g(b, g(b, z1)))), G(z0, g(b, g(b, z1))), G(b, g(b, z1)), G(b, z1))
H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

G, H, F

Compound Symbols:

c3, c4, c5, c6, c7, c8

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(a, g(z0, g(b, g(a, g(z0, z1))))) → c3(G(a, g(a, g(a, g(z0, g(b, g(b, z1)))))), G(a, g(a, g(z0, g(b, g(b, z1))))), G(a, g(z0, g(b, g(b, z1)))), G(z0, g(b, g(b, z1))), G(b, g(b, z1)), G(b, z1)) by

G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
G(a, g(x0, g(b, g(a, g(x0, x1))))) → c3

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
G(a, g(x0, g(b, g(a, g(x0, x1))))) → c3

S tuples:

H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
G(a, g(x0, g(b, g(a, g(x0, x1))))) → c3

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

H, F, G

Compound Symbols:

c4, c5, c6, c7, c8, c3, c3

(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

G(a, g(x0, g(b, g(a, g(x0, x1))))) → c3

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))

S tuples:

H(s(f(z0))) → c4(H(f(z0)), F(z0))
H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

H, F, G

Compound Symbols:

c4, c5, c6, c7, c8, c3

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace H(s(f(z0))) → c4(H(f(z0)), F(z0)) by

H(s(f(x0))) → c4(F(x0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))

S tuples:

H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1))
H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

H, F, G

Compound Symbols:

c5, c6, c7, c8, c3, c4

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace H(g(z0, s(z1))) → c5(H(g(s(z0), z1)), G(s(z0), z1)) by

H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))

S tuples:

H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1))
F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

H, F, G

Compound Symbols:

c6, c7, c8, c3, c4, c5

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace H(i(z0, z1)) → c6(I(i(c, h(h(z1))), z0), I(c, h(h(z1))), H(h(z1)), H(z1)) by

H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
H(i(x0, x1)) → c6

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
H(i(x0, x1)) → c6

S tuples:

F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
H(i(x0, x1)) → c6

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

F, G, H

Compound Symbols:

c7, c8, c3, c4, c5, c6, c6

(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

H(i(x0, x1)) → c6

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))

S tuples:

F(s(z0)) → c7(F(h(s(z0))), H(s(z0)))
F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

F, G, H

Compound Symbols:

c7, c8, c3, c4, c5, c6

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(s(z0)) → c7(F(h(s(z0))), H(s(z0))) by

F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))
F(s(x0)) → c7

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))
F(s(x0)) → c7

S tuples:

F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))
F(s(x0)) → c7

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

F, G, H

Compound Symbols:

c8, c3, c4, c5, c6, c7, c7

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(s(x0)) → c7

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))

S tuples:

F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1)))
G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

F, G, H

Compound Symbols:

c8, c3, c4, c5, c6, c7

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(g(s(z0), z1)) → c8(F(g(z0, s(z1))), G(z0, s(z1))) by

F(g(s(x0), x1)) → c8(F(g(x0, s(x1))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))
F(g(s(x0), x1)) → c8(F(g(x0, s(x1))))

S tuples:

G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))
F(g(s(x0), x1)) → c8(F(g(x0, s(x1))))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

G, H, F

Compound Symbols:

c3, c4, c5, c6, c7, c8

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace G(a, g(g(b, g(b, x1)), g(b, g(a, g(g(b, g(b, x1)), x1))))) → c3(G(a, g(a, g(a, g(a, b)))), G(a, g(a, g(g(b, g(b, x1)), g(b, g(b, x1))))), G(a, g(g(b, g(b, x1)), g(b, g(b, x1)))), G(g(b, g(b, x1)), g(b, g(b, x1))), G(b, g(b, x1)), G(b, x1)) by

G(a, g(g(b, g(b, x0)), g(b, g(a, g(g(b, g(b, x0)), x0))))) → c3(G(a, g(a, g(g(b, g(b, x0)), g(b, g(b, x0))))), G(a, g(g(b, g(b, x0)), g(b, g(b, x0)))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

i(z0, z0) → i(a, b)
g(z0, z0) → g(a, b)
g(a, g(z0, g(b, g(a, g(z0, z1))))) → g(a, g(a, g(a, g(z0, g(b, g(b, z1))))))
h(s(f(z0))) → h(f(z0))
h(g(z0, s(z1))) → h(g(s(z0), z1))
h(i(z0, z1)) → i(i(c, h(h(z1))), z0)
f(s(z0)) → s(s(f(h(s(z0)))))
f(g(s(z0), z1)) → f(g(z0, s(z1)))

Tuples:

G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))
F(g(s(x0), x1)) → c8(F(g(x0, s(x1))))
G(a, g(g(b, g(b, x0)), g(b, g(a, g(g(b, g(b, x0)), x0))))) → c3(G(a, g(a, g(g(b, g(b, x0)), g(b, g(b, x0))))), G(a, g(g(b, g(b, x0)), g(b, g(b, x0)))))

S tuples:

G(a, g(a, g(b, g(a, g(a, g(a, g(b, z1))))))) → c3(G(a, g(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, z1))))))))), G(a, g(a, g(a, g(b, g(b, g(a, g(b, z1))))))), G(a, g(a, g(b, g(b, g(a, g(b, z1)))))), G(a, g(b, g(b, g(a, g(b, z1))))), G(b, g(b, g(a, g(b, z1)))), G(b, g(a, g(b, z1))))
G(a, g(x0, g(b, g(a, g(x0, b))))) → c3(G(a, g(a, g(a, g(x0, g(b, g(a, b)))))), G(a, g(a, g(x0, g(b, g(b, b))))), G(a, g(x0, g(b, g(b, b)))), G(x0, g(b, g(b, b))), G(b, g(b, b)), G(b, b))
H(s(f(x0))) → c4(F(x0))
H(g(x0, s(x1))) → c5(H(g(s(x0), x1)))
H(i(x0, s(f(z0)))) → c6(I(i(c, h(h(f(z0)))), x0), I(c, h(h(s(f(z0))))), H(h(s(f(z0)))), H(s(f(z0))))
H(i(x0, g(z0, s(z1)))) → c6(I(i(c, h(h(g(s(z0), z1)))), x0), I(c, h(h(g(z0, s(z1))))), H(h(g(z0, s(z1)))), H(g(z0, s(z1))))
H(i(x0, i(z0, z1))) → c6(I(i(c, h(i(i(c, h(h(z1))), z0))), x0), I(c, h(h(i(z0, z1)))), H(h(i(z0, z1))), H(i(z0, z1)))
F(s(f(z0))) → c7(F(h(f(z0))), H(s(f(z0))))
F(g(s(x0), x1)) → c8(F(g(x0, s(x1))))
G(a, g(g(b, g(b, x0)), g(b, g(a, g(g(b, g(b, x0)), x0))))) → c3(G(a, g(a, g(g(b, g(b, x0)), g(b, g(b, x0))))), G(a, g(g(b, g(b, x0)), g(b, g(b, x0)))))

K tuples:none
Defined Rule Symbols:

i, g, h, f

Defined Pair Symbols:

G, H, F

Compound Symbols:

c3, c4, c5, c6, c7, c8, c3

(25) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 4]
transitions:
c0() → 0
i0(0, 0) → 1
g0(0, 0) → 2
h0(0) → 3
f0(0) → 4
a1() → 5
b1() → 6
i1(5, 6) → 1
a1() → 0
b1() → 0
a1() → 7
b1() → 8
g1(7, 8) → 2
s1(0) → 12
h1(12) → 11
f1(11) → 10
s1(10) → 9
s1(9) → 4
s1(0) → 0
a1() → 13
b1() → 14
s1(0) → 15
i0(13, 0) → 1
i0(0, 13) → 1
i0(14, 0) → 1
i0(0, 14) → 1
i0(15, 0) → 1
i0(0, 15) → 1
i0(13, 13) → 1
i0(13, 14) → 1
i0(13, 15) → 1
i0(14, 13) → 1
i0(15, 13) → 1
i0(14, 14) → 1
i0(14, 15) → 1
i0(15, 14) → 1
i0(15, 15) → 1
g0(13, 0) → 2
g0(0, 13) → 2
g0(14, 0) → 2
g0(0, 14) → 2
g0(15, 0) → 2
g0(0, 15) → 2
g0(13, 13) → 2
g0(13, 14) → 2
g0(13, 15) → 2
g0(14, 13) → 2
g0(15, 13) → 2
g0(14, 14) → 2
g0(14, 15) → 2
g0(15, 14) → 2
g0(15, 15) → 2
h0(13) → 3
h0(14) → 3
h0(15) → 3
f0(13) → 4
f0(14) → 4
f0(15) → 4
i1(13, 6) → 1
i1(5, 14) → 1
i1(13, 14) → 1
g1(13, 8) → 2
g1(7, 14) → 2
g1(13, 14) → 2
s1(13) → 15
s1(14) → 15
s1(15) → 15
h1(15) → 11
h1(15) → 3

(26) BOUNDS(O(1), O(n^1))