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