Termination w.r.t. Q of the given QTRS could not be shown:

(0) Obligation:

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

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

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

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

ADD(s(X), Y) → ADD(X, Y)
FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)
FROM(X) → FROM(s(X))

The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs.

(6) Complex Obligation (AND)

(7) Obligation:

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

FROM(X) → FROM(s(X))

The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

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

(8) Obligation:

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

FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)

The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

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

(9) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

FIRST(s(X), cons(Y, Z)) → FIRST(X, Z)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
FIRST(x1, x2)  =  x1
s(x1)  =  s(x1)
cons(x1, x2)  =  x1
and(x1, x2)  =  and(x1, x2)
true  =  true
false  =  false
if(x1, x2, x3)  =  if(x1, x2, x3)
add(x1, x2)  =  add(x1, x2)
0  =  0
first(x1, x2)  =  first(x1, x2)
nil  =  nil
from(x1)  =  x1

Lexicographic path order with status [LPO].
Precedence:

and₂ > false
true > false
if₃ > false
add₂ > s₁ > false
0 > nil > false
first₂ > nil > false

Status:

add₂: [2,1]
if₃: [1,2,3]
true: []
false: []
s₁: [1]
and₂: [1,2]
0: []
first₂: [1,2]
nil: []

The following usable rules [FROCOS05] were oriented:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

(10) Obligation:

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

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

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

(11) PisEmptyProof (EQUIVALENT transformation)

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

(12) TRUE

(13) Obligation:

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

ADD(s(X), Y) → ADD(X, Y)

The TRS R consists of the following rules:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

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

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ADD(s(X), Y) → ADD(X, Y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
ADD(x1, x2)  =  ADD(x1)
s(x1)  =  s(x1)
and(x1, x2)  =  and(x1, x2)
true  =  true
false  =  false
if(x1, x2, x3)  =  if(x2, x3)
add(x1, x2)  =  add(x1, x2)
0  =  0
first(x1, x2)  =  first(x1)
nil  =  nil
cons(x1, x2)  =  cons
from(x1)  =  from

Lexicographic path order with status [LPO].
Precedence:

and₂ > false > ADD₁
true > ADD₁
if₂ > ADD₁
add₂ > s₁ > first₁ > nil > ADD₁
add₂ > s₁ > first₁ > cons > ADD₁
0 > nil > ADD₁
from > cons > ADD₁

Status:

if₂: [1,2]
true: []
and₂: [1,2]
ADD₁: [1]
0: []
from: []
add₂: [1,2]
cons: []
false: []
s₁: [1]
first₁: [1]
nil: []

The following usable rules [FROCOS05] were oriented:

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

(15) Obligation:

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

and(true, X) → X
and(false, Y) → false
if(true, X, Y) → X
if(false, X, Y) → Y
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))
from(X) → cons(X, from(s(X)))

The set Q consists of the following terms:

and(true, x0)
and(false, x0)
if(true, x0, x1)
if(false, x0, x1)
add(0, x0)
add(s(x0), x1)
first(0, x0)
first(s(x0), cons(x1, x2))
from(x0)

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

(16) PisEmptyProof (EQUIVALENT transformation)

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

(17) TRUE