Termination w.r.t. Q proof of /tmp/tmpYugWXs/addList.trs

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

0 QTRS

↳1 Overlay + Local Confluence (⇔)

↳2 QTRS

↳3 DependencyPairsProof (⇔)

↳4 QDP

↳5 DependencyGraphProof (⇔)

↳6 AND

  ↳7 QDP

  ↳8 QDP

  ↳9 QDP

  ↳10 QDP

(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) 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.

(9) 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.

(10) 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.