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

(0) Obligation:

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

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

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:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

(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:

APPEND(cons(y, ys), x) → APPEND(ys, x)
P(s(s(x))) → P(s(x))
INC(s(x)) → INC(x)
ADDLISTS(xs, ys, zs) → IF(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
ADDLISTS(xs, ys, zs) → ISEMPTY(xs)
ADDLISTS(xs, ys, zs) → ISEMPTY(ys)
ADDLISTS(xs, ys, zs) → ISZERO(head(xs))
ADDLISTS(xs, ys, zs) → HEAD(xs)
ADDLISTS(xs, ys, zs) → TAIL(xs)
ADDLISTS(xs, ys, zs) → TAIL(ys)
ADDLISTS(xs, ys, zs) → P(head(xs))
ADDLISTS(xs, ys, zs) → INC(head(ys))
ADDLISTS(xs, ys, zs) → HEAD(ys)
ADDLISTS(xs, ys, zs) → APPEND(zs, head(ys))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLIST(xs, ys) → ADDLISTS(xs, ys, nil)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

INC(s(x)) → INC(x)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

INC(s(x)) → INC(x)

R is empty.
The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(10) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

(11) Obligation:

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

INC(s(x)) → INC(x)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• INC(s(x)) → INC(x)
  The graph contains the following edges 1 > 1

(13) TRUE

(14) Obligation:

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

P(s(s(x))) → P(s(x))

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(16) Obligation:

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

P(s(s(x))) → P(s(x))

R is empty.
The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(17) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

(18) Obligation:

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

P(s(s(x))) → P(s(x))

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• P(s(s(x))) → P(s(x))
  The graph contains the following edges 1 > 1

(20) TRUE

(21) Obligation:

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

APPEND(cons(y, ys), x) → APPEND(ys, x)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(23) Obligation:

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

APPEND(cons(y, ys), x) → APPEND(ys, x)

R is empty.
The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(24) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

(25) Obligation:

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

APPEND(cons(y, ys), x) → APPEND(ys, x)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• APPEND(cons(y, ys), x) → APPEND(ys, x)
  The graph contains the following edges 1 > 1, 2 >= 2

(27) TRUE

(28) Obligation:

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

ADDLISTS(xs, ys, zs) → IF(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
isZero(0) → true
isZero(s(x)) → false
head(cons(x, xs)) → x
tail(cons(x, xs)) → xs
tail(nil) → nil
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
addLists(xs, ys, zs) → if(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
if(true, true, b, xs, ys, xs2, ys2, zs, zs2) → zs
if(true, false, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, true, b, xs, ys, xs2, ys2, zs, zs2) → differentLengthError
if(false, false, false, xs, ys, xs2, ys2, zs, zs2) → addLists(xs2, ys2, zs)
if(false, false, true, xs, ys, xs2, ys2, zs, zs2) → addLists(xs, ys, zs2)
addList(xs, ys) → addLists(xs, ys, nil)

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(29) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(30) Obligation:

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

ADDLISTS(xs, ys, zs) → IF(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)
addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

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

(31) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

addLists(x0, x1, x2)
if(true, true, x0, x1, x2, x3, x4, x5, x6)
if(true, false, x0, x1, x2, x3, x4, x5, x6)
if(false, true, x0, x1, x2, x3, x4, x5, x6)
if(false, false, false, x0, x1, x2, x3, x4, x5)
if(false, false, true, x0, x1, x2, x3, x4, x5)
addList(x0, x1)

(32) Obligation:

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

ADDLISTS(xs, ys, zs) → IF(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(33) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs) we obtained the following new rules [LPAR04]:

IF(false, false, false, y_4, y_5, cons(y_7, y_8), cons(y_10, y_11), z2, y_13) → ADDLISTS(cons(y_7, y_8), cons(y_10, y_11), z2)

(34) Obligation:

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

ADDLISTS(xs, ys, zs) → IF(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys)))
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
IF(false, false, false, y_4, y_5, cons(y_7, y_8), cons(y_10, y_11), z2, y_13) → ADDLISTS(cons(y_7, y_8), cons(y_10, y_11), z2)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(35) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ADDLISTS(xs, ys, zs) → IF(isEmpty(xs), isEmpty(ys), isZero(head(xs)), tail(xs), tail(ys), cons(p(head(xs)), tail(xs)), cons(inc(head(ys)), tail(ys)), zs, append(zs, head(ys))) at position [0] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(head(cons(x0, x1))), tail(cons(x0, x1)), tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))
ADDLISTS(nil, y1, y2) → IF(true, isEmpty(y1), isZero(head(nil)), tail(nil), tail(y1), cons(p(head(nil)), tail(nil)), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

(36) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(head(cons(x0, x1))), tail(cons(x0, x1)), tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))
ADDLISTS(nil, y1, y2) → IF(true, isEmpty(y1), isZero(head(nil)), tail(nil), tail(y1), cons(p(head(nil)), tail(nil)), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(37) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(38) Obligation:

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

ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(head(cons(x0, x1))), tail(cons(x0, x1)), tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(39) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(head(cons(x0, x1))), tail(cons(x0, x1)), tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1))) at position [2,0] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), tail(cons(x0, x1)), tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

