0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 QDPOrderProof (⇔)
↳7 QDP
↳8 PisEmptyProof (⇔)
↳9 TRUE
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 PisEmptyProof (⇔)
↳14 TRUE
↳15 QDP
↳16 QDPOrderProof (⇔)
↳17 QDP
↳18 QDPOrderProof (⇔)
↳19 QDP
↳20 QDPOrderProof (⇔)
↳21 QDP
↳22 PisEmptyProof (⇔)
↳23 TRUE
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 PisEmptyProof (⇔)
↳28 TRUE
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
FROM(X) → CONS(X, n__from(n__s(X)))
2NDSPOS(s(N), cons(X, n__cons(Y, Z))) → ACTIVATE(Y)
2NDSPOS(s(N), cons(X, n__cons(Y, Z))) → 2NDSNEG(N, activate(Z))
2NDSPOS(s(N), cons(X, n__cons(Y, Z))) → ACTIVATE(Z)
2NDSNEG(s(N), cons(X, n__cons(Y, Z))) → ACTIVATE(Y)
2NDSNEG(s(N), cons(X, n__cons(Y, Z))) → 2NDSPOS(N, activate(Z))
2NDSNEG(s(N), cons(X, n__cons(Y, Z))) → ACTIVATE(Z)
PI(X) → 2NDSPOS(X, from(0))
PI(X) → FROM(0)
PLUS(s(X), Y) → S(plus(X, Y))
PLUS(s(X), Y) → PLUS(X, Y)
TIMES(s(X), Y) → PLUS(Y, times(X, Y))
TIMES(s(X), Y) → TIMES(X, Y)
SQUARE(X) → TIMES(X, X)
ACTIVATE(n__from(X)) → FROM(activate(X))
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
PLUS(s(X), Y) → PLUS(X, Y)
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(X), Y) → PLUS(X, Y)
trivial
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
TIMES(s(X), Y) → TIMES(X, Y)
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(s(X), Y) → TIMES(X, Y)
trivial
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__s(X)) → ACTIVATE(X)
trivial
ACTIVATE(n__from(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__from(X)) → ACTIVATE(X)
trivial
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
ncons2 > ACTIVATE1
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
2NDSPOS(s(N), cons(X, n__cons(Y, Z))) → 2NDSNEG(N, activate(Z))
2NDSNEG(s(N), cons(X, n__cons(Y, Z))) → 2NDSPOS(N, activate(Z))
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
2NDSPOS(s(N), cons(X, n__cons(Y, Z))) → 2NDSNEG(N, activate(Z))
2NDSNEG(s(N), cons(X, n__cons(Y, Z))) → 2NDSPOS(N, activate(Z))
ncons2 > cons2 > activate1
from1 > cons2 > activate1
from1 > nfrom1 > activate1
from1 > ns1 > s1 > activate1
from(X) → cons(X, n__from(n__s(X)))
2ndspos(0, Z) → rnil
2ndspos(s(N), cons(X, n__cons(Y, Z))) → rcons(posrecip(activate(Y)), 2ndsneg(N, activate(Z)))
2ndsneg(0, Z) → rnil
2ndsneg(s(N), cons(X, n__cons(Y, Z))) → rcons(negrecip(activate(Y)), 2ndspos(N, activate(Z)))
pi(X) → 2ndspos(X, from(0))
plus(0, Y) → Y
plus(s(X), Y) → s(plus(X, Y))
times(0, Y) → 0
times(s(X), Y) → plus(Y, times(X, Y))
square(X) → times(X, X)
from(X) → n__from(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(X) → X