YES Termination w.r.t. Q proof of Secret_06_TRS_addList.ari

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

0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 QDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 QReductionProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 QDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 QDP
        ↳17 QReductionProof (⇔, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 QDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 QReductionProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 QDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 QDP
        ↳31 QReductionProof (⇔, 0 ms)
        ↳32 QDP
        ↳33 TransformationProof (⇔, 0 ms)
        ↳34 QDP
        ↳35 DependencyGraphProof (⇔, 0 ms)
        ↳36 QDP
        ↳37 TransformationProof (⇔, 0 ms)
        ↳38 QDP
        ↳39 TransformationProof (⇔, 0 ms)
        ↳40 QDP
        ↳41 TransformationProof (⇔, 0 ms)
        ↳42 QDP
        ↳43 TransformationProof (⇔, 0 ms)
        ↳44 QDP
        ↳45 TransformationProof (⇔, 3 ms)
        ↳46 QDP
        ↳47 DependencyGraphProof (⇔, 0 ms)
        ↳48 QDP
        ↳49 UsableRulesProof (⇔, 0 ms)
        ↳50 QDP
        ↳51 QReductionProof (⇔, 0 ms)
        ↳52 QDP
        ↳53 TransformationProof (⇔, 0 ms)
        ↳54 QDP
        ↳55 TransformationProof (⇔, 0 ms)
        ↳56 QDP
        ↳57 TransformationProof (⇔, 0 ms)
        ↳58 QDP
        ↳59 UsableRulesProof (⇔, 0 ms)
        ↳60 QDP
        ↳61 QReductionProof (⇔, 0 ms)
        ↳62 QDP
        ↳63 TransformationProof (⇔, 0 ms)
        ↳64 QDP
        ↳65 UsableRulesProof (⇔, 0 ms)
        ↳66 QDP
        ↳67 QReductionProof (⇔, 0 ms)
        ↳68 QDP
        ↳69 TransformationProof (⇔, 0 ms)
        ↳70 QDP
        ↳71 UsableRulesProof (⇔, 0 ms)
        ↳72 QDP
        ↳73 QReductionProof (⇔, 0 ms)
        ↳74 QDP
        ↳75 TransformationProof (⇔, 0 ms)
        ↳76 QDP
        ↳77 UsableRulesProof (⇔, 0 ms)
        ↳78 QDP
        ↳79 TransformationProof (⇔, 0 ms)
        ↳80 QDP
        ↳81 QDPOrderProof (⇔, 0 ms)
        ↳82 QDP
        ↳83 DependencyGraphProof (⇔, 0 ms)
        ↳84 QDP
        ↳85 QDPOrderProof (⇔, 5 ms)
        ↳86 QDP
        ↳87 DependencyGraphProof (⇔, 0 ms)
        ↳88 TRUE

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

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

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

(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) TransformationProof (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(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))) → 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)))

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

(35) DependencyGraphProof (EQUIVALENT transformation)

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

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

(37) TransformationProof (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))) → 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)))

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

(39) TransformationProof (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))) → 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)))

(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), 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) TransformationProof (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))) → 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)))

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

(43) TransformationProof (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))) → 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)))

(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), 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) TransformationProof (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), 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))) → 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)))

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

(47) DependencyGraphProof (EQUIVALENT transformation)

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

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

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

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

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.

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

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

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) TransformationProof (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)))) → 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))))

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

(55) TransformationProof (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)))) → 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))))

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

(57) TransformationProof (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)))) → 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))))

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

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

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

(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))
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) TransformationProof (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)) → 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))

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

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

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

(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))
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) TransformationProof (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(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)) → 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))

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

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

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

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.

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

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

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) TransformationProof (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)) → 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))

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

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

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

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.

(79) TransformationProof (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) → IF(false, false, true, z0, z2, cons(0, z0), cons(y_0, z2), z3, y_1) → ADDLISTS(z0, z2, y_1)

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

(81) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


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: Combined order from the following AFS and order.
IF(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  x7
ADDLISTS(x1, x2, x3)  =  x2
cons(x1, x2)  =  cons(x2)

Knuth-Bendix order [KBO] with precedence:
trivial

and weight map:

dummyConstant=1
cons_1=1

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

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

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) DependencyGraphProof (EQUIVALENT transformation)

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

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

(85) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


IF(false, false, false, xs, ys, xs2, ys2, zs, zs2) → ADDLISTS(xs2, ys2, zs)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( IF(x1, ..., x9) ) = x1 + x2 + 2x6 + 2

POL( cons(x1, x2) ) = x1

POL( p(x1) ) = max{0, x1 - 1}

POL( s(x1) ) = x1 + 1

POL( 0 ) = 2

POL( inc(x1) ) = 0

POL( append(x1, x2) ) = 0

POL( nil ) = 1

POL( ADDLISTS(x1, ..., x3) ) = 2x1 + 2

POL( false ) = 1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

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

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

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) DependencyGraphProof (EQUIVALENT transformation)

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

(88) TRUE