(40) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), tail(cons(x0, x1)), tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(41) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), tail(cons(x0, x1)), tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1))) at position [3] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

(42) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(43) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(head(cons(x0, x1))), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1))) at position [5,0,0] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(x0), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

(44) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(x0), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(45) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(x0), tail(cons(x0, x1))), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1))) at position [5,1] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(x0), x1), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

(46) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(x0), x1), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1)))

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(47) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ADDLISTS(cons(x0, x1), y1, y2) → IF(false, isEmpty(y1), isZero(x0), x1, tail(y1), cons(p(x0), x1), cons(inc(head(y1)), tail(y1)), y2, append(y2, head(y1))) at position [1] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, tail(cons(x0, x1)), cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))
ADDLISTS(cons(y0, y1), nil, y3) → IF(false, true, isZero(y0), y1, tail(nil), cons(p(y0), y1), cons(inc(head(nil)), tail(nil)), y3, append(y3, head(nil)))

(48) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, tail(cons(x0, x1)), cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))
ADDLISTS(cons(y0, y1), nil, y3) → IF(false, true, isZero(y0), y1, tail(nil), cons(p(y0), y1), cons(inc(head(nil)), tail(nil)), y3, append(y3, head(nil)))

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(49) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(50) Obligation:

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

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, tail(cons(x0, x1)), cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)

The TRS R consists of the following rules:

isEmpty(cons(x, xs)) → false
isEmpty(nil) → true
head(cons(x, xs)) → x
isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
tail(nil) → nil
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(51) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(52) Obligation:

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

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, tail(cons(x0, x1)), cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
head(cons(x, xs)) → x
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isEmpty(cons(x0, x1))
isEmpty(nil)
isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(53) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

isEmpty(cons(x0, x1))
isEmpty(nil)

(54) Obligation:

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

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, tail(cons(x0, x1)), cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
head(cons(x, xs)) → x
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(55) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, tail(cons(x0, x1)), cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1)))) at position [4] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))

(56) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
head(cons(x, xs)) → x
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(57) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(head(cons(x0, x1))), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1)))) at position [6,0,0] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))

(58) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1))))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
head(cons(x, xs)) → x
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(59) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), tail(cons(x0, x1))), y3, append(y3, head(cons(x0, x1)))) at position [6,1] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, head(cons(x0, x1))))

(60) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, head(cons(x0, x1))))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
tail(cons(x, xs)) → xs
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
head(cons(x, xs)) → x
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(61) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(62) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, head(cons(x0, x1))))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
head(cons(x, xs)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
tail(cons(x0, x1))
tail(nil)
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(63) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

tail(cons(x0, x1))
tail(nil)

(64) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, head(cons(x0, x1))))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
head(cons(x, xs)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(65) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, head(cons(x0, x1)))) at position [8,1] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, x0))

(66) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, x0))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
head(cons(x, xs)) → x
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(67) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(68) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, x0))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
head(cons(x0, x1))
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(69) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

head(cons(x0, x1))

(70) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, x0))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(71) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ADDLISTS(cons(y0, y1), cons(x0, x1), y3) → IF(false, false, isZero(y0), y1, x1, cons(p(y0), y1), cons(inc(x0), x1), y3, append(y3, x0)) at position [2] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(p(0), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))

(72) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(p(0), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))

The TRS R consists of the following rules:

isZero(0) → true
isZero(s(x)) → false
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
p(0) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(73) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(74) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(p(0), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))

The TRS R consists of the following rules:

p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(0) → 0

The set Q consists of the following terms:

isZero(0)
isZero(s(x0))
append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(75) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

isZero(0)
isZero(s(x0))

(76) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(p(0), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))

The TRS R consists of the following rules:

