NO
0 QTRS
↳1 DependencyPairsProof (⇔, 0 ms)
↳2 QDP
↳3 DependencyGraphProof (⇔, 0 ms)
↳4 AND
↳5 QDP
↳6 MNOCProof (⇔, 0 ms)
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 MNOCProof (⇔, 0 ms)
↳16 QDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 QDP
↳19 QReductionProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 QDP
↳24 MNOCProof (⇔, 0 ms)
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 QReductionProof (⇔, 0 ms)
↳29 QDP
↳30 QDPSizeChangeProof (⇔, 0 ms)
↳31 YES
↳32 QDP
↳33 MNOCProof (⇔, 0 ms)
↳34 QDP
↳35 UsableRulesProof (⇔, 0 ms)
↳36 QDP
↳37 QReductionProof (⇔, 0 ms)
↳38 QDP
↳39 QDPSizeChangeProof (⇔, 0 ms)
↳40 YES
↳41 QDP
↳42 MNOCProof (⇔, 0 ms)
↳43 QDP
↳44 UsableRulesProof (⇔, 0 ms)
↳45 QDP
↳46 QReductionProof (⇔, 0 ms)
↳47 QDP
↳48 QDPSizeChangeProof (⇔, 0 ms)
↳49 YES
↳50 QDP
↳51 MNOCProof (⇔, 0 ms)
↳52 QDP
↳53 UsableRulesProof (⇔, 0 ms)
↳54 QDP
↳55 QReductionProof (⇔, 0 ms)
↳56 QDP
↳57 TransformationProof (⇔, 0 ms)
↳58 QDP
↳59 TransformationProof (⇔, 0 ms)
↳60 QDP
↳61 NonTerminationLoopProof (⇒, 0 ms)
↳62 NO
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
TERMS(N) → SQR(N)
TERMS(N) → TERMS(s(N))
SQR(s(X)) → ADD(sqr(X), dbl(X))
SQR(s(X)) → SQR(X)
SQR(s(X)) → DBL(X)
DBL(s(X)) → DBL(X)
ADD(s(X), Y) → ADD(X, Y)
FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
HALF(s(s(X))) → HALF(X)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
HALF(s(s(X))) → HALF(X)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
HALF(s(s(X))) → HALF(X)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
HALF(s(s(X))) → HALF(X)
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
HALF(s(s(X))) → HALF(X)
From the DPs we obtained the following set of size-change graphs:
FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
From the DPs we obtained the following set of size-change graphs:
ADD(s(X), Y) → ADD(X, Y)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
ADD(s(X), Y) → ADD(X, Y)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
ADD(s(X), Y) → ADD(X, Y)
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
ADD(s(X), Y) → ADD(X, Y)
From the DPs we obtained the following set of size-change graphs:
DBL(s(X)) → DBL(X)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
DBL(s(X)) → DBL(X)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
DBL(s(X)) → DBL(X)
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
DBL(s(X)) → DBL(X)
From the DPs we obtained the following set of size-change graphs:
SQR(s(X)) → SQR(X)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
SQR(s(X)) → SQR(X)
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
SQR(s(X)) → SQR(X)
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
SQR(s(X)) → SQR(X)
From the DPs we obtained the following set of size-change graphs:
TERMS(N) → TERMS(s(N))
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
TERMS(N) → TERMS(s(N))
terms(N) → cons(recip(sqr(N)), terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))
half(0) → 0
half(s(0)) → 0
half(s(s(X))) → s(half(X))
half(dbl(X)) → X
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
TERMS(N) → TERMS(s(N))
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
terms(x0)
sqr(0)
sqr(s(x0))
dbl(0)
dbl(s(x0))
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
half(0)
half(s(0))
half(s(s(x0)))
half(dbl(x0))
TERMS(N) → TERMS(s(N))
TERMS(s(z0)) → TERMS(s(s(z0))) → TERMS(s(z0)) → TERMS(s(s(z0)))
TERMS(s(z0)) → TERMS(s(s(z0)))
TERMS(s(s(z0))) → TERMS(s(s(s(z0)))) → TERMS(s(s(z0))) → TERMS(s(s(s(z0))))
TERMS(s(s(z0))) → TERMS(s(s(s(z0))))