YES(O(1), O(n^1)) 6.65/2.34 YES(O(1), O(n^1)) 6.65/2.39 6.65/2.39 6.65/2.39 6.65/2.39 6.65/2.39 6.65/2.39 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 6.65/2.39 6.65/2.39 6.65/2.39
6.65/2.39
6.65/2.39
6.65/2.39
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
6.65/2.39 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳2 CdtProblem
6.65/2.39 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳4 CdtProblem
6.65/2.39 
↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳6 CdtProblem
6.65/2.39 
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳8 CdtProblem
6.65/2.39 
↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳10 CdtProblem
6.65/2.39 
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
6.65/2.39 
↳12 CdtProblem
6.65/2.39 
↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳14 CdtProblem
6.65/2.39 
↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳16 CdtProblem
6.65/2.39 
↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳18 CdtProblem
6.65/2.39 
↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
6.65/2.39 
↳20 CdtProblem
6.65/2.39 
↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳22 CdtProblem
6.65/2.39 
↳23 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳24 CdtProblem
6.65/2.39 
↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳26 CdtProblem
6.65/2.39 
↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳28 CdtProblem
6.65/2.39 
↳29 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳30 CdtProblem
6.65/2.39 
↳31 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳32 CdtProblem
6.65/2.39 
↳33 SIsEmptyProof (BOTH BOUNDS(ID, ID))
6.65/2.39 
↳34 BOUNDS(O(1), O(1))
6.65/2.39
6.65/2.39 6.65/2.39
6.65/2.39
6.65/2.39

(0) Obligation:

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

f(0, 1, x) → f(h(x), h(x), x) 6.65/2.39
h(0) → 0 6.65/2.39
h(g(x, y)) → y

Rewrite Strategy: INNERMOST
6.65/2.39
6.65/2.39

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

Converted CpxTRS to CDT
6.65/2.39
6.65/2.39

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.39
h(0) → 0 6.65/2.39
h(g(z0, z1)) → z1
Tuples:

F(0, 1, z0) → c(F(h(z0), h(z0), z0), H(z0), H(z0))
S tuples:

F(0, 1, z0) → c(F(h(z0), h(z0), z0), H(z0), H(z0))
K tuples:none
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c

6.65/2.39
6.65/2.39

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

Removed 2 trailing tuple parts
6.65/2.39
6.65/2.39

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.39
h(0) → 0 6.65/2.39
h(g(z0, z1)) → z1
Tuples:

F(0, 1, z0) → c(F(h(z0), h(z0), z0))
S tuples:

F(0, 1, z0) → c(F(h(z0), h(z0), z0))
K tuples:none
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c

6.65/2.39
6.65/2.39

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

Use narrowing to replace F(0, 1, z0) → c(F(h(z0), h(z0), z0)) by

F(0, 1, 0) → c(F(h(0), 0, 0)) 6.65/2.39
F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.39
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.39
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1)))
6.65/2.39
6.65/2.39

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.39
h(0) → 0 6.65/2.39
h(g(z0, z1)) → z1
Tuples:

F(0, 1, 0) → c(F(h(0), 0, 0)) 6.65/2.39
F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.39
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.39
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1)))
S tuples:

F(0, 1, 0) → c(F(h(0), 0, 0)) 6.65/2.39
F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.39
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.39
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1)))
K tuples:none
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c

6.65/2.40
6.65/2.40

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

Removed 1 trailing tuple parts
6.65/2.40
6.65/2.40

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.40
h(0) → 0 6.65/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c
S tuples:

F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c
K tuples:none
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.65/2.40
6.65/2.40

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(0, 1, 0) → c
6.65/2.40
6.65/2.40

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.40
h(0) → 0 6.65/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c
S tuples:

F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c
K tuples:none
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.65/2.40
6.65/2.40

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(0, 1, 0) → c
We considered the (Usable) Rules:

h(g(z0, z1)) → z1 6.65/2.40
h(0) → 0
And the Tuples:

F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c
The order we found is given by the following interpretation:
Polynomial interpretation : 6.65/2.40

POL(0) = 0    6.65/2.40
POL(1) = 0    6.65/2.40
POL(F(x1, x2, x3)) = [5] + [5]x3    6.65/2.40
POL(c) = 0    6.65/2.40
POL(c(x1)) = x1    6.65/2.40
POL(g(x1, x2)) = x2    6.65/2.40
POL(h(x1)) = x1   
6.65/2.40
6.65/2.40

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.40
h(0) → 0 6.65/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c
S tuples:

F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1)))
K tuples:

F(0, 1, 0) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.65/2.40
6.65/2.40

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(0, 1, g(z0, z1)) → c(F(h(g(z0, z1)), z1, g(z0, z1))) by

F(0, 1, g(z0, z1)) → c(F(z1, z1, g(z0, z1)))
6.65/2.40
6.65/2.40

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.40
h(0) → 0 6.65/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, z1, g(z0, z1)))
S tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, z1, g(z0, z1)))
K tuples:

