(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), 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:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(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:
EQ(s(x), s(y)) → EQ(x, y)
LE(s(x), s(y)) → LE(x, y)
APP(add(n, x), y) → APP(x, y)
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
MIN(add(n, add(m, x))) → LE(n, m)
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
RM(n, add(m, x)) → EQ(n, m)
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
MINSORT(x) → MINS(x, nil, nil)
MINS(x, y, z) → IF(null(x), x, y, z)
MINS(x, y, z) → NULL(x)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF(false, x, y, z) → EQ(head(x), min(x))
IF(false, x, y, z) → HEAD(x)
IF(false, x, y, z) → MIN(x)
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
IF2(true, x, y, z) → APP(rm(head(x), tail(x)), y)
IF2(true, x, y, z) → RM(head(x), tail(x))
IF2(true, x, y, z) → HEAD(x)
IF2(true, x, y, z) → TAIL(x)
IF2(true, x, y, z) → APP(z, add(head(x), nil))
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(false, x, y, z) → TAIL(x)
IF2(false, x, y, z) → HEAD(x)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
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 14 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APP(add(n, x), y) → APP(x, y)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
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:
APP(add(n, x), y) → APP(x, y)
R is empty.
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
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].
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APP(add(n, x), y) → APP(x, y)
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:
- APP(add(n, x), y) → APP(x, y)
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:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
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:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
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].
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(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:
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
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:
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
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].
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(26) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( IF_MIN(x1, x2) ) = max{0, 2x1 + x2 - 2} |
POL( MIN(x1) ) = max{0, 2x1 - 1} |
POL( add(x1, x2) ) = 2x2 + 2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
(27) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(28) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(29) YES
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x), s(y)) → EQ(x, y)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(31) 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.
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x), s(y)) → EQ(x, y)
R is empty.
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(33) 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].
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
EQ(s(x), s(y)) → EQ(x, y)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(35) 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:
- EQ(s(x), s(y)) → EQ(x, y)
The graph contains the following edges 1 > 1, 2 > 2
(36) YES
(37) Obligation:
Q DP problem:
The TRS P consists of the following rules:
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(38) 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.
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(40) 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].
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(42) 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:
- RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
The graph contains the following edges 1 >= 2, 2 >= 3
- IF_RM(true, n, add(m, x)) → RM(n, x)
The graph contains the following edges 2 >= 1, 3 > 2
- IF_RM(false, n, add(m, x)) → RM(n, x)
The graph contains the following edges 2 >= 1, 3 > 2
(43) YES
(44) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
MINS(x, y, z) → IF(null(x), x, y, z)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
The TRS R consists of the following rules:
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(x) → mins(x, nil, nil)
mins(x, y, z) → if(null(x), x, y, z)
if(true, x, y, z) → z
if(false, x, y, z) → if2(eq(head(x), min(x)), x, y, z)
if2(true, x, y, z) → mins(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
if2(false, x, y, z) → mins(tail(x), add(head(x), y), z)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(45) 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.
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
MINS(x, y, z) → IF(null(x), x, y, z)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
We have to consider all minimal (P,Q,R)-chains.
(47) 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].
minsort(x0)
mins(x0, x1, x2)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(48) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
MINS(x, y, z) → IF(null(x), x, y, z)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(49) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
MINS(
x,
y,
z) →
IF(
null(
x),
x,
y,
z) at position [0] we obtained the following new rules [LPAR04]:
MINS(nil, y1, y2) → IF(true, nil, y1, y2) → MINS(nil, y1, y2) → IF(true, nil, y1, y2)
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2) → MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
(50) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
MINS(nil, y1, y2) → IF(true, nil, y1, y2)
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(51) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(52) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
null(nil) → true
null(add(n, x)) → false
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(53) 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.
(54) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(55) 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].
null(nil)
null(add(x0, x1))
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, x, y, z) → MINS(app(rm(head(x), tail(x)), y), nil, app(z, add(head(x), nil)))
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(57) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF2(
true,
x,
y,
z) →
MINS(
app(
rm(
head(
x),
tail(
x)),
y),
nil,
app(
z,
add(
head(
x),
nil))) at position [0] we obtained the following new rules [LPAR04]:
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, tail(add(x0, x1))), y1), nil, app(y2, add(head(add(x0, x1)), nil))) → IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, tail(add(x0, x1))), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(head(add(x0, x1)), x1), y1), nil, app(y2, add(head(add(x0, x1)), nil))) → IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(head(add(x0, x1)), x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
IF2(true, nil, y1, y2) → MINS(app(rm(head(nil), nil), y1), nil, app(y2, add(head(nil), nil))) → IF2(true, nil, y1, y2) → MINS(app(rm(head(nil), nil), y1), nil, app(y2, add(head(nil), nil)))
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, tail(add(x0, x1))), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(head(add(x0, x1)), x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
IF2(true, nil, y1, y2) → MINS(app(rm(head(nil), nil), y1), nil, app(y2, add(head(nil), nil)))
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(59) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF2(
true,
add(
x0,
x1),
y1,
y2) →
MINS(
app(
rm(
x0,
tail(
add(
x0,
x1))),
y1),
nil,
app(
y2,
add(
head(
add(
x0,
x1)),
nil))) at position [0,0,1] we obtained the following new rules [LPAR04]:
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(head(add(x0, x1)), nil))) → IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(head(add(x0, x1)), x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
IF2(true, nil, y1, y2) → MINS(app(rm(head(nil), nil), y1), nil, app(y2, add(head(nil), nil)))
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(61) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF2(
true,
add(
x0,
x1),
y1,
y2) →
MINS(
app(
rm(
head(
add(
x0,
x1)),
x1),
y1),
nil,
app(
y2,
add(
head(
add(
x0,
x1)),
nil))) at position [0,0,0] we obtained the following new rules [LPAR04]:
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(head(add(x0, x1)), nil))) → IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(true, nil, y1, y2) → MINS(app(rm(head(nil), nil), y1), nil, app(y2, add(head(nil), nil)))
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(63) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF2(
true,
nil,
y1,
y2) →
MINS(
app(
rm(
head(
nil),
nil),
y1),
nil,
app(
y2,
add(
head(
nil),
nil))) at position [0,0] we obtained the following new rules [LPAR04]:
IF2(true, nil, y1, y2) → MINS(app(nil, y1), nil, app(y2, add(head(nil), nil))) → IF2(true, nil, y1, y2) → MINS(app(nil, y1), nil, app(y2, add(head(nil), nil)))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(head(add(x0, x1)), nil)))
IF2(true, nil, y1, y2) → MINS(app(nil, y1), nil, app(y2, add(head(nil), nil)))
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(65) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF2(
true,
add(
x0,
x1),
y1,
y2) →
MINS(
app(
rm(
x0,
x1),
y1),
nil,
app(
y2,
add(
head(
add(
x0,
x1)),
nil))) at position [2,1,0] we obtained the following new rules [LPAR04]:
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil))) → IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(true, nil, y1, y2) → MINS(app(nil, y1), nil, app(y2, add(head(nil), nil)))
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(67) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF2(
true,
nil,
y1,
y2) →
MINS(
app(
nil,
y1),
nil,
app(
y2,
add(
head(
nil),
nil))) at position [0] we obtained the following new rules [LPAR04]:
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil))) → IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(false, x, y, z) → MINS(tail(x), add(head(x), y), z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(69) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
IF2(
false,
x,
y,
z) →
MINS(
tail(
x),
add(
head(
x),
y),
z) at position [0] we obtained the following new rules [LPAR04]:
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(head(add(x0, x1)), y1), y2) → IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(head(add(x0, x1)), y1), y2)
IF2(false, nil, y1, y2) → MINS(nil, add(head(nil), y1), y2) → IF2(false, nil, y1, y2) → MINS(nil, add(head(nil), y1), y2)
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(head(add(x0, x1)), y1), y2)
IF2(false, nil, y1, y2) → MINS(nil, add(head(nil), y1), y2)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(71) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(head(add(x0, x1)), y1), y2)
The TRS R consists of the following rules:
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(73) 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.
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(head(add(x0, x1)), y1), y2)
The TRS R consists of the following rules:
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(75) 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(add(x0, x1))
tail(nil)
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(head(add(x0, x1)), y1), y2)
The TRS R consists of the following rules:
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(77) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF2(
false,
add(
x0,
x1),
y1,
y2) →
MINS(
x1,
add(
head(
add(
x0,
x1)),
y1),
y2) at position [1,0] we obtained the following new rules [LPAR04]:
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2) → IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, y, z) → IF2(eq(head(x), min(x)), x, y, z)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
The TRS R consists of the following rules:
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(79) TransformationProof (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
IF(
false,
x,
y,
z) →
IF2(
eq(
head(
x),
min(
x)),
x,
y,
z) we obtained the following new rules [LPAR04]:
IF(false, add(z0, z1), z2, z3) → IF2(eq(head(add(z0, z1)), min(add(z0, z1))), add(z0, z1), z2, z3) → IF(false, add(z0, z1), z2, z3) → IF2(eq(head(add(z0, z1)), min(add(z0, z1))), add(z0, z1), z2, z3)
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, nil, y1, y2) → MINS(y1, nil, app(y2, add(head(nil), nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(head(add(z0, z1)), min(add(z0, z1))), add(z0, z1), z2, z3)
The TRS R consists of the following rules:
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(81) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(head(add(z0, z1)), min(add(z0, z1))), add(z0, z1), z2, z3)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
The TRS R consists of the following rules:
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(83) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
IF(
false,
add(
z0,
z1),
z2,
z3) →
IF2(
eq(
head(
add(
z0,
z1)),
min(
add(
z0,
z1))),
add(
z0,
z1),
z2,
z3) at position [0,0] we obtained the following new rules [LPAR04]:
IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3) → IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
The TRS R consists of the following rules:
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(85) 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.
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
The TRS R consists of the following rules:
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
head(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(87) 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(add(x0, x1))
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
The TRS R consists of the following rules:
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(89) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
IF2(true, add(x0, x1), y1, y2) → MINS(app(rm(x0, x1), y1), nil, app(y2, add(x0, nil)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( MINS(x1, ..., x3) ) = x1 + x2 |
POL( app(x1, x2) ) = x1 + x2 |
POL( add(x1, x2) ) = x1 + x2 + 1 |
POL( if_rm(x1, ..., x3) ) = x3 |
POL( IF2(x1, ..., x4) ) = x2 + x3 |
POL( min(x1) ) = max{0, x1 - 2} |
POL( if_min(x1, x2) ) = x2 |
POL( IF(x1, ..., x4) ) = x1 + x2 + x3 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
(90) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
The TRS R consists of the following rules:
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(91) 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.
(92) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
The TRS R consists of the following rules:
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(93) 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].
app(nil, x0)
app(add(x0, x1), x2)
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
(94) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
The TRS R consists of the following rules:
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
The set Q consists of the following terms:
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(add(x0, nil))
min(add(x0, add(x1, x2)))
if_min(true, add(x0, add(x1, x2)))
if_min(false, add(x0, add(x1, x2)))
We have to consider all minimal (P,Q,R)-chains.
(95) 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:
- IF(false, add(z0, z1), z2, z3) → IF2(eq(z0, min(add(z0, z1))), add(z0, z1), z2, z3)
The graph contains the following edges 2 >= 2, 3 >= 3, 4 >= 4
- IF2(false, add(x0, x1), y1, y2) → MINS(x1, add(x0, y1), y2)
The graph contains the following edges 2 > 1, 4 >= 3
- MINS(add(x0, x1), y1, y2) → IF(false, add(x0, x1), y1, y2)
The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4
(96) YES