(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))
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(0) = 1
POL(app(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = 1 + x1 + x2
POL(nil) = 0
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(sum(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
plus(0, y) → y
(2) 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(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(app(x1, x2)) = 1 + x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(nil) = 0
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(sum(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
app(nil, k) → k
app(l, nil) → l
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
plus(s(x), y) → s(plus(x, y))
Q is empty.
(5) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(app(x1, x2)) = 2·x1 + 2·x2
POL(cons(x1, x2)) = x1 + x2
POL(nil) = 0
POL(plus(x1, x2)) = 2 + 2·x1 + x2
POL(s(x1)) = 1 + x1
POL(sum(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
plus(s(x), y) → s(plus(x, y))
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
Q is empty.
(7) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(app(x1, x2)) = 2·x1 + x2
POL(cons(x1, x2)) = 2 + x1 + x2
POL(nil) = 0
POL(sum(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
app(cons(x, l), k) → cons(x, app(l, k))
(8) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
Q is empty.
(9) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(10) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
The set Q consists of the following terms:
sum(cons(x0, nil))
sum(app(x0, cons(x1, cons(x2, x3))))
(11) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(12) 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)))))
SUM(app(l, cons(x, cons(y, k)))) → SUM(cons(x, cons(y, k)))
The TRS R consists of the following rules:
sum(cons(x, nil)) → cons(x, nil)
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k)))))
The set Q consists of the following terms:
sum(cons(x0, nil))
sum(app(x0, cons(x1, cons(x2, x3))))
We have to consider all minimal (P,Q,R)-chains.
(13) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.
(14) TRUE