0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 PisEmptyProof (⇔)
↳8 TRUE
f(cons(nil, y)) → y
f(cons(f(cons(nil, y)), z)) → copy(n, y, z)
copy(0, y, z) → f(z)
copy(s(x), y, z) → copy(x, y, cons(f(y), z))
F(cons(f(cons(nil, y)), z)) → COPY(n, y, z)
COPY(0, y, z) → F(z)
COPY(s(x), y, z) → COPY(x, y, cons(f(y), z))
COPY(s(x), y, z) → F(y)
f(cons(nil, y)) → y
f(cons(f(cons(nil, y)), z)) → copy(n, y, z)
copy(0, y, z) → f(z)
copy(s(x), y, z) → copy(x, y, cons(f(y), z))
COPY(s(x), y, z) → COPY(x, y, cons(f(y), z))
f(cons(nil, y)) → y
f(cons(f(cons(nil, y)), z)) → copy(n, y, z)
copy(0, y, z) → f(z)
copy(s(x), y, z) → copy(x, y, cons(f(y), z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
COPY(s(x), y, z) → COPY(x, y, cons(f(y), z))
POL(COPY(x1, x2, x3)) = x1 + x3
POL(cons(x1, x2)) = 0
POL(copy(x1, x2, x3)) = 0
POL(f(x1)) = 0
POL(n) = 0
POL(nil) = 0
POL(s(x1)) = 1 + x1
f(cons(nil, y)) → y
f(cons(f(cons(nil, y)), z)) → copy(n, y, z)
copy(0, y, z) → f(z)
copy(s(x), y, z) → copy(x, y, cons(f(y), z))