YES(O(1), O(n^2)) 6.37/2.02 YES(O(1), O(n^2)) 6.37/2.04 6.37/2.04 6.37/2.04 6.37/2.04 6.37/2.04 6.37/2.04 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 6.37/2.04 6.37/2.04 6.37/2.04
6.37/2.04
6.37/2.04
6.37/2.04
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^2)).

0 CpxRelTRS
6.37/2.04 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
6.37/2.04 
↳2 CdtProblem
6.37/2.04 
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)
6.37/2.04 
↳4 CdtProblem
6.37/2.04 
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
6.37/2.04 
↳6 CdtProblem
6.37/2.04 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))
6.37/2.04 
↳8 CdtProblem
6.37/2.04 
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))
6.37/2.04 
↳10 BOUNDS(O(1), O(1))
6.37/2.04
6.37/2.04 6.37/2.04
6.37/2.04
6.37/2.04

(0) Obligation:

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

isort(Cons(x, xs), r) → isort(xs, insert(x, r)) 6.37/2.04
isort(Nil, r) → Nil 6.37/2.04
insert(S(x), r) → insert[Ite](<(S(x), x), S(x), r) 6.37/2.04
inssort(xs) → isort(xs, Nil)

The (relative) TRS S consists of the following rules:

<(S(x), S(y)) → <(x, y) 6.37/2.04
<(0, S(y)) → True 6.37/2.04
<(x, 0) → False 6.37/2.04
insert[Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) 6.37/2.04
insert[Ite](True, x, r) → Cons(x, r)

Rewrite Strategy: INNERMOST
6.37/2.04
6.37/2.04

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
6.37/2.04
6.37/2.04

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 6.37/2.04
<(0, S(z0)) → True 6.37/2.04
<(z0, 0) → False 6.37/2.04
insert[Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 6.37/2.04
insert[Ite](True, z0, z1) → Cons(z0, z1) 6.37/2.04
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 6.37/2.04
isort(Nil, z0) → Nil 6.37/2.04
insert(S(z0), z1) → insert[Ite](<(S(z0), z0), S(z0), z1) 6.37/2.04
inssort(z0) → isort(z0, Nil)
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 6.37/2.04
INSERT[ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 6.37/2.04
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.04
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0)) 6.37/2.04
INSSORT(z0) → c8(ISORT(z0, Nil))
S tuples:

ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.04
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0)) 6.37/2.04
INSSORT(z0) → c8(ISORT(z0, Nil))
K tuples:none
Defined Rule Symbols:

isort, insert, inssort, <, insert[Ite]

Defined Pair Symbols:

<', INSERT[ITE], ISORT, INSERT, INSSORT

Compound Symbols:

c, c3, c5, c7, c8

6.37/2.04
6.37/2.04

