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

(0) Obligation:

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

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

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

(2) Obligation:

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

APP(cons(x, l), k) → APP(l, k)
SUM(cons(x, cons(y, l))) → SUM(cons(plus(x, y), l))
SUM(cons(x, cons(y, l))) → PLUS(x, y)
SUM(app(l, cons(x, cons(y, k)))) → SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) → APP(l, sum(cons(x, cons(y, k))))
SUM(app(l, cons(x, cons(y, k)))) → SUM(cons(x, cons(y, k)))
PLUS(s(x), y) → PLUS(x, y)
SUM(plus(cons(0, x), cons(y, l))) → PRED(sum(cons(s(x), cons(y, l))))
SUM(plus(cons(0, x), cons(y, l))) → SUM(cons(s(x), cons(y, l)))

The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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

(3) DependencyGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

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

PLUS(s(x), y) → PLUS(x, y)

The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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

(6) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PLUS(s(x), y) → PLUS(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
PLUS(x1, x2)  =  x1
s(x1)  =  s(x1)

Recursive Path Order [RPO].
Precedence:

trivial

The following usable rules [FROCOS05] were oriented: none

(7) Obligation:

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

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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

(8) PisEmptyProof (EQUIVALENT transformation)

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

(9) TRUE

(10) Obligation:

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

APP(cons(x, l), k) → APP(l, k)

The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

APP(cons(x, l), k) → APP(l, k)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
APP(x1, x2)  =  APP(x1)
cons(x1, x2)  =  cons(x2)

Recursive Path Order [RPO].
Precedence:

cons₁ > APP₁

The following usable rules [FROCOS05] were oriented: none

(12) Obligation:

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

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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

(13) PisEmptyProof (EQUIVALENT transformation)

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

(14) TRUE

(15) Obligation:

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

SUM(cons(x, cons(y, l))) → SUM(cons(plus(x, y), l))

The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

SUM(cons(x, cons(y, l))) → SUM(cons(plus(x, y), l))

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
SUM(x1)  =  SUM(x1)
cons(x1, x2)  =  cons(x2)
plus(x1, x2)  =  plus(x2)
s(x1)  =  x1
0  =  0

Recursive Path Order [RPO].
Precedence:

cons₁ > SUM₁
cons₁ > plus₁

The following usable rules [FROCOS05] were oriented: none

(17) Obligation:

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

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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

(18) PisEmptyProof (EQUIVALENT transformation)

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

(19) TRUE

(20) Obligation:

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

SUM(app(l, cons(x, cons(y, k)))) → SUM(app(l, sum(cons(x, cons(y, k)))))

The TRS R consists of the following rules:

app(nil, k) → k
app(l, nil) → l
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
sum(plus(cons(0, x), cons(y, l))) → pred(sum(cons(s(x), cons(y, l))))
pred(cons(s(x), nil)) → cons(x, nil)

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