nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
LENGTH(cons(x, l)) → LENGTH(l)
COND(false, n, l) → NTHTAIL(s(n), l)
NTHTAIL(n, l) → GE(n, length(l))
COND(false, n, l) → TAIL(nthtail(s(n), l))
GE(s(u), s(v)) → GE(u, v)
NTHTAIL(n, l) → LENGTH(l)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
LENGTH(cons(x, l)) → LENGTH(l)
COND(false, n, l) → NTHTAIL(s(n), l)
NTHTAIL(n, l) → GE(n, length(l))
COND(false, n, l) → TAIL(nthtail(s(n), l))
GE(s(u), s(v)) → GE(u, v)
NTHTAIL(n, l) → LENGTH(l)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
GE(s(u), s(v)) → GE(u, v)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GE(s(u), s(v)) → GE(u, v)
The value of delta used in the strict ordering is 12.
POL(GE(x1, x2)) = (3)x_2
POL(s(x1)) = 4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
LENGTH(cons(x, l)) → LENGTH(l)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LENGTH(cons(x, l)) → LENGTH(l)
The value of delta used in the strict ordering is 4.
POL(LENGTH(x1)) = (4)x_1
POL(cons(x1, x2)) = 1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
COND(false, n, l) → NTHTAIL(s(n), l)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)