We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {sort(nil()) -> nil()}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(sort) = {}, Uargs(cons) = {2}, Uargs(insert) = {2},
Uargs(choose) = {}, Uargs(s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
sort(x1) = [0 0] x1 + [1]
[0 0] [1]
nil() = [0]
[0]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [1]
[1 0] [0 1] [1]
insert(x1, x2) = [0 0] x1 + [1 1] x2 + [1]
[0 0] [0 0] [1]
choose(x1, x2, x3, x4) = [0 0] x1 + [1 1] x2 + [0 0] x3 + [0 0] x4 + [1]
[1 1] [0 0] [0 0] [1 1] [1]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
Weak Trs: {sort(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component: {insert(x, nil()) -> cons(x, nil())}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(sort) = {}, Uargs(cons) = {2}, Uargs(insert) = {2},
Uargs(choose) = {}, Uargs(s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
sort(x1) = [0 0] x1 + [1]
[0 0] [0]
nil() = [0]
[0]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 1] [0]
insert(x1, x2) = [0 0] x1 + [1 1] x2 + [2]
[1 0] [0 0] [0]
choose(x1, x2, x3, x4) = [0 0] x1 + [1 1] x2 + [0 0] x3 + [0 0] x4 + [0]
[0 0] [0 0] [0 0] [0 0] [1]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
Weak Trs:
{ insert(x, nil()) -> cons(x, nil())
, sort(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(sort) = {}, Uargs(cons) = {2}, Uargs(insert) = {2},
Uargs(choose) = {}, Uargs(s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
sort(x1) = [0 0] x1 + [1]
[0 0] [0]
nil() = [0]
[0]
cons(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
[1 0] [0 1] [0]
insert(x1, x2) = [0 0] x1 + [1 1] x2 + [2]
[1 0] [0 0] [2]
choose(x1, x2, x3, x4) = [0 0] x1 + [1 1] x2 + [0 0] x3 + [0 0] x4 + [0]
[1 0] [0 0] [0 0] [0 0] [1]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ sort(cons(x, y)) -> insert(x, sort(y))
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
Weak Trs:
{ insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, insert(x, nil()) -> cons(x, nil())
, sort(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
The weightgap principle does not apply
We try instead 'weightgap of dimension Nat 3, maximal degree 2, cbits 3' on the problem
Strict Trs:
{ sort(cons(x, y)) -> insert(x, sort(y))
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
Weak Trs:
{ insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, insert(x, nil()) -> cons(x, nil())
, sort(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
The weightgap principle applies, where following rules are oriented strictly:
TRS Component:
{choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)}
Interpretation of nonconstant growth:
-------------------------------------
The following argument positions are usable:
Uargs(sort) = {}, Uargs(cons) = {2}, Uargs(insert) = {2},
Uargs(choose) = {}, Uargs(s) = {}
We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
Interpretation Functions:
sort(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
nil() = [0]
[0]
[0]
cons(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
[1 0 0] [0 1 2] [0]
[0 0 1] [0 0 0] [2]
insert(x1, x2) = [0 0 0] x1 + [1 1 2] x2 + [0]
[1 0 0] [0 0 0] [0]
[0 0 1] [0 0 0] [2]
choose(x1, x2, x3, x4) = [0 0 0] x1 + [1 1 0] x2 + [0 0 0] x3 + [0 0 1] x4 + [1]
[1 0 0] [0 0 0] [0 0 0] [0 0 0] [0]
[0 0 1] [0 0 0] [0 0 0] [0 0 0] [1]
0() = [0]
[0]
[0]
s(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 1] [1]
The strictly oriented rules are moved into the weak component.
We consider the following Problem:
Strict Trs:
{ sort(cons(x, y)) -> insert(x, sort(y))
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))}
Weak Trs:
{ choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, insert(x, nil()) -> cons(x, nil())
, sort(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
We consider the following Problem:
Strict Trs:
{ sort(cons(x, y)) -> insert(x, sort(y))
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))}
Weak Trs:
{ choose(x, cons(v, w), s(y), s(z)) -> choose(x, cons(v, w), y, z)
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, insert(x, nil()) -> cons(x, nil())
, sort(nil()) -> nil()}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^2))
Proof:
The following argument positions are usable:
Uargs(sort) = {}, Uargs(cons) = {2}, Uargs(insert) = {2},
Uargs(choose) = {}, Uargs(s) = {}
We have the following constructor-based EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
Interpretation Functions:
sort(x1) = [2 0 1] x1 + [1]
[0 0 0] [0]
[0 0 1] [0]
nil() = [1]
[0]
[0]
cons(x1, x2) = [0 0 0] x1 + [1 0 1] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 1] [1]
insert(x1, x2) = [0 0 0] x1 + [1 0 2] x2 + [0]
[0 0 0] [0 0 0] [0]
[0 0 0] [0 0 1] [1]
choose(x1, x2, x3, x4) = [0 0 0] x1 + [1 0 2] x2 + [0 0 0] x3 + [0 0 0] x4 + [0]
[0 0 0] [0 0 0] [0 0 0] [0 0 0] [0]
[0 0 0] [0 0 1] [0 0 0] [0 0 0] [1]
0() = [0]
[0]
[0]
s(x1) = [0 0 0] x1 + [0]
[0 0 0] [0]
[0 0 0] [0]
Hurray, we answered YES(?,O(n^2))