(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)
ACTIVE(half(0)) → MARK(0)
ACTIVE(half(s(0))) → MARK(0)
ACTIVE(half(s(s(X)))) → MARK(s(half(X)))
ACTIVE(half(s(s(X)))) → S(half(X))
ACTIVE(half(s(s(X)))) → HALF(X)
ACTIVE(half(dbl(X))) → MARK(X)
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(mark(X)))
MARK(s(X)) → S(mark(X))
MARK(s(X)) → MARK(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)
MARK(half(X)) → ACTIVE(half(mark(X)))
MARK(half(X)) → HALF(mark(X))
MARK(half(X)) → MARK(X)
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)
HALF(mark(X)) → HALF(X)
HALF(active(X)) → HALF(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 10 SCCs with 34 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HALF(active(X)) → HALF(X)
HALF(mark(X)) → HALF(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


HALF(active(X)) → HALF(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
HALF(x1)  =  x1
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

HALF(mark(X)) → HALF(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


HALF(mark(X)) → HALF(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
HALF(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(9) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(11) TRUE

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


FIRST(X1, mark(X2)) → FIRST(X1, X2)
FIRST(X1, active(X2)) → FIRST(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
FIRST(x1, x2)  =  FIRST(x2)
mark(x1)  =  mark(x1)
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
[FIRST1, active1]

Status:
FIRST1: [1]
mark1: [1]
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FIRST(mark(X1), X2) → FIRST(X1, X2)
FIRST(active(X1), X2) → FIRST(X1, X2)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


FIRST(mark(X1), X2) → FIRST(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
FIRST(x1, x2)  =  x1
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

FIRST(active(X1), X2) → FIRST(X1, X2)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(17) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


FIRST(active(X1), X2) → FIRST(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
FIRST(x1, x2)  =  x1
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(18) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(19) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(20) TRUE

(21) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DBL(active(X)) → DBL(X)
DBL(mark(X)) → DBL(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


DBL(active(X)) → DBL(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
DBL(x1)  =  x1
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(23) Obligation:

Q DP problem:
The TRS P consists of the following rules:

DBL(mark(X)) → DBL(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(24) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


DBL(mark(X)) → DBL(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
DBL(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(25) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(26) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(27) TRUE

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ADD(X1, mark(X2)) → ADD(X1, X2)
ADD(X1, active(X2)) → ADD(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ADD(x1, x2)  =  ADD(x2)
mark(x1)  =  mark(x1)
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
[ADD1, active1]

Status:
ADD1: [1]
mark1: [1]
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADD(mark(X1), X2) → ADD(X1, X2)
ADD(active(X1), X2) → ADD(X1, X2)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(31) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ADD(mark(X1), X2) → ADD(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ADD(x1, x2)  =  x1
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ADD(active(X1), X2) → ADD(X1, X2)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(33) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


ADD(active(X1), X2) → ADD(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ADD(x1, x2)  =  x1
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(34) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(35) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(36) TRUE

(37) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(active(X)) → S(X)
S(mark(X)) → S(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


S(active(X)) → S(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
S(x1)  =  x1
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S(mark(X)) → S(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


S(mark(X)) → S(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
S(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(41) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(42) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(43) TRUE

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SQR(active(X)) → SQR(X)
SQR(mark(X)) → SQR(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


SQR(active(X)) → SQR(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
SQR(x1)  =  x1
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SQR(mark(X)) → SQR(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(47) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


SQR(mark(X)) → SQR(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
SQR(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(48) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(49) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(50) TRUE

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

RECIP(active(X)) → RECIP(X)
RECIP(mark(X)) → RECIP(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(52) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


RECIP(active(X)) → RECIP(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
RECIP(x1)  =  x1
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

RECIP(mark(X)) → RECIP(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


RECIP(mark(X)) → RECIP(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
RECIP(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(55) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(56) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(57) TRUE

(58) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(59) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CONS(x1, x2)  =  CONS(x2)
mark(x1)  =  mark(x1)
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
[CONS1, active1]

Status:
CONS1: [1]
mark1: [1]
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(61) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CONS(mark(X1), X2) → CONS(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CONS(x1, x2)  =  x1
mark(x1)  =  mark(x1)
active(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

CONS(active(X1), X2) → CONS(X1, X2)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(63) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


CONS(active(X1), X2) → CONS(X1, X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
CONS(x1, x2)  =  x1
active(x1)  =  active(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(64) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(65) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(66) TRUE

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TERMS(active(X)) → TERMS(X)
TERMS(mark(X)) → TERMS(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(68) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TERMS(active(X)) → TERMS(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
TERMS(x1)  =  x1
active(x1)  =  active(x1)
mark(x1)  =  x1

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
active1: [1]


The following usable rules [FROCOS05] were oriented: none

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TERMS(mark(X)) → TERMS(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(70) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


TERMS(mark(X)) → TERMS(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
TERMS(x1)  =  x1
mark(x1)  =  mark(x1)

Lexicographic path order with status [LPO].
Quasi-Precedence:
trivial

Status:
mark1: [1]


The following usable rules [FROCOS05] were oriented: none

(71) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(72) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(73) TRUE

(74) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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(mark(X)))
ACTIVE(add(s(X), Y)) → MARK(s(add(X, Y)))
MARK(s(X)) → MARK(X)
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)))
ACTIVE(half(s(s(X)))) → MARK(s(half(X)))
MARK(dbl(X)) → MARK(X)
MARK(first(X1, X2)) → ACTIVE(first(mark(X1), mark(X2)))
ACTIVE(half(dbl(X))) → MARK(X)
MARK(first(X1, X2)) → MARK(X1)
MARK(first(X1, X2)) → MARK(X2)
MARK(half(X)) → ACTIVE(half(mark(X)))
MARK(half(X)) → MARK(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(75) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(terms(X)) → MARK(X)
ACTIVE(sqr(s(X))) → MARK(s(add(sqr(X), dbl(X))))
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)))
MARK(s(X)) → MARK(X)
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)
ACTIVE(half(s(s(X)))) → MARK(s(half(X)))
MARK(dbl(X)) → MARK(X)
ACTIVE(half(dbl(X))) → MARK(X)
MARK(first(X1, X2)) → MARK(X1)
MARK(first(X1, X2)) → MARK(X2)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK(x1)
terms(x1)  =  terms(x1)
ACTIVE(x1)  =  ACTIVE(x1)
mark(x1)  =  x1
cons(x1, x2)  =  x1
recip(x1)  =  x1
sqr(x1)  =  sqr(x1)
s(x1)  =  s(x1)
add(x1, x2)  =  add(x1, x2)
dbl(x1)  =  dbl(x1)
0  =  0
first(x1, x2)  =  first(x1, x2)
half(x1)  =  x1
active(x1)  =  x1
nil  =  nil

Lexicographic path order with status [LPO].
Quasi-Precedence:
[terms1, sqr1] > add2 > s1 > [MARK1, ACTIVE1, first2, nil]
[terms1, sqr1] > dbl1 > s1 > [MARK1, ACTIVE1, first2, nil]
[terms1, sqr1] > dbl1 > 0 > [MARK1, ACTIVE1, first2, nil]

Status:
MARK1: [1]
terms1: [1]
ACTIVE1: [1]
sqr1: [1]
s1: [1]
add2: [1,2]
dbl1: [1]
0: []
first2: [2,1]
nil: []


The following usable rules [FROCOS05] were oriented:

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(mark(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)))
active(half(s(s(X)))) → mark(s(half(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
active(half(dbl(X))) → mark(X)
mark(half(X)) → active(half(mark(X)))
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)
half(active(X)) → half(X)
half(mark(X)) → half(X)
active(sqr(0)) → mark(0)
active(dbl(0)) → mark(0)
active(first(0, X)) → mark(nil)
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)

(76) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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))
MARK(cons(X1, X2)) → MARK(X1)
MARK(recip(X)) → ACTIVE(recip(mark(X)))
MARK(recip(X)) → MARK(X)
MARK(sqr(X)) → ACTIVE(sqr(mark(X)))
MARK(s(X)) → ACTIVE(s(mark(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)))
MARK(half(X)) → ACTIVE(half(mark(X)))
MARK(half(X)) → MARK(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(77) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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(mark(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)))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK
terms(x1)  =  terms
ACTIVE(x1)  =  x1
mark(x1)  =  mark(x1)
cons(x1, x2)  =  cons
recip(x1)  =  recip
sqr(x1)  =  sqr
s(x1)  =  s
add(x1, x2)  =  add
dbl(x1)  =  dbl
first(x1, x2)  =  first
half(x1)  =  half
active(x1)  =  active(x1)
0  =  0
nil  =  nil

Lexicographic path order with status [LPO].
Quasi-Precedence:
[MARK, terms, half] > [mark1, cons, recip, sqr, s, add, dbl, first, active1, nil]
0 > [mark1, cons, recip, sqr, s, add, dbl, first, active1, nil]

Status:
MARK: []
terms: []
mark1: [1]
cons: []
recip: []
sqr: []
s: []
add: []
dbl: []
first: []
half: []
active1: [1]
0: []
nil: []


The following usable rules [FROCOS05] were oriented:

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)
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)
dbl(active(X)) → dbl(X)
dbl(mark(X)) → dbl(X)
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)
half(active(X)) → half(X)
half(mark(X)) → half(X)

(78) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MARK(terms(X)) → ACTIVE(terms(mark(X)))
ACTIVE(terms(N)) → MARK(cons(recip(sqr(N)), terms(s(N))))
MARK(cons(X1, X2)) → MARK(X1)
MARK(recip(X)) → MARK(X)
MARK(half(X)) → ACTIVE(half(mark(X)))
MARK(half(X)) → MARK(X)

The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(79) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MARK(terms(X)) → ACTIVE(terms(mark(X)))
ACTIVE(terms(N)) → MARK(cons(recip(sqr(N)), terms(s(N))))
MARK(cons(X1, X2)) → MARK(X1)
MARK(recip(X)) → MARK(X)
MARK(half(X)) → ACTIVE(half(mark(X)))
MARK(half(X)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
MARK(x1)  =  MARK(x1)
terms(x1)  =  terms(x1)
ACTIVE(x1)  =  x1
mark(x1)  =  x1
cons(x1, x2)  =  cons(x1)
recip(x1)  =  recip(x1)
sqr(x1)  =  sqr(x1)
s(x1)  =  x1
half(x1)  =  half(x1)
active(x1)  =  x1
add(x1, x2)  =  add(x2)
dbl(x1)  =  dbl(x1)
0  =  0
first(x1, x2)  =  x2
nil  =  nil

Lexicographic path order with status [LPO].
Quasi-Precedence:
terms1 > sqr1 > [MARK1, cons1, recip1, add1, dbl1, nil]
half1 > [MARK1, cons1, recip1, add1, dbl1, nil]
0 > [MARK1, cons1, recip1, add1, dbl1, nil]

Status:
MARK1: [1]
terms1: [1]
cons1: [1]
recip1: [1]
sqr1: [1]
half1: [1]
add1: [1]
dbl1: [1]
0: []
nil: []


The following usable rules [FROCOS05] were oriented:

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(mark(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)))
active(half(s(s(X)))) → mark(s(half(X)))
mark(first(X1, X2)) → active(first(mark(X1), mark(X2)))
active(half(dbl(X))) → mark(X)
mark(half(X)) → active(half(mark(X)))
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)
half(active(X)) → half(X)
half(mark(X)) → half(X)
active(sqr(0)) → mark(0)
active(dbl(0)) → mark(0)
active(first(0, X)) → mark(nil)
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
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)

(80) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)))
active(half(0)) → mark(0)
active(half(s(0))) → mark(0)
active(half(s(s(X)))) → mark(s(half(X)))
active(half(dbl(X))) → mark(X)
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(mark(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)
mark(half(X)) → active(half(mark(X)))
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)
half(mark(X)) → half(X)
half(active(X)) → half(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(81) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(82) TRUE