(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

INSSORT(z0) → c8(ISORT(z0, Nil))
6.37/2.04
6.37/2.04

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 6.37/2.04
<(0, S(z0)) → True 6.37/2.04
<(z0, 0) → False 6.37/2.04
insert[Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 6.37/2.04
insert[Ite](True, z0, z1) → Cons(z0, z1) 6.37/2.04
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 6.37/2.04
isort(Nil, z0) → Nil 6.37/2.04
insert(S(z0), z1) → insert[Ite](<(S(z0), z0), S(z0), z1) 6.37/2.04
inssort(z0) → isort(z0, Nil)
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 6.37/2.04
INSERT[ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 6.37/2.04
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.04
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
S tuples:

ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.04
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
K tuples:none
Defined Rule Symbols:

isort, insert, inssort, <, insert[Ite]

Defined Pair Symbols:

<', INSERT[ITE], ISORT, INSERT

Compound Symbols:

c, c3, c5, c7

6.37/2.04
6.37/2.04

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

ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
We considered the (Usable) Rules:

<(S(z0), S(z1)) → <(z0, z1) 6.37/2.04
<(z0, 0) → False 6.37/2.04
<(0, S(z0)) → True 6.37/2.04
insert(S(z0), z1) → insert[Ite](<(S(z0), z0), S(z0), z1) 6.37/2.04
insert[Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 6.37/2.04
insert[Ite](True, z0, z1) → Cons(z0, z1)
And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 6.37/2.04
INSERT[ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 6.37/2.04
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.04
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 6.37/2.04

POL(0) = [2]    6.37/2.04
POL(<(x1, x2)) = [5]x1    6.37/2.04
POL(<'(x1, x2)) = 0    6.37/2.04
POL(Cons(x1, x2)) = [1] + x2    6.37/2.04
POL(False) = 0    6.37/2.04
POL(INSERT(x1, x2)) = 0    6.37/2.04
POL(INSERT[ITE](x1, x2, x3)) = 0    6.37/2.04
POL(ISORT(x1, x2)) = [2]x1    6.37/2.04
POL(S(x1)) = x1    6.37/2.04
POL(True) = [5]    6.37/2.04
POL(c(x1)) = x1    6.37/2.04
POL(c3(x1)) = x1    6.37/2.04
POL(c5(x1, x2)) = x1 + x2    6.37/2.04
POL(c7(x1, x2)) = x1 + x2    6.37/2.04
POL(insert(x1, x2)) = 0    6.37/2.04
POL(insert[Ite](x1, x2, x3)) = [3] + [3]x3   
6.37/2.05
6.37/2.05

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 6.37/2.05
<(0, S(z0)) → True 6.37/2.05
<(z0, 0) → False 6.37/2.05
insert[Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 6.37/2.05
insert[Ite](True, z0, z1) → Cons(z0, z1) 6.37/2.05
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 6.37/2.05
isort(Nil, z0) → Nil 6.37/2.05
insert(S(z0), z1) → insert[Ite](<(S(z0), z0), S(z0), z1) 6.37/2.05
inssort(z0) → isort(z0, Nil)
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 6.37/2.05
INSERT[ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 6.37/2.05
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.05
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
S tuples:

INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
K tuples:

ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
Defined Rule Symbols:

isort, insert, inssort, <, insert[Ite]

Defined Pair Symbols:

<', INSERT[ITE], ISORT, INSERT

Compound Symbols:

c, c3, c5, c7

6.37/2.05
6.37/2.05

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

INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
We considered the (Usable) Rules:

<(S(z0), S(z1)) → <(z0, z1) 6.37/2.05
<(z0, 0) → False 6.37/2.05
<(0, S(z0)) → True 6.37/2.05
insert(S(z0), z1) → insert[Ite](<(S(z0), z0), S(z0), z1) 6.37/2.05
insert[Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 6.37/2.05
insert[Ite](True, z0, z1) → Cons(z0, z1)
And the Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 6.37/2.05
INSERT[ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 6.37/2.05
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.05
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 6.37/2.05

POL(0) = 0    6.37/2.05
POL(<(x1, x2)) = 0    6.37/2.05
POL(<'(x1, x2)) = 0    6.37/2.05
POL(Cons(x1, x2)) = [2] + x2    6.37/2.05
POL(False) = 0    6.37/2.05
POL(INSERT(x1, x2)) = [1] + x2    6.37/2.05
POL(INSERT[ITE](x1, x2, x3)) = x3    6.37/2.05
POL(ISORT(x1, x2)) = [2]x1 + x1·x2 + [3]x12    6.37/2.05
POL(S(x1)) = 0    6.37/2.05
POL(True) = 0    6.37/2.05
POL(c(x1)) = x1    6.37/2.05
POL(c3(x1)) = x1    6.37/2.05
POL(c5(x1, x2)) = x1 + x2    6.37/2.05
POL(c7(x1, x2)) = x1 + x2    6.37/2.05
POL(insert(x1, x2)) = [2] + x2    6.37/2.05
POL(insert[Ite](x1, x2, x3)) = [2] + x3   
6.37/2.05
6.37/2.05

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

<(S(z0), S(z1)) → <(z0, z1) 6.37/2.05
<(0, S(z0)) → True 6.37/2.05
<(z0, 0) → False 6.37/2.05
insert[Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 6.37/2.05
insert[Ite](True, z0, z1) → Cons(z0, z1) 6.37/2.05
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 6.37/2.05
isort(Nil, z0) → Nil 6.37/2.05
insert(S(z0), z1) → insert[Ite](<(S(z0), z0), S(z0), z1) 6.37/2.05
inssort(z0) → isort(z0, Nil)
Tuples:

<'(S(z0), S(z1)) → c(<'(z0, z1)) 6.37/2.05
INSERT[ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 6.37/2.05
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.05
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
S tuples:none
K tuples:

ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 6.37/2.05
INSERT(S(z0), z1) → c7(INSERT[ITE](<(S(z0), z0), S(z0), z1), <'(S(z0), z0))
Defined Rule Symbols:

isort, insert, inssort, <, insert[Ite]

Defined Pair Symbols:

<', INSERT[ITE], ISORT, INSERT

Compound Symbols:

c, c3, c5, c7

6.37/2.05
6.37/2.05

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

The set S is empty
6.37/2.05
6.37/2.05

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

6.37/2.05
6.37/2.05
6.66/2.12 EOF