MAYBE 3.19/1.93 MAYBE 3.19/1.94 3.19/1.94 3.19/1.94 3.19/1.94 3.19/1.94 3.19/1.94 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 3.19/1.94 3.19/1.94 3.19/1.94
3.19/1.94
3.19/1.94
3.19/1.94
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
3.19/1.94 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
3.19/1.94 
↳2 CdtProblem
3.19/1.94 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
3.19/1.94 
↳4 CdtProblem
3.19/1.94 
↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
3.19/1.94 
↳6 CdtProblem
3.19/1.94 
↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))
3.19/1.94 
↳8 CdtProblem
3.19/1.94
3.19/1.94 3.19/1.94
3.19/1.94
3.19/1.94

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(g(x)) → f(a(g(g(f(x))), g(f(x))))

Rewrite Strategy: INNERMOST
3.19/1.94
3.19/1.94

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
3.19/1.94
3.19/1.94

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(g(z0)) → f(a(g(g(f(z0))), g(f(z0))))
Tuples:

F(g(z0)) → c(F(a(g(g(f(z0))), g(f(z0)))), F(z0), F(z0))
S tuples:

F(g(z0)) → c(F(a(g(g(f(z0))), g(f(z0)))), F(z0), F(z0))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c

3.19/1.94
3.19/1.94

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts
3.19/1.94
3.19/1.94

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(g(z0)) → f(a(g(g(f(z0))), g(f(z0))))
Tuples:

F(g(z0)) → c(F(z0), F(z0))
S tuples:

F(g(z0)) → c(F(z0), F(z0))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c

3.19/1.94
3.19/1.94

(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(g(z0)) → c(F(z0), F(z0)) by

F(g(g(y0))) → c(F(g(y0)), F(g(y0)))
3.19/1.94
3.19/1.94

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(g(z0)) → f(a(g(g(f(z0))), g(f(z0))))
Tuples:

F(g(g(y0))) → c(F(g(y0)), F(g(y0)))
S tuples:

F(g(g(y0))) → c(F(g(y0)), F(g(y0)))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c

3.19/1.94
3.19/1.94

(7) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(g(g(y0))) → c(F(g(y0)), F(g(y0))) by

F(g(g(g(y0)))) → c(F(g(g(y0))), F(g(g(y0))))
3.19/1.94
3.19/1.94

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(g(z0)) → f(a(g(g(f(z0))), g(f(z0))))
Tuples:

F(g(g(g(y0)))) → c(F(g(g(y0))), F(g(g(y0))))
S tuples:

F(g(g(g(y0)))) → c(F(g(g(y0))), F(g(g(y0))))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c

3.19/1.94
3.19/1.94
3.19/1.96 EOF