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

0 CpxTRS
3.46/1.40 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
3.46/1.40 
↳2 CdtProblem
3.46/1.40 
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)
3.46/1.40 
↳4 CdtProblem
3.46/1.40 
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
3.46/1.40 
↳6 CdtProblem
3.46/1.40 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
3.46/1.40 
↳8 CdtProblem
3.46/1.40 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))
3.46/1.40 
↳10 CdtProblem
3.46/1.40 
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))
3.46/1.40 
↳12 BOUNDS(O(1), O(1))
3.46/1.40
3.46/1.40 3.46/1.40
3.46/1.40
3.46/1.40

(0) Obligation:

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

shuffle(Cons(x, xs)) → Cons(x, shuffle(reverse(xs))) 3.46/1.40
reverse(Cons(x, xs)) → append(reverse(xs), Cons(x, Nil)) 3.46/1.40
append(Cons(x, xs), ys) → Cons(x, append(xs, ys)) 3.46/1.40
shuffle(Nil) → Nil 3.46/1.40
reverse(Nil) → Nil 3.46/1.40
append(Nil, ys) → ys 3.46/1.40
goal(xs) → shuffle(xs)

Rewrite Strategy: INNERMOST
3.46/1.40
3.46/1.40

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

Converted CpxTRS to CDT
3.46/1.40
3.46/1.40

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

shuffle(Cons(z0, z1)) → Cons(z0, shuffle(reverse(z1))) 3.46/1.40
shuffle(Nil) → Nil 3.46/1.40
reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.46/1.40
reverse(Nil) → Nil 3.46/1.40
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.46/1.40
append(Nil, z0) → z0 3.46/1.40
goal(z0) → shuffle(z0)
Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.46/1.40
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.46/1.40
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2)) 3.46/1.40
GOAL(z0) → c6(SHUFFLE(z0))
S tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2)) 3.79/1.41
GOAL(z0) → c6(SHUFFLE(z0))
K tuples:none
Defined Rule Symbols:

shuffle, reverse, append, goal

Defined Pair Symbols:

SHUFFLE, REVERSE, APPEND, GOAL

Compound Symbols:

c, c2, c4, c6

3.79/1.41
3.79/1.41

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0) → c6(SHUFFLE(z0))
3.79/1.41
3.79/1.41

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

shuffle(Cons(z0, z1)) → Cons(z0, shuffle(reverse(z1))) 3.79/1.41
shuffle(Nil) → Nil 3.79/1.41
reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.79/1.41
reverse(Nil) → Nil 3.79/1.41
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.79/1.41
append(Nil, z0) → z0 3.79/1.41
goal(z0) → shuffle(z0)
Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
S tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
K tuples:none
Defined Rule Symbols:

shuffle, reverse, append, goal

Defined Pair Symbols:

SHUFFLE, REVERSE, APPEND

Compound Symbols:

c, c2, c4

3.79/1.41
3.79/1.41

(5) 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.

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1))
We considered the (Usable) Rules:

reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.79/1.41
reverse(Nil) → Nil 3.79/1.41
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.79/1.41
append(Nil, z0) → z0
And the Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 3.79/1.41

POL(APPEND(x1, x2)) = 0    3.79/1.41
POL(Cons(x1, x2)) = [1] + x1 + x2    3.79/1.41
POL(Nil) = 0    3.79/1.41
POL(REVERSE(x1)) = 0    3.79/1.41
POL(SHUFFLE(x1)) = x1    3.79/1.41
POL(append(x1, x2)) = x1 + x2    3.79/1.41
POL(c(x1, x2)) = x1 + x2    3.79/1.41
POL(c2(x1, x2)) = x1 + x2    3.79/1.41
POL(c4(x1)) = x1    3.79/1.41
POL(reverse(x1)) = x1   
3.79/1.41
3.79/1.41

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

shuffle(Cons(z0, z1)) → Cons(z0, shuffle(reverse(z1))) 3.79/1.41
shuffle(Nil) → Nil 3.79/1.41
reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.79/1.41
reverse(Nil) → Nil 3.79/1.41
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.79/1.41
append(Nil, z0) → z0 3.79/1.41
goal(z0) → shuffle(z0)
Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
S tuples:

REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
K tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1))
Defined Rule Symbols:

shuffle, reverse, append, goal

Defined Pair Symbols:

SHUFFLE, REVERSE, APPEND

Compound Symbols:

c, c2, c4

3.79/1.41
3.79/1.41

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1))
We considered the (Usable) Rules:

reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.79/1.41
reverse(Nil) → Nil 3.79/1.41
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.79/1.41
append(Nil, z0) → z0
And the Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 3.79/1.41

POL(APPEND(x1, x2)) = [1]    3.79/1.41
POL(Cons(x1, x2)) = [2] + x2    3.79/1.41
POL(Nil) = 0    3.79/1.41
POL(REVERSE(x1)) = [3]x1    3.79/1.41
POL(SHUFFLE(x1)) = x1 + x12    3.79/1.41
POL(append(x1, x2)) = x1 + x2    3.79/1.41
POL(c(x1, x2)) = x1 + x2    3.79/1.41
POL(c2(x1, x2)) = x1 + x2    3.79/1.41
POL(c4(x1)) = x1    3.79/1.41
POL(reverse(x1)) = x1   
3.79/1.41
3.79/1.41

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

shuffle(Cons(z0, z1)) → Cons(z0, shuffle(reverse(z1))) 3.79/1.41
shuffle(Nil) → Nil 3.79/1.41
reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.79/1.41
reverse(Nil) → Nil 3.79/1.41
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.79/1.41
append(Nil, z0) → z0 3.79/1.41
goal(z0) → shuffle(z0)
Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
S tuples:

APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
K tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1))
Defined Rule Symbols:

shuffle, reverse, append, goal

Defined Pair Symbols:

SHUFFLE, REVERSE, APPEND

Compound Symbols:

c, c2, c4

3.79/1.41
3.79/1.41

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))) transformation)

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

APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
We considered the (Usable) Rules:

reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.79/1.41
reverse(Nil) → Nil 3.79/1.41
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.79/1.41
append(Nil, z0) → z0
And the Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation : 3.79/1.41

POL(APPEND(x1, x2)) = x1    3.79/1.41
POL(Cons(x1, x2)) = [1] + x2    3.79/1.41
POL(Nil) = 0    3.79/1.41
POL(REVERSE(x1)) = x12    3.79/1.41
POL(SHUFFLE(x1)) = x13    3.79/1.41
POL(append(x1, x2)) = x1 + x2    3.79/1.41
POL(c(x1, x2)) = x1 + x2    3.79/1.41
POL(c2(x1, x2)) = x1 + x2    3.79/1.41
POL(c4(x1)) = x1    3.79/1.41
POL(reverse(x1)) = x1   
3.79/1.41
3.79/1.41

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

shuffle(Cons(z0, z1)) → Cons(z0, shuffle(reverse(z1))) 3.79/1.41
shuffle(Nil) → Nil 3.79/1.41
reverse(Cons(z0, z1)) → append(reverse(z1), Cons(z0, Nil)) 3.79/1.41
reverse(Nil) → Nil 3.79/1.41
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 3.79/1.41
append(Nil, z0) → z0 3.79/1.41
goal(z0) → shuffle(z0)
Tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
S tuples:none
K tuples:

SHUFFLE(Cons(z0, z1)) → c(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.79/1.41
REVERSE(Cons(z0, z1)) → c2(APPEND(reverse(z1), Cons(z0, Nil)), REVERSE(z1)) 3.79/1.41
APPEND(Cons(z0, z1), z2) → c4(APPEND(z1, z2))
Defined Rule Symbols:

shuffle, reverse, append, goal

Defined Pair Symbols:

SHUFFLE, REVERSE, APPEND

Compound Symbols:

c, c2, c4

3.79/1.41
3.79/1.41

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

The set S is empty
3.79/1.41
3.79/1.41

(12) BOUNDS(O(1), O(1))

3.79/1.41
3.79/1.41
3.91/1.51 EOF