p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(0) → 0

The set Q consists of the following terms:

append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(77) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(p(0), y1), cons(inc(y2), y3), y4, append(y4, y2)) at position [5,0] we obtained the following new rules [LPAR04]:

ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(0, y1), cons(inc(y2), y3), y4, append(y4, y2))

(78) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(0, y1), cons(inc(y2), y3), y4, append(y4, y2))

The TRS R consists of the following rules:

p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0
inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(0) → 0

The set Q consists of the following terms:

append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(79) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(80) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2)
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(0, y1), cons(inc(y2), y3), y4, append(y4, y2))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0

The set Q consists of the following terms:

append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(81) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule IF(false, false, true, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs, ys, zs2) we obtained the following new rules [LPAR04]:

IF(false, false, true, z0, z2, cons(0, z0), cons(y_0, z2), z3, y_1) → ADDLISTS(z0, z2, y_1)

(82) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(0, y1), cons(inc(y2), y3), y4, append(y4, y2))
IF(false, false, true, z0, z2, cons(0, z0), cons(y_0, z2), z3, y_1) → ADDLISTS(z0, z2, y_1)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0

The set Q consists of the following terms:

append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(83) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

IF(false, false, true, z0, z2, cons(0, z0), cons(y_0, z2), z3, y_1) → ADDLISTS(z0, z2, y_1)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 1   
POL(ADDLISTS(x₁, x₂, x₃)) = x₁   
POL(IF(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉)) = x₆   
POL(append(x₁, x₂)) = 0   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(false) = 0   
POL(inc(x₁)) = 0   
POL(nil) = 0   
POL(p(x₁)) = x₁   
POL(s(x₁)) = x₁   
POL(true) = 0   

The following usable rules [FROCOS05] were oriented:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

(84) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))
ADDLISTS(cons(0, y1), cons(y2, y3), y4) → IF(false, false, true, y1, y3, cons(0, y1), cons(inc(y2), y3), y4, append(y4, y2))

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0

The set Q consists of the following terms:

append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(85) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(86) Obligation:

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

ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))
IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0

The set Q consists of the following terms:

append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(87) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ADDLISTS(cons(s(x0), y1), cons(y2, y3), y4) → IF(false, false, false, y1, y3, cons(p(s(x0)), y1), cons(inc(y2), y3), y4, append(y4, y2))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(ADDLISTS(x1, x2, x3)) =

/ 1 \ \ 0 /

+

/ 0 1 \ \ 0 1 /

·

x1

+

/ 0 0 \ \ 0 0 /

·

x2

+

/ 1 1 \ \ 0 0 /

·

x3

POL(cons(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

+

/ 0 0 \ \ 0 1 /

·

x2

POL(s(x1)) =

/ 1 \ \ 0 /

+

/ 1 0 \ \ 1 0 /

·

x1

POL(IF(x1, x2, x3, x4, x5, x6, x7, x8, x9)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 0 0 /

·

x2

+

/ 1 0 \ \ 0 0 /

·

x3

+

/ 0 0 \ \ 0 0 /

·

x4

+

/ 0 0 \ \ 0 0 /

·

x5

+

/ 0 1 \ \ 1 1 /

·

x6

+

/ 0 0 \ \ 0 0 /

·

x7

+

/ 1 1 \ \ 0 0 /

·

x8

+

/ 0 0 \ \ 0 0 /

·

x9

POL(false) =

/ 1 \ \ 0 /

POL(p(x1)) =

/ 0 \ \ 0 /

+

/ 0 1 \ \ 0 1 /

·

x1

POL(inc(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

POL(append(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

+

/ 0 1 \ \ 0 0 /

·

x2

POL(nil) =

/ 0 \ \ 0 /

POL(0) =

/ 0 \ \ 0 /

The following usable rules [FROCOS05] were oriented:

p(s(0)) → 0
p(s(s(x))) → s(p(s(x)))

(88) Obligation:

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

IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)

The TRS R consists of the following rules:

inc(s(x)) → s(inc(x))
inc(0) → s(0)
append(nil, x) → cons(x, nil)
append(cons(y, ys), x) → cons(y, append(ys, x))
p(s(s(x))) → s(p(s(x)))
p(s(0)) → 0

The set Q consists of the following terms:

append(nil, x0)
append(cons(x0, x1), x2)
p(s(s(x0)))
p(s(0))
p(0)
inc(s(x0))
inc(0)

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

(89) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(90) TRUE