F(0, 1, 0) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.65/2.40
6.65/2.40

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

Removed 1 trailing tuple parts
6.65/2.40
6.65/2.40

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.40
h(0) → 0 6.65/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c 6.65/2.40
F(0, 1, g(z0, z1)) → c
S tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, g(z0, z1)) → c
K tuples:

F(0, 1, 0) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.65/2.40
6.65/2.40

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

F(0, 1, g(z0, z1)) → c 6.65/2.40
F(0, 1, 0) → c
6.65/2.40
6.65/2.40

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.65/2.40
h(0) → 0 6.65/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c 6.65/2.40
F(0, 1, g(z0, z1)) → c
S tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, g(z0, z1)) → c
K tuples:

F(0, 1, 0) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.65/2.40
6.65/2.40

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(0, 1, g(z0, z1)) → c
We considered the (Usable) Rules:

h(g(z0, z1)) → z1 6.65/2.40
h(0) → 0
And the Tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.65/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.65/2.40
F(0, 1, 0) → c 6.65/2.40
F(0, 1, g(z0, z1)) → c
The order we found is given by the following interpretation:
Polynomial interpretation : 6.65/2.40

POL(0) = [2]    6.98/2.40
POL(1) = [1]    6.98/2.40
POL(F(x1, x2, x3)) = x3    6.98/2.40
POL(c) = 0    6.98/2.40
POL(c(x1)) = x1    6.98/2.40
POL(g(x1, x2)) = [2] + x1 + x2    6.98/2.40
POL(h(x1)) = [4] + [4]x1   
6.98/2.40
6.98/2.40

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.98/2.40
h(0) → 0 6.98/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.98/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.98/2.40
F(0, 1, 0) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c
S tuples:

F(0, 1, 0) → c(F(0, h(0), 0)) 6.98/2.40
F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1)))
K tuples:

F(0, 1, 0) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.98/2.40
6.98/2.40

(21) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(0, 1, 0) → c(F(0, h(0), 0)) by

F(0, 1, 0) → c(F(0, 0, 0))
6.98/2.40
6.98/2.40

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.98/2.40
h(0) → 0 6.98/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.98/2.40
F(0, 1, 0) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c 6.98/2.40
F(0, 1, 0) → c(F(0, 0, 0))
S tuples:

F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.98/2.40
F(0, 1, 0) → c(F(0, 0, 0))
K tuples:

F(0, 1, 0) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.98/2.40
6.98/2.40

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

Removed 1 trailing tuple parts
6.98/2.40
6.98/2.40

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.98/2.40
h(0) → 0 6.98/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.98/2.40
F(0, 1, 0) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c
S tuples:

F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.98/2.40
F(0, 1, 0) → c
K tuples:

F(0, 1, 0) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.98/2.40
6.98/2.40

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

F(0, 1, 0) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c
6.98/2.40
6.98/2.40

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.98/2.40
h(0) → 0 6.98/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) 6.98/2.40
F(0, 1, g(z0, z1)) → c
S tuples:

F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1)))
K tuples:

F(0, 1, g(z0, z1)) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.98/2.40
6.98/2.40

(27) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(0, 1, g(z0, z1)) → c(F(z1, h(g(z0, z1)), g(z0, z1))) by

F(0, 1, g(z0, z1)) → c(F(z1, z1, g(z0, z1)))
6.98/2.40
6.98/2.40

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.98/2.40
h(0) → 0 6.98/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c 6.98/2.40
F(0, 1, g(z0, z1)) → c(F(z1, z1, g(z0, z1)))
S tuples:

F(0, 1, g(z0, z1)) → c(F(z1, z1, g(z0, z1)))
K tuples:

F(0, 1, g(z0, z1)) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c, c

6.98/2.40
6.98/2.40

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

Removed 1 trailing tuple parts
6.98/2.40
6.98/2.40

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.98/2.40
h(0) → 0 6.98/2.40
h(g(z0, z1)) → z1
Tuples:

F(0, 1, g(z0, z1)) → c
S tuples:

F(0, 1, g(z0, z1)) → c
K tuples:

F(0, 1, g(z0, z1)) → c
Defined Rule Symbols:

f, h

Defined Pair Symbols:

F

Compound Symbols:

c

6.98/2.40
6.98/2.40

(31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(0, 1, g(z0, z1)) → c
6.98/2.40
6.98/2.40

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(0, 1, z0) → f(h(z0), h(z0), z0) 6.98/2.40
h(0) → 0 6.98/2.40
h(g(z0, z1)) → z1
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

f, h

Defined Pair Symbols:none

Compound Symbols:none

6.98/2.40
6.98/2.40

(33) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
6.98/2.40
6.98/2.40

(34) BOUNDS(O(1), O(1))

6.98/2.40
6.98/2.40
6.98/2.47 EOF