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 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
↳18 QDPOrderProof (⇔)
↳19 QDP
↳20 PisEmptyProof (⇔)
↳21 TRUE
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 QDPOrderProof (⇔)
↳26 QDP
↳27 PisEmptyProof (⇔)
↳28 TRUE
↳29 QDP
↳30 QDPOrderProof (⇔)
↳31 QDP
↳32 QDPOrderProof (⇔)
↳33 QDP
↳34 PisEmptyProof (⇔)
↳35 TRUE
↳36 QDP
↳37 QDPOrderProof (⇔)
↳38 QDP
↳39 QDPOrderProof (⇔)
↳40 QDP
↳41 PisEmptyProof (⇔)
↳42 TRUE
↳43 QDP
↳44 QDPOrderProof (⇔)
↳45 QDP
↳46 PisEmptyProof (⇔)
↳47 TRUE
↳48 QDP
↳49 QDPOrderProof (⇔)
↳50 QDP
↳51 QDPOrderProof (⇔)
↳52 QDP
↳53 PisEmptyProof (⇔)
↳54 TRUE
↳55 QDP
↳56 QDPOrderProof (⇔)
↳57 QDP
↳58 DependencyGraphProof (⇔)
↳59 QDP
↳60 QDPOrderProof (⇔)
↳61 QDP
↳62 PisEmptyProof (⇔)
↳63 TRUE
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
ACTIVE(terms(N)) → MARK(cons(recip(sqr(N)), terms(s(N))))
ACTIVE(terms(N)) → CONS(recip(sqr(N)), terms(s(N)))
ACTIVE(terms(N)) → RECIP(sqr(N))
ACTIVE(terms(N)) → SQR(N)
ACTIVE(terms(N)) → TERMS(s(N))
ACTIVE(terms(N)) → S(N)
ACTIVE(sqr(0)) → MARK(0)
ACTIVE(sqr(s(X))) → MARK(s(add(sqr(X), dbl(X))))
ACTIVE(sqr(s(X))) → S(add(sqr(X), dbl(X)))
ACTIVE(sqr(s(X))) → ADD(sqr(X), dbl(X))
ACTIVE(sqr(s(X))) → SQR(X)
ACTIVE(sqr(s(X))) → DBL(X)
ACTIVE(dbl(0)) → MARK(0)
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
ACTIVE(dbl(s(X))) → S(s(dbl(X)))
ACTIVE(dbl(s(X))) → S(dbl(X))
ACTIVE(dbl(s(X))) → DBL(X)
ACTIVE(add(0, X)) → MARK(X)
ACTIVE(add(s(X), Y)) → MARK(s(add(X, Y)))
ACTIVE(add(s(X), Y)) → S(add(X, Y))
ACTIVE(add(s(X), Y)) → ADD(X, Y)
ACTIVE(first(0, X)) → MARK(nil)
ACTIVE(first(s(X), cons(Y, Z))) → MARK(cons(Y, first(X, Z)))
ACTIVE(first(s(X), cons(Y, Z))) → CONS(Y, first(X, Z))
ACTIVE(first(s(X), cons(Y, Z))) → FIRST(X, Z)
MARK(terms(X)) → ACTIVE(terms(mark(X)))
MARK(terms(X)) → TERMS(mark(X))
MARK(terms(X)) → MARK(X)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
MARK(cons(X1, X2)) → MARK(X1)
MARK(recip(X)) → ACTIVE(recip(mark(X)))
MARK(recip(X)) → RECIP(mark(X))
MARK(recip(X)) → MARK(X)
MARK(sqr(X)) → ACTIVE(sqr(mark(X)))
MARK(sqr(X)) → SQR(mark(X))
MARK(sqr(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(X))
MARK(0) → ACTIVE(0)
MARK(add(X1, X2)) → ACTIVE(add(mark(X1), mark(X2)))
MARK(add(X1, X2)) → ADD(mark(X1), mark(X2))
MARK(add(X1, X2)) → MARK(X1)
MARK(add(X1, X2)) → MARK(X2)
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
MARK(dbl(X)) → DBL(mark(X))
MARK(dbl(X)) → MARK(X)
MARK(first(X1, X2)) → ACTIVE(first(mark(X1), mark(X2)))
MARK(first(X1, X2)) → FIRST(mark(X1), mark(X2))
MARK(first(X1, X2)) → MARK(X1)
MARK(first(X1, X2)) → MARK(X2)
MARK(nil) → ACTIVE(nil)
TERMS(mark(X)) → TERMS(X)
TERMS(active(X)) → TERMS(X)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
RECIP(mark(X)) → RECIP(X)
RECIP(active(X)) → RECIP(X)
SQR(mark(X)) → SQR(X)
SQR(active(X)) → SQR(X)
S(mark(X)) → S(X)
S(active(X)) → S(X)
ADD(mark(X1), X2) → ADD(X1, X2)
ADD(X1, mark(X2)) → ADD(X1, X2)
ADD(active(X1), X2) → ADD(X1, X2)
ADD(X1, active(X2)) → ADD(X1, X2)
DBL(mark(X)) → DBL(X)
DBL(active(X)) → DBL(X)
FIRST(mark(X1), X2) → FIRST(X1, X2)
FIRST(X1, mark(X2)) → FIRST(X1, X2)
FIRST(active(X1), X2) → FIRST(X1, X2)
FIRST(X1, active(X2)) → FIRST(X1, X2)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
FIRST(X1, mark(X2)) → FIRST(X1, X2)
FIRST(mark(X1), X2) → FIRST(X1, X2)
FIRST(active(X1), X2) → FIRST(X1, X2)
FIRST(X1, active(X2)) → FIRST(X1, X2)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
FIRST(X1, mark(X2)) → FIRST(X1, X2)
FIRST(mark(X1), X2) → FIRST(X1, X2)
FIRST(active(X1), X2) → FIRST(X1, X2)
FIRST(X1, active(X2)) → FIRST(X1, X2)
mark1 > FIRST2
active1 > FIRST2
FIRST2: [1,2]
mark1: [1]
active1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
DBL(active(X)) → DBL(X)
DBL(mark(X)) → DBL(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DBL(active(X)) → DBL(X)
trivial
active1: [1]
DBL(mark(X)) → DBL(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DBL(mark(X)) → DBL(X)
mark1 > DBL1
DBL1: [1]
mark1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
ADD(X1, mark(X2)) → ADD(X1, X2)
ADD(mark(X1), X2) → ADD(X1, X2)
ADD(active(X1), X2) → ADD(X1, X2)
ADD(X1, active(X2)) → ADD(X1, X2)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ADD(X1, mark(X2)) → ADD(X1, X2)
ADD(mark(X1), X2) → ADD(X1, X2)
ADD(active(X1), X2) → ADD(X1, X2)
ADD(X1, active(X2)) → ADD(X1, X2)
mark1 > ADD2
active1 > ADD2
ADD2: [1,2]
mark1: [1]
active1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
S(active(X)) → S(X)
S(mark(X)) → S(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(active(X)) → S(X)
trivial
active1: [1]
S(mark(X)) → S(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
S(mark(X)) → S(X)
mark1 > S1
S1: [1]
mark1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
SQR(active(X)) → SQR(X)
SQR(mark(X)) → SQR(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SQR(active(X)) → SQR(X)
trivial
active1: [1]
SQR(mark(X)) → SQR(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SQR(mark(X)) → SQR(X)
mark1 > SQR1
SQR1: [1]
mark1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
RECIP(active(X)) → RECIP(X)
RECIP(mark(X)) → RECIP(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
RECIP(active(X)) → RECIP(X)
trivial
active1: [1]
RECIP(mark(X)) → RECIP(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
RECIP(mark(X)) → RECIP(X)
mark1 > RECIP1
RECIP1: [1]
mark1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
mark1 > CONS2
active1 > CONS2
CONS2: [1,2]
mark1: [1]
active1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
TERMS(active(X)) → TERMS(X)
TERMS(mark(X)) → TERMS(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TERMS(active(X)) → TERMS(X)
trivial
active1: [1]
TERMS(mark(X)) → TERMS(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TERMS(mark(X)) → TERMS(X)
mark1 > TERMS1
TERMS1: [1]
mark1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
MARK(terms(X)) → ACTIVE(terms(mark(X)))
ACTIVE(terms(N)) → MARK(cons(recip(sqr(N)), terms(s(N))))
MARK(terms(X)) → MARK(X)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(sqr(s(X))) → MARK(s(add(sqr(X), dbl(X))))
MARK(cons(X1, X2)) → MARK(X1)
MARK(recip(X)) → ACTIVE(recip(mark(X)))
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
MARK(recip(X)) → MARK(X)
MARK(sqr(X)) → ACTIVE(sqr(mark(X)))
ACTIVE(add(0, X)) → MARK(X)
MARK(sqr(X)) → MARK(X)
MARK(s(X)) → ACTIVE(s(X))
ACTIVE(add(s(X), Y)) → MARK(s(add(X, Y)))
MARK(add(X1, X2)) → ACTIVE(add(mark(X1), mark(X2)))
ACTIVE(first(s(X), cons(Y, Z))) → MARK(cons(Y, first(X, Z)))
MARK(add(X1, X2)) → MARK(X1)
MARK(add(X1, X2)) → MARK(X2)
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
MARK(dbl(X)) → MARK(X)
MARK(first(X1, X2)) → ACTIVE(first(mark(X1), mark(X2)))
MARK(first(X1, X2)) → MARK(X1)
MARK(first(X1, X2)) → MARK(X2)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACTIVE(terms(N)) → MARK(cons(recip(sqr(N)), terms(s(N))))
MARK(terms(X)) → MARK(X)
ACTIVE(sqr(s(X))) → MARK(s(add(sqr(X), dbl(X))))
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(dbl(s(X))) → MARK(s(s(dbl(X))))
ACTIVE(add(0, X)) → MARK(X)
MARK(sqr(X)) → MARK(X)
ACTIVE(add(s(X), Y)) → MARK(s(add(X, Y)))
ACTIVE(first(s(X), cons(Y, Z))) → MARK(cons(Y, first(X, Z)))
MARK(add(X1, X2)) → MARK(X1)
MARK(add(X1, X2)) → MARK(X2)
MARK(dbl(X)) → MARK(X)
MARK(first(X1, X2)) → MARK(X1)
MARK(first(X1, X2)) → MARK(X2)
terms1 > cons1
terms1 > sqr1
s > sqr1
s > add2
s > dbl1 > 0 > nil
s > first2 > cons1
s > first2 > nil
terms1: [1]
cons1: [1]
sqr1: [1]
s: []
add2: [2,1]
dbl1: [1]
0: []
first2: [2,1]
nil: []
mark(terms(X)) → active(terms(mark(X)))
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
mark(recip(X)) → active(recip(mark(X)))
active(dbl(s(X))) → mark(s(s(dbl(X))))
mark(sqr(X)) → active(sqr(mark(X)))
active(add(0, X)) → mark(X)
mark(s(X)) → active(s(X))
active(add(s(X), Y)) → mark(s(add(X, Y)))
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(0) → active(0)
mark(nil) → active(nil)
terms(active(X)) → terms(X)
terms(mark(X)) → terms(X)
sqr(active(X)) → sqr(X)
sqr(mark(X)) → sqr(X)
recip(active(X)) → recip(X)
recip(mark(X)) → recip(X)
s(active(X)) → s(X)
s(mark(X)) → s(X)
cons(X1, mark(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
dbl(active(X)) → dbl(X)
dbl(mark(X)) → dbl(X)
add(X1, mark(X2)) → add(X1, X2)
add(mark(X1), X2) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(mark(X1), X2) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
active(sqr(0)) → mark(0)
active(dbl(0)) → mark(0)
active(first(0, X)) → mark(nil)
MARK(terms(X)) → ACTIVE(terms(mark(X)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(recip(X)) → ACTIVE(recip(mark(X)))
MARK(recip(X)) → MARK(X)
MARK(sqr(X)) → ACTIVE(sqr(mark(X)))
MARK(s(X)) → ACTIVE(s(X))
MARK(add(X1, X2)) → ACTIVE(add(mark(X1), mark(X2)))
MARK(dbl(X)) → ACTIVE(dbl(mark(X)))
MARK(first(X1, X2)) → ACTIVE(first(mark(X1), mark(X2)))
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
MARK(recip(X)) → MARK(X)
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(recip(X)) → MARK(X)
recip1 > MARK1
MARK1: [1]
recip1: [1]
active(terms(N)) → mark(cons(recip(sqr(N)), terms(s(N))))
active(sqr(0)) → mark(0)
active(sqr(s(X))) → mark(s(add(sqr(X), dbl(X))))
active(dbl(0)) → mark(0)
active(dbl(s(X))) → mark(s(s(dbl(X))))
active(add(0, X)) → mark(X)
active(add(s(X), Y)) → mark(s(add(X, Y)))
active(first(0, X)) → mark(nil)
active(first(s(X), cons(Y, Z))) → mark(cons(Y, first(X, Z)))
mark(terms(X)) → active(terms(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(recip(X)) → active(recip(mark(X)))
mark(sqr(X)) → active(sqr(mark(X)))
mark(s(X)) → active(s(X))
mark(0) → active(0)
mark(add(X1, X2)) → active(add(mark(X1), mark(X2)))
mark(dbl(X)) → active(dbl(mark(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
mark(nil) → active(nil)
terms(mark(X)) → terms(X)
terms(active(X)) → terms(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
recip(mark(X)) → recip(X)
recip(active(X)) → recip(X)
sqr(mark(X)) → sqr(X)
sqr(active(X)) → sqr(X)
s(mark(X)) → s(X)
s(active(X)) → s(X)
add(mark(X1), X2) → add(X1, X2)
add(X1, mark(X2)) → add(X1, X2)
add(active(X1), X2) → add(X1, X2)
add(X1, active(X2)) → add(X1, X2)
dbl(mark(X)) → dbl(X)
dbl(active(X)) → dbl(X)
first(mark(X1), X2) → first(X1, X2)
first(X1, mark(X2)) → first(X1, X2)
first(active(X1), X2) → first(X1, X2)
first(X1, active(X2)) → first(X1, X2)