(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
Q is empty.
(1) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The set Q consists of the following terms:
sort(x0)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
member(x0, nil)
member(x0, cons(x1, x2))
or(x0, true)
or(x0, false)
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
max(nil)
max(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SORT(l) → ST(0, l)
ST(n, l) → COND1(member(n, l), n, l)
ST(n, l) → MEMBER(n, l)
COND1(true, n, l) → ST(s(n), l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
COND1(false, n, l) → GT(n, max(l))
COND1(false, n, l) → MAX(l)
COND2(false, n, l) → ST(s(n), l)
MEMBER(n, cons(m, l)) → OR(equal(n, m), member(n, l))
MEMBER(n, cons(m, l)) → EQUAL(n, m)
MEMBER(n, cons(m, l)) → MEMBER(n, l)
EQUAL(s(x), s(y)) → EQUAL(x, y)
GT(s(u), s(v)) → GT(u, v)
MAX(cons(u, l)) → IF(gt(u, max(l)), u, max(l))
MAX(cons(u, l)) → GT(u, max(l))
MAX(cons(u, l)) → MAX(l)
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The set Q consists of the following terms:
sort(x0)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
member(x0, nil)
member(x0, cons(x1, x2))
or(x0, true)
or(x0, false)
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
max(nil)
max(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 8 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GT(s(u), s(v)) → GT(u, v)
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The set Q consists of the following terms:
sort(x0)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
member(x0, nil)
member(x0, cons(x1, x2))
or(x0, true)
or(x0, false)
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
max(nil)
max(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAX(cons(u, l)) → MAX(l)
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The set Q consists of the following terms:
sort(x0)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
member(x0, nil)
member(x0, cons(x1, x2))
or(x0, true)
or(x0, false)
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
max(nil)
max(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQUAL(s(x), s(y)) → EQUAL(x, y)
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The set Q consists of the following terms:
sort(x0)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
member(x0, nil)
member(x0, cons(x1, x2))
or(x0, true)
or(x0, false)
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
max(nil)
max(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MEMBER(n, cons(m, l)) → MEMBER(n, l)
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The set Q consists of the following terms:
sort(x0)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
member(x0, nil)
member(x0, cons(x1, x2))
or(x0, true)
or(x0, false)
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
max(nil)
max(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
COND1(true, n, l) → ST(s(n), l)
ST(n, l) → COND1(member(n, l), n, l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
COND2(false, n, l) → ST(s(n), l)
The TRS R consists of the following rules:
sort(l) → st(0, l)
st(n, l) → cond1(member(n, l), n, l)
cond1(true, n, l) → cons(n, st(s(n), l))
cond1(false, n, l) → cond2(gt(n, max(l)), n, l)
cond2(true, n, l) → nil
cond2(false, n, l) → st(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
or(x, true) → true
or(x, false) → x
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
if(true, u, v) → u
if(false, u, v) → v
The set Q consists of the following terms:
sort(x0)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
member(x0, nil)
member(x0, cons(x1, x2))
or(x0, true)
or(x0, false)
equal(0, 0)
equal(s(x0), 0)
equal(0, s(x0))
equal(s(x0), s(x1))
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
max(nil)
max(cons(x0, x1))
if(true, x0, x1)
if(false, x0, x1)
We have to consider all minimal (P,Q,R)-chains.