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

0 CpxTRS
3.81/1.44 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
3.81/1.44 
↳2 CdtProblem
3.81/1.44 
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
3.81/1.44 
↳4 CdtProblem
3.81/1.44 
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
3.81/1.44 
↳6 CdtProblem
3.81/1.44 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))
3.81/1.44 
↳8 CdtProblem
3.81/1.44 
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))
3.81/1.44 
↳10 BOUNDS(O(1), O(1))
3.81/1.44
3.81/1.44 3.81/1.44
3.81/1.44
3.81/1.44

(0) Obligation:

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

app(nil, y) → y 3.81/1.44
app(add(n, x), y) → add(n, app(x, y)) 3.81/1.44
reverse(nil) → nil 3.81/1.44
reverse(add(n, x)) → app(reverse(x), add(n, nil)) 3.81/1.44
shuffle(nil) → nil 3.81/1.44
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))

Rewrite Strategy: INNERMOST
3.81/1.44
3.81/1.44

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

Converted CpxTRS to CDT
3.81/1.44
3.81/1.44

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0 3.81/1.44
app(add(z0, z1), z2) → add(z0, app(z1, z2)) 3.81/1.44
reverse(nil) → nil 3.81/1.44
reverse(add(z0, z1)) → app(reverse(z1), add(z0, nil)) 3.81/1.44
shuffle(nil) → nil 3.81/1.44
shuffle(add(z0, z1)) → add(z0, shuffle(reverse(z1)))
Tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
S tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
K tuples:none
Defined Rule Symbols:

app, reverse, shuffle

Defined Pair Symbols:

APP, REVERSE, SHUFFLE

Compound Symbols:

c1, c3, c5

3.81/1.44
3.81/1.44

(3) 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(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
We considered the (Usable) Rules:

reverse(nil) → nil 3.81/1.44
reverse(add(z0, z1)) → app(reverse(z1), add(z0, nil)) 3.81/1.44
app(nil, z0) → z0 3.81/1.44
app(add(z0, z1), z2) → add(z0, app(z1, z2))
And the Tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 3.81/1.44

POL(APP(x1, x2)) = 0    3.81/1.44
POL(REVERSE(x1)) = 0    3.81/1.44
POL(SHUFFLE(x1)) = [2]x1    3.81/1.44
POL(add(x1, x2)) = [4] + x1 + x2    3.81/1.44
POL(app(x1, x2)) = x1 + x2    3.81/1.44
POL(c1(x1)) = x1    3.81/1.44
POL(c3(x1, x2)) = x1 + x2    3.81/1.44
POL(c5(x1, x2)) = x1 + x2    3.81/1.44
POL(nil) = 0    3.81/1.44
POL(reverse(x1)) = x1   
3.81/1.44
3.81/1.44

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0 3.81/1.44
app(add(z0, z1), z2) → add(z0, app(z1, z2)) 3.81/1.44
reverse(nil) → nil 3.81/1.44
reverse(add(z0, z1)) → app(reverse(z1), add(z0, nil)) 3.81/1.44
shuffle(nil) → nil 3.81/1.44
shuffle(add(z0, z1)) → add(z0, shuffle(reverse(z1)))
Tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
S tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1))
K tuples:

SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
Defined Rule Symbols:

app, reverse, shuffle

Defined Pair Symbols:

APP, REVERSE, SHUFFLE

Compound Symbols:

c1, c3, c5

3.81/1.44
3.81/1.44

(5) 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(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1))
We considered the (Usable) Rules:

reverse(nil) → nil 3.81/1.44
reverse(add(z0, z1)) → app(reverse(z1), add(z0, nil)) 3.81/1.44
app(nil, z0) → z0 3.81/1.44
app(add(z0, z1), z2) → add(z0, app(z1, z2))
And the Tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 3.81/1.44

POL(APP(x1, x2)) = [1]    3.81/1.44
POL(REVERSE(x1)) = [2]x1    3.81/1.44
POL(SHUFFLE(x1)) = x12    3.81/1.44
POL(add(x1, x2)) = [2] + x2    3.81/1.44
POL(app(x1, x2)) = x1 + x2    3.81/1.44
POL(c1(x1)) = x1    3.81/1.44
POL(c3(x1, x2)) = x1 + x2    3.81/1.44
POL(c5(x1, x2)) = x1 + x2    3.81/1.44
POL(nil) = 0    3.81/1.44
POL(reverse(x1)) = x1   
3.81/1.44
3.81/1.44

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0 3.81/1.44
app(add(z0, z1), z2) → add(z0, app(z1, z2)) 3.81/1.44
reverse(nil) → nil 3.81/1.44
reverse(add(z0, z1)) → app(reverse(z1), add(z0, nil)) 3.81/1.44
shuffle(nil) → nil 3.81/1.44
shuffle(add(z0, z1)) → add(z0, shuffle(reverse(z1)))
Tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
S tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2))
K tuples:

SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1))
Defined Rule Symbols:

app, reverse, shuffle

Defined Pair Symbols:

APP, REVERSE, SHUFFLE

Compound Symbols:

c1, c3, c5

3.81/1.44
3.81/1.44

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

APP(add(z0, z1), z2) → c1(APP(z1, z2))
We considered the (Usable) Rules:

reverse(nil) → nil 3.81/1.44
reverse(add(z0, z1)) → app(reverse(z1), add(z0, nil)) 3.81/1.44
app(nil, z0) → z0 3.81/1.44
app(add(z0, z1), z2) → add(z0, app(z1, z2))
And the Tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
The order we found is given by the following interpretation:
Polynomial interpretation : 3.81/1.44

POL(APP(x1, x2)) = x1 + x1·x2    3.81/1.44
POL(REVERSE(x1)) = x12    3.81/1.44
POL(SHUFFLE(x1)) = x13    3.81/1.44
POL(add(x1, x2)) = [1] + x2    3.81/1.44
POL(app(x1, x2)) = x1 + x2    3.81/1.44
POL(c1(x1)) = x1    3.81/1.44
POL(c3(x1, x2)) = x1 + x2    3.81/1.44
POL(c5(x1, x2)) = x1 + x2    3.81/1.44
POL(nil) = 0    3.81/1.44
POL(reverse(x1)) = x1   
3.81/1.44
3.81/1.44

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

app(nil, z0) → z0 3.81/1.44
app(add(z0, z1), z2) → add(z0, app(z1, z2)) 3.81/1.44
reverse(nil) → nil 3.81/1.44
reverse(add(z0, z1)) → app(reverse(z1), add(z0, nil)) 3.81/1.44
shuffle(nil) → nil 3.81/1.44
shuffle(add(z0, z1)) → add(z0, shuffle(reverse(z1)))
Tuples:

APP(add(z0, z1), z2) → c1(APP(z1, z2)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1))
S tuples:none
K tuples:

SHUFFLE(add(z0, z1)) → c5(SHUFFLE(reverse(z1)), REVERSE(z1)) 3.81/1.44
REVERSE(add(z0, z1)) → c3(APP(reverse(z1), add(z0, nil)), REVERSE(z1)) 3.81/1.44
APP(add(z0, z1), z2) → c1(APP(z1, z2))
Defined Rule Symbols:

app, reverse, shuffle

Defined Pair Symbols:

APP, REVERSE, SHUFFLE

Compound Symbols:

c1, c3, c5

3.81/1.44
3.81/1.44

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

The set S is empty
3.81/1.44
3.81/1.44

(10) BOUNDS(O(1), O(1))

3.81/1.44
3.81/1.44
3.81/1.49 EOF