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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
ST(n, l) → MEMBER(n, l)
COND1(false, n, l) → MAX(l)
COND1(false, n, l) → GT(n, max(l))
GT(s(u), s(v)) → GT(u, v)
MEMBER(n, cons(m, l)) → OR(equal(n, m), member(n, l))
MAX(cons(u, l)) → MAX(l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
SORT(l) → ST(0, l)
MAX(cons(u, l)) → GT(u, max(l))
MAX(cons(u, l)) → IF(gt(u, max(l)), u, max(l))
MEMBER(n, cons(m, l)) → EQUAL(n, m)
EQUAL(s(x), s(y)) → EQUAL(x, y)
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
MEMBER(n, cons(m, l)) → MEMBER(n, l)
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
ST(n, l) → MEMBER(n, l)
COND1(false, n, l) → MAX(l)
COND1(false, n, l) → GT(n, max(l))
GT(s(u), s(v)) → GT(u, v)
MEMBER(n, cons(m, l)) → OR(equal(n, m), member(n, l))
MAX(cons(u, l)) → MAX(l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
SORT(l) → ST(0, l)
MAX(cons(u, l)) → GT(u, max(l))
MAX(cons(u, l)) → IF(gt(u, max(l)), u, max(l))
MEMBER(n, cons(m, l)) → EQUAL(n, m)
EQUAL(s(x), s(y)) → EQUAL(x, y)
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
MEMBER(n, cons(m, l)) → MEMBER(n, l)
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GT(s(u), s(v)) → GT(u, v)
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GT(s(u), s(v)) → GT(u, v)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GT(s(u), s(v)) → GT(u, v)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
MAX(cons(u, l)) → MAX(l)
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
MAX(cons(u, l)) → MAX(l)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
MAX(cons(u, l)) → MAX(l)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
EQUAL(s(x), s(y)) → EQUAL(x, y)
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
EQUAL(s(x), s(y)) → EQUAL(x, y)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
EQUAL(s(x), s(y)) → EQUAL(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
MEMBER(n, cons(m, l)) → MEMBER(n, l)
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
MEMBER(n, cons(m, l)) → MEMBER(n, l)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
MEMBER(n, cons(m, l)) → MEMBER(n, l)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
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
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
sort(x0)
cond2(false, x0, x1)
gt(s(x0), s(x1))
cond2(true, x0, x1)
equal(s(x0), s(x1))
st(x0, x1)
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
cond1(true, x0, x1)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
cond1(false, x0, x1)
sort(x0)
cond2(false, x0, x1)
cond2(true, x0, x1)
st(x0, x1)
cond1(true, x0, x1)
cond1(false, x0, x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
ST(x0, nil) → COND1(false, x0, nil)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ NonInfProof
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
ST(x0, nil) → COND1(false, x0, nil)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
COND1(false, y0, nil) → COND2(gt(y0, 0), y0, nil)
COND1(false, 0, y1) → COND2(false, 0, y1)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ NonInfProof
COND1(false, y0, nil) → COND2(gt(y0, 0), y0, nil)
COND1(false, 0, y1) → COND2(false, 0, y1)
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
COND1(true, n, l) → ST(s(n), l)
ST(x0, nil) → COND1(false, x0, nil)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ NonInfProof
COND1(false, y0, nil) → COND2(gt(y0, 0), y0, nil)
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
COND1(false, 0, y1) → COND2(false, 0, y1)
ST(x0, nil) → COND1(false, x0, nil)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
COND2(false, 0, z0) → ST(s(0), z0)
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND2(false, z0, nil) → ST(s(z0), nil)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ NonInfProof
COND1(false, y0, nil) → COND2(gt(y0, 0), y0, nil)
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND1(false, 0, y1) → COND2(false, 0, y1)
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
COND2(false, 0, z0) → ST(s(0), z0)
ST(x0, nil) → COND1(false, x0, nil)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, z0, nil) → ST(s(z0), nil)
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ NonInfProof
COND1(false, y0, nil) → COND2(gt(y0, 0), y0, nil)
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND1(false, 0, y1) → COND2(false, 0, y1)
ST(x0, nil) → COND1(false, x0, nil)
COND2(false, 0, z0) → ST(s(0), z0)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND2(false, z0, nil) → ST(s(z0), nil)
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
ST(s(0), nil) → COND1(false, s(0), nil)
ST(s(z0), nil) → COND1(false, s(z0), nil)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
COND1(false, y0, nil) → COND2(gt(y0, 0), y0, nil)
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND1(false, 0, y1) → COND2(false, 0, y1)
ST(s(0), nil) → COND1(false, s(0), nil)
COND2(false, 0, z0) → ST(s(0), z0)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, z0, nil) → ST(s(z0), nil)
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
ST(s(z0), nil) → COND1(false, s(z0), nil)
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ NonInfProof
COND1(false, y0, nil) → COND2(gt(y0, 0), y0, nil)
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
ST(s(0), nil) → COND1(false, s(0), nil)
COND2(false, 0, z0) → ST(s(0), z0)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, z0, nil) → ST(s(z0), nil)
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
ST(s(z0), nil) → COND1(false, s(z0), nil)
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
COND1(false, 0, nil) → COND2(false, 0, nil)
COND1(false, s(x0), nil) → COND2(true, s(x0), nil)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND1(false, 0, nil) → COND2(false, 0, nil)
COND2(false, 0, z0) → ST(s(0), z0)
ST(s(0), nil) → COND1(false, s(0), nil)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND2(false, z0, nil) → ST(s(z0), nil)
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
COND1(false, s(x0), nil) → COND2(true, s(x0), nil)
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
ST(s(z0), nil) → COND1(false, s(z0), nil)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ NonInfProof
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND2(false, 0, z0) → ST(s(0), z0)
COND1(false, y0, cons(x0, x1)) → COND2(gt(y0, if(gt(x0, max(x1)), x0, max(x1))), y0, cons(x0, x1))
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
COND1(false, s(z0), cons(z1, z2)) → COND2(gt(s(z0), if(gt(z1, max(z2)), z1, max(z2))), s(z0), cons(z1, z2))
COND1(false, s(0), cons(z0, z1)) → COND2(gt(s(0), if(gt(z0, max(z1)), z0, max(z1))), s(0), cons(z0, z1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND2(false, 0, z0) → ST(s(0), z0)
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND1(false, s(z0), cons(z1, z2)) → COND2(gt(s(z0), if(gt(z1, max(z2)), z1, max(z2))), s(z0), cons(z1, z2))
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
COND1(false, s(0), cons(z0, z1)) → COND2(gt(s(0), if(gt(z0, max(z1)), z0, max(z1))), s(0), cons(z0, z1))
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ NonInfProof
COND1(true, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND2(false, z0, cons(z1, z2)) → ST(s(z0), cons(z1, z2))
COND1(false, s(z0), cons(z1, z2)) → COND2(gt(s(z0), if(gt(z1, max(z2)), z1, max(z2))), s(z0), cons(z1, z2))
ST(s(z0), cons(z1, z2)) → COND1(or(equal(s(z0), z1), member(s(z0), z2)), s(z0), cons(z1, z2))
COND1(false, s(0), cons(z0, z1)) → COND2(gt(s(0), if(gt(z0, max(z1)), z0, max(z1))), s(0), cons(z0, z1))
ST(s(0), cons(x1, x2)) → COND1(or(equal(s(0), x1), member(s(0), x2)), s(0), cons(x1, x2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
POL(0) = 0
POL(COND1(x1, x2, x3)) = -1 - x1 - x2 + x3
POL(COND2(x1, x2, x3)) = -1 - x1 - x2 + x3
POL(ST(x1, x2)) = -1 - x1 + x2
POL(c) = -1
POL(cons(x1, x2)) = 2·x1 + x2
POL(equal(x1, x2)) = 0
POL(false) = 0
POL(gt(x1, x2)) = 0
POL(if(x1, x2, x3)) = 1 + 2·x1
POL(max(x1)) = 2
POL(member(x1, x2)) = 0
POL(nil) = 0
POL(or(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
The following rules are usable:
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
true → or(x, true)
false → gt(0, v)
false → member(n, nil)
gt(u, v) → gt(s(u), s(v))
x → or(x, false)
or(equal(n, m), member(n, l)) → member(n, cons(m, l))
true → gt(s(u), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
ST(n, l) → COND1(member(n, l), n, l)
COND1(false, n, l) → COND2(gt(n, max(l)), n, l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
COND2(false, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(nil) → 0
max(cons(u, l)) → if(gt(u, max(l)), u, max(l))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
if(true, u, v) → u
if(false, u, v) → v
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
max(cons(x0, x1))
equal(0, 0)
equal(s(x0), 0)
gt(s(x0), s(x1))
equal(s(x0), s(x1))
if(false, x0, x1)
max(nil)
member(x0, cons(x1, x2))
gt(0, x0)
member(x0, nil)
or(x0, false)
or(x0, true)
if(true, x0, x1)
equal(0, s(x0))
gt(s(x0), 0)
max(cons(x0, x1))
gt(s(x0), s(x1))
if(false, x0, x1)
max(nil)
gt(0, x0)
if(true, x0, x1)
gt(s(x0), 0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
ST(n, l) → COND1(member(n, l), n, l)
COND1(true, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
equal(0, 0)
equal(s(x0), 0)
equal(s(x0), s(x1))
member(x0, cons(x1, x2))
member(x0, nil)
or(x0, false)
or(x0, true)
equal(0, s(x0))
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
ST(x0, nil) → COND1(false, x0, nil)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ NonInfProof
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
ST(x0, nil) → COND1(false, x0, nil)
COND1(true, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
equal(0, 0)
equal(s(x0), 0)
equal(s(x0), s(x1))
member(x0, cons(x1, x2))
member(x0, nil)
or(x0, false)
or(x0, true)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ NonInfProof
ST(x0, cons(x1, x2)) → COND1(or(equal(x0, x1), member(x0, x2)), x0, cons(x1, x2))
COND1(true, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
equal(0, 0)
equal(s(x0), 0)
equal(s(x0), s(x1))
member(x0, cons(x1, x2))
member(x0, nil)
or(x0, false)
or(x0, true)
equal(0, s(x0))
ST(s(z0), cons(x1, x2)) → COND1(or(equal(s(z0), x1), member(s(z0), x2)), s(z0), cons(x1, x2))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Instantiation
↳ QDP
↳ NonInfProof
COND1(true, n, l) → ST(s(n), l)
ST(s(z0), cons(x1, x2)) → COND1(or(equal(s(z0), x1), member(s(z0), x2)), s(z0), cons(x1, x2))
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
equal(0, 0)
equal(s(x0), 0)
equal(s(x0), s(x1))
member(x0, cons(x1, x2))
member(x0, nil)
or(x0, false)
or(x0, true)
equal(0, s(x0))
POL(0) = 0
POL(COND1(x1, x2, x3)) = -1 - x1 - x2 + x3
POL(ST(x1, x2)) = -1 - x1 + x2
POL(c) = -1
POL(cons(x1, x2)) = x1 + x2
POL(equal(x1, x2)) = x1
POL(false) = 0
POL(member(x1, x2)) = 0
POL(nil) = 2
POL(or(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
COND1(true, n, l) → ST(s(n), l)
The following rules are usable:
ST(n, l) → COND1(member(n, l), n, l)
true → or(x, true)
or(equal(n, m), member(n, l)) → member(n, cons(m, l))
false → member(n, nil)
x → or(x, false)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
ST(n, l) → COND1(member(n, l), n, l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
equal(0, 0)
equal(s(x0), 0)
equal(s(x0), s(x1))
member(x0, cons(x1, x2))
member(x0, nil)
or(x0, false)
or(x0, true)
equal(0, s(x0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ NonInfProof
↳ AND
↳ QDP
↳ QDP
↳ DependencyGraphProof
COND1(true, n, l) → ST(s(n), l)
member(n, nil) → false
member(n, cons(m, l)) → or(equal(n, m), member(n, l))
equal(0, 0) → true
equal(s(x), 0) → false
equal(0, s(y)) → false
equal(s(x), s(y)) → equal(x, y)
or(x, true) → true
or(x, false) → x
equal(0, 0)
equal(s(x0), 0)
equal(s(x0), s(x1))
member(x0, cons(x1, x2))
member(x0, nil)
or(x0, false)
or(x0, true)
equal(0, s(x0))