YES
Termination w.r.t. Q proof of ../tpdb/TRS/AG01/#3.17.trs
Termination w.r.t. Q of the following Term Rewriting System could be proven:
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.
↳ QTRS
↳ RRRPoloQTRSProof
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.
The following Q TRS is given: 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.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:
app(nil, k) → k
app(l, nil) → l
Used ordering:
Polynomial interpretation [25]:
POL(0) = 0
POL(app(x1, x2)) = 1 + 2·x1 + 2·x2
POL(cons(x1, x2)) = x1 + x2
POL(nil) = 0
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
POL(sum(x1)) = x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
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(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.
The following Q TRS is given: 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(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.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:
plus(0, y) → y
Used ordering:
Polynomial interpretation [25]:
POL(0) = 2
POL(app(x1, x2)) = x1 + 2·x2
POL(cons(x1, x2)) = x1 + x2
POL(nil) = 0
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
POL(sum(x1)) = x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
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(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(s(x), y) → s(plus(x, y))
Q is empty.
The following Q TRS is given: 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(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(s(x), y) → s(plus(x, y))
Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:
app(cons(x, l), k) → cons(x, app(l, k))
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l))
Used ordering:
Polynomial interpretation [25]:
POL(app(x1, x2)) = 2 + 2·x1 + 2·x2
POL(cons(x1, x2)) = 1 + 2·x1 + x2
POL(nil) = 0
POL(plus(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(sum(x1)) = x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
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)))))
plus(s(x), y) → s(plus(x, y))
Q is empty.
The following Q TRS is given: 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)))))
plus(s(x), y) → s(plus(x, y))
Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:
plus(s(x), y) → s(plus(x, y))
Used ordering:
Polynomial interpretation [25]:
POL(app(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x1 + 2·x2
POL(nil) = 0
POL(plus(x1, x2)) = 2·x1 + 2·x2
POL(s(x1)) = 1 + x1
POL(sum(x1)) = x1
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ Overlay + Local Confluence
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.
The TRS is overlay and locally confluent. By [19] we can switch to innermost.
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
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))))
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
SUM(app(l, cons(x, cons(y, k)))) → SUM(cons(x, cons(y, k)))
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:
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.
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ RRRPoloQTRSProof
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
SUM(app(l, cons(x, cons(y, k)))) → SUM(cons(x, cons(y, k)))
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:
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.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 2 less nodes.