YES(O(1), O(n^2)) 5.03/1.79 YES(O(1), O(n^2)) 5.46/1.83 5.46/1.83 5.46/1.83
5.46/1.83 5.46/1.830 CpxRelTRS5.46/1.83
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))5.46/1.83
↳2 CdtProblem5.46/1.83
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)5.46/1.83
↳4 CdtProblem5.46/1.83
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))5.46/1.83
↳6 CdtProblem5.46/1.83
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))5.46/1.83
↳8 CdtProblem5.46/1.83
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))5.46/1.83
↳10 BOUNDS(O(1), O(1))5.46/1.83
isort(Cons(x, xs), r) → isort(xs, insert(x, r)) 5.46/1.83
insert(x', Cons(x, xs)) → insert[Ite][False][Ite](<(x', x), x', Cons(x, xs)) 5.46/1.83
isort(Nil, r) → r 5.46/1.83
insert(x, Nil) → Cons(x, Nil) 5.46/1.83
inssort(xs) → isort(xs, Nil)
<(S(x), S(y)) → <(x, y) 5.46/1.83
<(0, S(y)) → True 5.46/1.83
<(x, 0) → False 5.46/1.83
insert[Ite][False][Ite](False, x', Cons(x, xs)) → Cons(x, insert(x', xs)) 5.46/1.83
insert[Ite][False][Ite](True, x, r) → Cons(x, r)
Tuples:
<(S(z0), S(z1)) → <(z0, z1) 5.46/1.83
<(0, S(z0)) → True 5.46/1.83
<(z0, 0) → False 5.46/1.83
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 5.46/1.83
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1) 5.46/1.83
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 5.46/1.83
isort(Nil, z0) → z0 5.46/1.83
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 5.46/1.83
insert(z0, Nil) → Cons(z0, Nil) 5.46/1.83
inssort(z0) → isort(z0, Nil)
S tuples:
<'(S(z0), S(z1)) → c(<'(z0, z1)) 5.46/1.83
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 5.46/1.83
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 5.46/1.83
INSSORT(z0) → c9(ISORT(z0, Nil))
K tuples:none
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1)) 5.46/1.83
INSSORT(z0) → c9(ISORT(z0, Nil))
isort, insert, inssort, <, insert[Ite][False][Ite]
<', INSERT[ITE][FALSE][ITE], ISORT, INSERT, INSSORT
c, c3, c5, c7, c9
INSSORT(z0) → c9(ISORT(z0, Nil))
Tuples:
<(S(z0), S(z1)) → <(z0, z1) 5.46/1.83
<(0, S(z0)) → True 5.46/1.83
<(z0, 0) → False 5.46/1.83
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 5.46/1.83
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1) 5.46/1.83
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 5.46/1.83
isort(Nil, z0) → z0 5.46/1.83
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 5.46/1.83
insert(z0, Nil) → Cons(z0, Nil) 5.46/1.83
inssort(z0) → isort(z0, Nil)
S tuples:
<'(S(z0), S(z1)) → c(<'(z0, z1)) 5.46/1.83
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 5.46/1.83
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
K tuples:none
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
isort, insert, inssort, <, insert[Ite][False][Ite]
<', INSERT[ITE][FALSE][ITE], ISORT, INSERT
c, c3, c5, c7
We considered the (Usable) Rules:
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
And the Tuples:
<(S(z0), S(z1)) → <(z0, z1) 5.46/1.83
<(0, S(z0)) → True 5.46/1.83
<(z0, 0) → False 5.46/1.83
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 5.46/1.83
insert(z0, Nil) → Cons(z0, Nil) 5.46/1.83
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 5.46/1.83
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
The order we found is given by the following interpretation:
<'(S(z0), S(z1)) → c(<'(z0, z1)) 5.46/1.83
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 5.46/1.83
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
POL(0) = [3] 5.46/1.83
POL(<(x1, x2)) = 0 5.46/1.83
POL(<'(x1, x2)) = 0 5.46/1.83
POL(Cons(x1, x2)) = [2] + x2 5.46/1.83
POL(False) = 0 5.46/1.83
POL(INSERT(x1, x2)) = [1] 5.46/1.83
POL(INSERT[ITE][FALSE][ITE](x1, x2, x3)) = [1] 5.46/1.83
POL(ISORT(x1, x2)) = [2]x1 5.46/1.83
POL(Nil) = 0 5.46/1.83
POL(S(x1)) = [3] + x1 5.46/1.83
POL(True) = [5] 5.46/1.83
POL(c(x1)) = x1 5.46/1.83
POL(c3(x1)) = x1 5.46/1.83
POL(c5(x1, x2)) = x1 + x2 5.46/1.83
POL(c7(x1, x2)) = x1 + x2 5.46/1.83
POL(insert(x1, x2)) = 0 5.46/1.83
POL(insert[Ite][False][Ite](x1, x2, x3)) = [3] + [3]x2 + [3]x3
Tuples:
<(S(z0), S(z1)) → <(z0, z1) 5.46/1.83
<(0, S(z0)) → True 5.46/1.83
<(z0, 0) → False 5.46/1.83
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 5.46/1.83
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1) 5.46/1.83
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 5.46/1.83
isort(Nil, z0) → z0 5.46/1.83
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 5.46/1.83
insert(z0, Nil) → Cons(z0, Nil) 5.46/1.83
inssort(z0) → isort(z0, Nil)
S tuples:
<'(S(z0), S(z1)) → c(<'(z0, z1)) 5.46/1.83
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 5.46/1.83
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
K tuples:
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
Defined Rule Symbols:
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2))
isort, insert, inssort, <, insert[Ite][False][Ite]
<', INSERT[ITE][FALSE][ITE], ISORT, INSERT
c, c3, c5, c7
We considered the (Usable) Rules:
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
And the Tuples:
<(S(z0), S(z1)) → <(z0, z1) 5.46/1.83
<(0, S(z0)) → True 5.46/1.83
<(z0, 0) → False 5.46/1.83
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 5.46/1.83
insert(z0, Nil) → Cons(z0, Nil) 5.46/1.83
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 5.46/1.83
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1)
The order we found is given by the following interpretation:
<'(S(z0), S(z1)) → c(<'(z0, z1)) 5.46/1.83
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 5.46/1.83
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
POL(0) = 0 5.46/1.83
POL(<(x1, x2)) = 0 5.46/1.83
POL(<'(x1, x2)) = 0 5.46/1.83
POL(Cons(x1, x2)) = [1] + x2 5.46/1.83
POL(False) = 0 5.46/1.83
POL(INSERT(x1, x2)) = [1] + x2 5.46/1.83
POL(INSERT[ITE][FALSE][ITE](x1, x2, x3)) = x3 5.46/1.83
POL(ISORT(x1, x2)) = [2]x1·x2 + x12 5.46/1.83
POL(Nil) = 0 5.46/1.83
POL(S(x1)) = 0 5.46/1.83
POL(True) = 0 5.46/1.83
POL(c(x1)) = x1 5.46/1.83
POL(c3(x1)) = x1 5.46/1.83
POL(c5(x1, x2)) = x1 + x2 5.46/1.83
POL(c7(x1, x2)) = x1 + x2 5.46/1.83
POL(insert(x1, x2)) = [1] + x2 5.46/1.83
POL(insert[Ite][False][Ite](x1, x2, x3)) = [1] + x3
Tuples:
<(S(z0), S(z1)) → <(z0, z1) 5.46/1.83
<(0, S(z0)) → True 5.46/1.83
<(z0, 0) → False 5.46/1.83
insert[Ite][False][Ite](False, z0, Cons(z1, z2)) → Cons(z1, insert(z0, z2)) 5.46/1.83
insert[Ite][False][Ite](True, z0, z1) → Cons(z0, z1) 5.46/1.83
isort(Cons(z0, z1), z2) → isort(z1, insert(z0, z2)) 5.46/1.83
isort(Nil, z0) → z0 5.46/1.83
insert(z0, Cons(z1, z2)) → insert[Ite][False][Ite](<(z0, z1), z0, Cons(z1, z2)) 5.46/1.83
insert(z0, Nil) → Cons(z0, Nil) 5.46/1.83
inssort(z0) → isort(z0, Nil)
S tuples:none
<'(S(z0), S(z1)) → c(<'(z0, z1)) 5.46/1.83
INSERT[ITE][FALSE][ITE](False, z0, Cons(z1, z2)) → c3(INSERT(z0, z2)) 5.46/1.83
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
Defined Rule Symbols:
ISORT(Cons(z0, z1), z2) → c5(ISORT(z1, insert(z0, z2)), INSERT(z0, z2)) 5.46/1.83
INSERT(z0, Cons(z1, z2)) → c7(INSERT[ITE][FALSE][ITE](<(z0, z1), z0, Cons(z1, z2)), <'(z0, z1))
isort, insert, inssort, <, insert[Ite][False][Ite]
<', INSERT[ITE][FALSE][ITE], ISORT, INSERT
c, c3, c5, c7