(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
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:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
(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:
MIN(s(x), s(y)) → MIN(x, y)
LEN(cons(x, xs)) → LEN(xs)
SUM(x, s(y)) → SUM(x, y)
LE(s(x), s(y)) → LE(x, y)
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
ADDLIST(x, y) → IF(le(0, min(len(x), len(y))), 0, x, y, nil)
ADDLIST(x, y) → LE(0, min(len(x), len(y)))
ADDLIST(x, y) → MIN(len(x), len(y))
ADDLIST(x, y) → LEN(x)
ADDLIST(x, y) → LEN(y)
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
IF(true, c, xs, ys, z) → LE(s(c), min(len(xs), len(ys)))
IF(true, c, xs, ys, z) → MIN(len(xs), len(ys))
IF(true, c, xs, ys, z) → LEN(xs)
IF(true, c, xs, ys, z) → LEN(ys)
IF(true, c, xs, ys, z) → SUM(take(c, xs), take(c, ys))
IF(true, c, xs, ys, z) → TAKE(c, xs)
IF(true, c, xs, ys, z) → TAKE(c, ys)
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 12 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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:
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
R is empty.
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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].
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
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:
- TAKE(s(x), cons(y, ys)) → TAKE(x, ys)
The graph contains the following edges 1 > 1, 2 > 2
(13) YES
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x), s(y)) → LE(x, y)
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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:
LE(s(x), s(y)) → LE(x, y)
R is empty.
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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].
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LE(s(x), s(y)) → LE(x, y)
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:
- LE(s(x), s(y)) → LE(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(20) YES
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM(x, s(y)) → SUM(x, y)
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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:
SUM(x, s(y)) → SUM(x, y)
R is empty.
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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].
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SUM(x, s(y)) → SUM(x, y)
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:
- SUM(x, s(y)) → SUM(x, y)
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:
LEN(cons(x, xs)) → LEN(xs)
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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:
LEN(cons(x, xs)) → LEN(xs)
R is empty.
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
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].
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LEN(cons(x, xs)) → LEN(xs)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) 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:
- LEN(cons(x, xs)) → LEN(xs)
The graph contains the following edges 1 > 1
(34) YES
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(s(x), s(y)) → MIN(x, y)
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
We have to consider all minimal (P,Q,R)-chains.
(36) 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.
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(s(x), s(y)) → MIN(x, y)
R is empty.
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
We have to consider all minimal (P,Q,R)-chains.
(38) 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].
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(s(x), s(y)) → MIN(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(40) 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:
- MIN(s(x), s(y)) → MIN(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(41) YES
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The TRS R consists of the following rules:
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
addList(x, y) → if(le(0, min(len(x), len(y))), 0, x, y, nil)
if(false, c, x, y, z) → z
if(true, c, xs, ys, z) → if(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
We have to consider all minimal (P,Q,R)-chains.
(43) 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.
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The TRS R consists of the following rules:
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
We have to consider all minimal (P,Q,R)-chains.
(45) 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].
addList(x0, x1)
if(false, x0, x1, x2, x3)
if(true, x0, x1, x2, x3)
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The TRS R consists of the following rules:
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(47) NonInfProof (EQUIVALENT transformation)
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that
final constraints are written in
bold face.
For Pair
IF(
true,
c,
xs,
ys,
z) →
IF(
le(
s(
c),
min(
len(
xs),
len(
ys))),
s(
c),
xs,
ys,
cons(
sum(
take(
c,
xs),
take(
c,
ys)),
z)) the following chains were created:
- We consider the chain IF(true, x0, x1, x2, x3) → IF(le(s(x0), min(len(x1), len(x2))), s(x0), x1, x2, cons(sum(take(x0, x1), take(x0, x2)), x3)), IF(true, x4, x5, x6, x7) → IF(le(s(x4), min(len(x5), len(x6))), s(x4), x5, x6, cons(sum(take(x4, x5), take(x4, x6)), x7)) which results in the following constraint:
| (1) (IF(le(s(x0), min(len(x1), len(x2))), s(x0), x1, x2, cons(sum(take(x0, x1), take(x0, x2)), x3))=IF(true, x4, x5, x6, x7) ⇒ IF(true, x4, x5, x6, x7)≥IF(le(s(x4), min(len(x5), len(x6))), s(x4), x5, x6, cons(sum(take(x4, x5), take(x4, x6)), x7))) |
We simplified constraint (1) using rules (I), (II), (III), (IV), (VII) which results in the following new constraint:
| (2) (s(x0)=x8∧min(x10, x11)=x9∧le(x8, x9)=true∧cons(sum(take(x0, x1), take(x0, x2)), x3)=x7 ⇒ IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7))) |
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on le(x8, x9)=true which results in the following new constraints:
| (3) (le(x14, x13)=true∧s(x0)=s(x14)∧min(x10, x11)=s(x13)∧cons(sum(take(x0, x1), take(x0, x2)), x3)=x7∧(∀x15,x16,x17,x18,x19,x20,x21:le(x14, x13)=true∧s(x15)=x14∧min(x16, x17)=x13∧cons(sum(take(x15, x18), take(x15, x19)), x20)=x21 ⇒ IF(true, s(x15), x18, x19, x21)≥IF(le(s(s(x15)), min(len(x18), len(x19))), s(s(x15)), x18, x19, cons(sum(take(s(x15), x18), take(s(x15), x19)), x21))) ⇒ IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7))) |
| (4) (true=true∧s(x0)=0∧min(x10, x11)=x22∧cons(sum(take(x0, x1), take(x0, x2)), x3)=x7 ⇒ IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7))) |
We simplified constraint (3) using rules (I), (II) which results in the following new constraint:
| (5) (le(x14, x13)=true∧x0=x14∧min(x10, x11)=s(x13)∧cons(sum(take(x0, x1), take(x0, x2)), x3)=x7∧(∀x15,x16,x17,x18,x19,x20,x21:le(x14, x13)=true∧s(x15)=x14∧min(x16, x17)=x13∧cons(sum(take(x15, x18), take(x15, x19)), x20)=x21 ⇒ IF(true, s(x15), x18, x19, x21)≥IF(le(s(s(x15)), min(len(x18), len(x19))), s(s(x15)), x18, x19, cons(sum(take(s(x15), x18), take(s(x15), x19)), x21))) ⇒ IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7))) |
We solved constraint (4) using rules (I), (II).We simplified constraint (5) using rule (V) (with possible (I) afterwards) using induction on min(x10, x11)=s(x13) which results in the following new constraint:
| (6) (min(x26, x25)=s(x13)∧le(x14, x13)=true∧x0=x14∧cons(sum(take(x0, x1), take(x0, x2)), x3)=x7∧(∀x15,x16,x17,x18,x19,x20,x21:le(x14, x13)=true∧s(x15)=x14∧min(x16, x17)=x13∧cons(sum(take(x15, x18), take(x15, x19)), x20)=x21 ⇒ IF(true, s(x15), x18, x19, x21)≥IF(le(s(s(x15)), min(len(x18), len(x19))), s(s(x15)), x18, x19, cons(sum(take(s(x15), x18), take(s(x15), x19)), x21)))∧(∀x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40:min(x26, x25)=s(x27)∧le(x28, x27)=true∧x29=x28∧cons(sum(take(x29, x30), take(x29, x31)), x32)=x33∧(∀x34,x35,x36,x37,x38,x39,x40:le(x28, x27)=true∧s(x34)=x28∧min(x35, x36)=x27∧cons(sum(take(x34, x37), take(x34, x38)), x39)=x40 ⇒ IF(true, s(x34), x37, x38, x40)≥IF(le(s(s(x34)), min(len(x37), len(x38))), s(s(x34)), x37, x38, cons(sum(take(s(x34), x37), take(s(x34), x38)), x40))) ⇒ IF(true, s(x29), x30, x31, x33)≥IF(le(s(s(x29)), min(len(x30), len(x31))), s(s(x29)), x30, x31, cons(sum(take(s(x29), x30), take(s(x29), x31)), x33))) ⇒ IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7))) |
We simplified constraint (6) using rule (VI) where we applied the induction hypothesis (∀x27,x28,x29,x30,x31,x32,x33,x34,x35,x36,x37,x38,x39,x40:min(x26, x25)=s(x27)∧le(x28, x27)=true∧x29=x28∧cons(sum(take(x29, x30), take(x29, x31)), x32)=x33∧(∀x34,x35,x36,x37,x38,x39,x40:le(x28, x27)=true∧s(x34)=x28∧min(x35, x36)=x27∧cons(sum(take(x34, x37), take(x34, x38)), x39)=x40 ⇒ IF(true, s(x34), x37, x38, x40)≥IF(le(s(s(x34)), min(len(x37), len(x38))), s(s(x34)), x37, x38, cons(sum(take(s(x34), x37), take(s(x34), x38)), x40))) ⇒ IF(true, s(x29), x30, x31, x33)≥IF(le(s(s(x29)), min(len(x30), len(x31))), s(s(x29)), x30, x31, cons(sum(take(s(x29), x30), take(s(x29), x31)), x33))) with σ = [x27 / x13, x28 / x14, x29 / x0, x30 / x1, x31 / x2, x32 / x3, x33 / x7, x34 / x15, x37 / x18, x38 / x19, x40 / x21, x35 / x16, x36 / x17, x39 / x20] which results in the following new constraint:
| (7) (IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7)) ⇒ IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7))) |
To summarize, we get the following constraints P
≥ for the following pairs.
- IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
- (IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7)) ⇒ IF(true, s(x0), x1, x2, x7)≥IF(le(s(s(x0)), min(len(x1), len(x2))), s(s(x0)), x1, x2, cons(sum(take(s(x0), x1), take(s(x0), x2)), x7)))
The constraints for P
> respective P
bound are constructed from P
≥ where we just replace every occurence of "t ≥ s" in P
≥ by "t > s" respective "t ≥
c". Here
c stands for the fresh constant used for P
bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation [NONINF]:
POL(0) = 0
POL(IF(x1, x2, x3, x4, x5)) = -1 - x1 - x2 - x3 - x4 - x5
POL(c) = -1
POL(cons(x1, x2)) = x2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(len(x1)) = 0
POL(min(x1, x2)) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(sum(x1, x2)) = 0
POL(take(x1, x2)) = 0
POL(true) = 0
The following pairs are in P
>:
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The following pairs are in P
bound:
IF(true, c, xs, ys, z) → IF(le(s(c), min(len(xs), len(ys))), s(c), xs, ys, cons(sum(take(c, xs), take(c, ys)), z))
The following rules are usable:
false → le(s(x), 0)
le(x, y) → le(s(x), s(y))
true → le(0, x)
(48) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
len(nil) → 0
len(cons(x, xs)) → s(len(xs))
min(0, y) → 0
min(s(x), 0) → 0
min(s(x), s(y)) → min(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
take(0, cons(y, ys)) → y
take(s(x), cons(y, ys)) → take(x, ys)
sum(x, 0) → x
sum(x, s(y)) → s(sum(x, y))
le(0, x) → true
The set Q consists of the following terms:
min(0, x0)
min(s(x0), 0)
min(s(x0), s(x1))
len(nil)
len(cons(x0, x1))
sum(x0, 0)
sum(x0, s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
take(0, cons(x0, x1))
take(s(x0), cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(49) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(50) YES