(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
g(x, x) → g(a, b)
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))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0, z0) → g(a, b)
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))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(z0, z0) → c1(G(a, b))
G(c, g(c, z0)) → c2(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
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(z0, z0) → c1(G(a, b))
G(c, g(c, z0)) → c2(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
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)) → c2(G(e, g(d, z0)), G(d, z0))
G(d, g(d, z0)) → c3(G(c, g(e, z0)), G(e, z0))
G(e, g(e, z0)) → c4(G(d, g(c, z0)), G(c, z0))
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(z0, z0) → g(a, b)
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))
f(g(z0, z1)) → g(z1, g(f(f(z0)), a))
Tuples:
G(z0, z0) → c1(G(a, b))
S tuples:
G(z0, z0) → c1(G(a, b))
K tuples:none
Defined Rule Symbols:
g, f
Defined Pair Symbols:
G
Compound Symbols:
c1
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
G(z0, z0) → c1(G(a, b))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0, z0) → g(a, b)
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))
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
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))