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