0.00/0.56
0.00/0.56
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
g(X) → u(h(X), h(X), X)
0.00/0.56
u(d, c(Y), X) → k(Y)
0.00/0.56
h(d) → c(a)
0.00/0.56
h(d) → c(b)
0.00/0.56
f(k(a), k(b), X) → f(X, X, X)
Rewrite Strategy: INNERMOST
0.00/0.56
0.00/0.56
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
0.00/0.56
0.00/0.56
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0) → u(h(z0), h(z0), z0)
0.00/0.56
u(d, c(z0), z1) → k(z0)
0.00/0.56
h(d) → c(a)
0.00/0.56
h(d) → c(b)
0.00/0.56
f(k(a), k(b), z0) → f(z0, z0, z0)
Tuples:
G(z0) → c1(U(h(z0), h(z0), z0), H(z0), H(z0))
0.00/0.56
F(k(a), k(b), z0) → c5(F(z0, z0, z0))
S tuples:
G(z0) → c1(U(h(z0), h(z0), z0), H(z0), H(z0))
0.00/0.56
F(k(a), k(b), z0) → c5(F(z0, z0, z0))
K tuples:none
Defined Rule Symbols:
g, u, h, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c5
0.00/0.56
0.00/0.56
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
0.00/0.56
0.00/0.56
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0) → u(h(z0), h(z0), z0)
0.00/0.56
u(d, c(z0), z1) → k(z0)
0.00/0.56
h(d) → c(a)
0.00/0.56
h(d) → c(b)
0.00/0.56
f(k(a), k(b), z0) → f(z0, z0, z0)
Tuples:
G(z0) → c1
0.00/0.56
F(k(a), k(b), z0) → c5
S tuples:
G(z0) → c1
0.00/0.56
F(k(a), k(b), z0) → c5
K tuples:none
Defined Rule Symbols:
g, u, h, f
Defined Pair Symbols:
G, F
Compound Symbols:
c1, c5
0.00/0.56
0.00/0.56
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
G(z0) → c1
0.00/0.56
F(k(a), k(b), z0) → c5
0.00/0.56
0.00/0.56
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(z0) → u(h(z0), h(z0), z0)
0.00/0.56
u(d, c(z0), z1) → k(z0)
0.00/0.56
h(d) → c(a)
0.00/0.56
h(d) → c(b)
0.00/0.56
f(k(a), k(b), z0) → f(z0, z0, z0)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
g, u, h, f
Defined Pair Symbols:none
Compound Symbols:none
0.00/0.56
0.00/0.56
(7) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
0.00/0.56
0.00/0.56
(8) BOUNDS(O(1), O(1))
0.00/0.56