MAYBE 39.62/35.82 MAYBE 39.62/35.83 39.62/35.83 39.62/35.83 39.62/35.83 39.62/35.83 39.62/35.83 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 39.62/35.83 39.62/35.83 39.62/35.83
39.62/35.83 39.62/35.83 39.62/35.83
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
39.62/35.83
39.62/35.86 EOF