(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
g(x, x, x) → g(c, d, e)
g(x, y, x) → g(c, d, e)
s(f(x, y)) → f(y, f(s(s(x)), a))
h(h(x, a), y) → h(h(a, y), h(a, x))
f(x, f(y, f(x, y))) → f(a, f(x, f(y, b)))
f(h(a, y), g(x, b, a)) → h(f(x, s(y)), s(b))
h(f(x, s(y)), b) → f(a, g(y, a, f(s(x), a)))
f(x, g(x, a, f(s(x), y))) → f(h(x, b), g(a, b, y))
s(y) → b
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))
Tuples:
G(z0, z0, z0) → c1(G(c, d, e))
G(z0, z1, z0) → c2(G(c, d, e))
S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
H(f(z0, s(z1)), b) → c6(F(a, g(z1, a, f(s(z0), a))), G(z1, a, f(s(z0), a)), F(s(z0), a), S(z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
F(z0, g(z0, a, f(s(z0), z1))) → c9(F(h(z0, b), g(a, b, z1)), H(z0, b), G(a, b, z1))
S tuples:
G(z0, z0, z0) → c1(G(c, d, e))
G(z0, z1, z0) → c2(G(c, d, e))
S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
H(f(z0, s(z1)), b) → c6(F(a, g(z1, a, f(s(z0), a))), G(z1, a, f(s(z0), a)), F(s(z0), a), S(z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
F(z0, g(z0, a, f(s(z0), z1))) → c9(F(h(z0, b), g(a, b, z1)), H(z0, b), G(a, b, z1))
K tuples:none
Defined Rule Symbols:
g, s, h, f
Defined Pair Symbols:
G, S, H, F
Compound Symbols:
c1, c2, c3, c5, c6, c7, c8, c9
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
S(f(z0, z1)) → c3(F(z1, f(s(s(z0)), a)), F(s(s(z0)), a), S(s(z0)), S(z0))
H(h(z0, a), z1) → c5(H(h(a, z1), h(a, z0)), H(a, z1), H(a, z0))
H(f(z0, s(z1)), b) → c6(F(a, g(z1, a, f(s(z0), a))), G(z1, a, f(s(z0), a)), F(s(z0), a), S(z0))
F(z0, f(z1, f(z0, z1))) → c7(F(a, f(z0, f(z1, b))), F(z0, f(z1, b)), F(z1, b))
F(h(a, z0), g(z1, b, a)) → c8(H(f(z1, s(z0)), s(b)), F(z1, s(z0)), S(z0), S(b))
F(z0, g(z0, a, f(s(z0), z1))) → c9(F(h(z0, b), g(a, b, z1)), H(z0, b), G(a, b, z1))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))
Tuples:
G(z0, z0, z0) → c1(G(c, d, e))
G(z0, z1, z0) → c2(G(c, d, e))
S tuples:
G(z0, z0, z0) → c1(G(c, d, e))
G(z0, z1, z0) → c2(G(c, d, e))
K tuples:none
Defined Rule Symbols:
g, s, h, f
Defined Pair Symbols:
G
Compound Symbols:
c1, c2
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
G(z0, z1, z0) → c2(G(c, d, e))
G(z0, z0, z0) → c1(G(c, d, e))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0, z0, z0) → g(c, d, e)
g(z0, z1, z0) → g(c, d, e)
s(f(z0, z1)) → f(z1, f(s(s(z0)), a))
s(z0) → b
h(h(z0, a), z1) → h(h(a, z1), h(a, z0))
h(f(z0, s(z1)), b) → f(a, g(z1, a, f(s(z0), a)))
f(z0, f(z1, f(z0, z1))) → f(a, f(z0, f(z1, b)))
f(h(a, z0), g(z1, b, a)) → h(f(z1, s(z0)), s(b))
f(z0, g(z0, a, f(s(z0), z1))) → f(h(z0, b), g(a, b, z1))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
g, s, h, f
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))