39.62/35.83
39.62/35.83
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(b(x)) → b(b(a(a(x))))
Rewrite Strategy: INNERMOST
39.62/35.83
39.62/35.83
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
39.62/35.83
39.62/35.83
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(b(z0)) → b(b(a(a(z0))))
Tuples:
A(b(z0)) → c(A(a(z0)), A(z0))
S tuples:
A(b(z0)) → c(A(a(z0)), A(z0))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c
39.62/35.83
39.62/35.83
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
b(
z0)) →
c(
A(
a(
z0)),
A(
z0)) by
A(b(b(z0))) → c(A(b(b(a(a(z0))))), A(b(z0)))
39.62/35.83
39.62/35.83
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(b(z0)) → b(b(a(a(z0))))
Tuples:
A(b(b(z0))) → c(A(b(b(a(a(z0))))), A(b(z0)))
S tuples:
A(b(b(z0))) → c(A(b(b(a(a(z0))))), A(b(z0)))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c
39.62/35.83