(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
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:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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:
QSORT(xs) → QS(half(length(xs)), xs)
QSORT(xs) → HALF(length(xs))
QSORT(xs) → LENGTH(xs)
QS(n, cons(x, xs)) → APPEND(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → HALF(n)
QS(n, cons(x, xs)) → FILTERLOW(get(n, cons(x, xs)), cons(x, xs))
QS(n, cons(x, xs)) → GET(n, cons(x, xs))
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → FILTERHIGH(get(n, cons(x, xs)), cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
LENGTH(cons(x, xs)) → LENGTH(xs)
HALF(s(s(x))) → HALF(x)
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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 8 SCCs with 10 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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:
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
R is empty.
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
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:
- GET(s(n), cons(x, cons(y, xs))) → GET(n, cons(y, xs))
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:
HALF(s(s(x))) → HALF(x)
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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:
HALF(s(s(x))) → HALF(x)
R is empty.
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
HALF(s(s(x))) → HALF(x)
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:
- HALF(s(s(x))) → HALF(x)
The graph contains the following edges 1 > 1
(20) YES
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LENGTH(cons(x, xs)) → LENGTH(xs)
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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:
LENGTH(cons(x, xs)) → LENGTH(xs)
R is empty.
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LENGTH(cons(x, xs)) → LENGTH(xs)
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:
- LENGTH(cons(x, xs)) → LENGTH(xs)
The graph contains the following edges 1 > 1
(27) YES
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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:
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
R is empty.
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPEND(cons(x, xs), ys) → APPEND(xs, ys)
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:
- APPEND(cons(x, xs), ys) → APPEND(xs, ys)
The graph contains the following edges 1 > 1, 2 >= 2
(34) YES
(35) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(x, y)
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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:
GE(s(x), s(y)) → GE(x, y)
R is empty.
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(39) Obligation:
Q DP problem:
The TRS P consists of the following rules:
GE(s(x), s(y)) → GE(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:
- GE(s(x), s(y)) → GE(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:
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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:
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(46) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(47) 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:
- FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
- IF2(true, n, x, xs) → FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
- IF2(false, n, x, xs) → FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
(48) YES
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(50) 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.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(52) 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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(53) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
The TRS R consists of the following rules:
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
The set Q consists of the following terms:
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(54) 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:
- FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
- IF1(true, n, x, xs) → FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
- IF1(false, n, x, xs) → FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
(55) YES
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
The TRS R consists of the following rules:
qsort(xs) → qs(half(length(xs)), xs)
qs(n, nil) → nil
qs(n, cons(x, xs)) → append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))), cons(get(n, cons(x, xs)), qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))
length(nil) → 0
length(cons(x, xs)) → s(length(xs))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, nil) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(57) 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.
(58) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(59) 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].
qsort(x0)
qs(x0, nil)
qs(x0, cons(x1, x2))
append(nil, ys)
append(cons(x0, x1), ys)
length(nil)
length(cons(x0, x1))
(60) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(61) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
n,
cons(
x,
xs)) →
QS(
half(
n),
filterhigh(
get(
n,
cons(
x,
xs)),
cons(
x,
xs))) at position [1] we obtained the following new rules [LPAR04]:
QS(n, cons(x, xs)) → QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs)) → QS(n, cons(x, xs)) → QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs)))
QS(n, cons(x, xs)) → QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(63) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
n,
cons(
x,
xs)) →
QS(
half(
n),
filterlow(
get(
n,
cons(
x,
xs)),
cons(
x,
xs))) at position [1] we obtained the following new rules [LPAR04]:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs)) → QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
(64) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if2(ge(x, get(n, cons(x, xs))), get(n, cons(x, xs)), x, xs))
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(65) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QS(
n,
cons(
x,
xs)) →
QS(
half(
n),
if2(
ge(
x,
get(
n,
cons(
x,
xs))),
get(
n,
cons(
x,
xs)),
x,
xs)) at position [1] we obtained the following new rules [LPAR04]:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
(66) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(67) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
x0,
cons(
x1,
nil)) →
QS(
half(
x0),
if2(
ge(
x1,
x1),
get(
x0,
cons(
x1,
nil)),
x1,
nil)) at position [1,1] we obtained the following new rules [LPAR04]:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
(68) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(69) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
half(
0),
if2(
ge(
x0,
x0),
get(
0,
cons(
x0,
cons(
x1,
x2))),
x0,
cons(
x1,
x2))) at position [0] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
(70) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(71) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
s(
x0),
cons(
x1,
cons(
x2,
x3))) →
QS(
half(
s(
x0)),
if2(
ge(
x1,
get(
x0,
cons(
x2,
x3))),
get(
s(
x0),
cons(
x1,
cons(
x2,
x3))),
x1,
cons(
x2,
x3))) at position [1,1] we obtained the following new rules [LPAR04]:
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
(72) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, get(x0, cons(x1, nil))), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(73) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
x0,
cons(
x1,
nil)) →
QS(
half(
x0),
if2(
ge(
x1,
get(
x0,
cons(
x1,
nil))),
x1,
x1,
nil)) at position [1,0,1] we obtained the following new rules [LPAR04]:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(75) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
half(
0),
if2(
ge(
x0,
get(
0,
cons(
x0,
cons(
x1,
x2)))),
x0,
x0,
cons(
x1,
x2))) at position [0] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
(76) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(s(x0), cons(x1, cons(x2, x3)))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(77) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
s(
x0),
cons(
x1,
cons(
x2,
x3))) →
QS(
half(
s(
x0)),
if2(
ge(
x1,
get(
s(
x0),
cons(
x1,
cons(
x2,
x3)))),
get(
x0,
cons(
x2,
x3)),
x1,
cons(
x2,
x3))) at position [1,0,1] we obtained the following new rules [LPAR04]:
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
(78) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(79) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
0,
if2(
ge(
x0,
x0),
get(
0,
cons(
x0,
cons(
x1,
x2))),
x0,
cons(
x1,
x2))) at position [1,1] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
(80) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, get(0, cons(x0, cons(x1, x2)))), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(81) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
0,
if2(
ge(
x0,
get(
0,
cons(
x0,
cons(
x1,
x2)))),
x0,
x0,
cons(
x1,
x2))) at position [1,0,1] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
(82) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(n, cons(x, xs)) → QS(half(n), if1(ge(get(n, cons(x, xs)), x), get(n, cons(x, xs)), x, xs))
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(83) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
QS(
n,
cons(
x,
xs)) →
QS(
half(
n),
if1(
ge(
get(
n,
cons(
x,
xs)),
x),
get(
n,
cons(
x,
xs)),
x,
xs)) at position [1] we obtained the following new rules [LPAR04]:
QS(y0, cons(0, y2)) → QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2)) → QS(y0, cons(0, y2)) → QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
(84) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), if1(true, get(y0, cons(0, y2)), 0, y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(85) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
y0,
cons(
0,
y2)) →
QS(
half(
y0),
if1(
true,
get(
y0,
cons(
0,
y2)),
0,
y2)) at position [1] we obtained the following new rules [LPAR04]:
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2)) → QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
(86) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), get(x0, cons(x1, nil)), x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(87) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
x0,
cons(
x1,
nil)) →
QS(
half(
x0),
if1(
ge(
x1,
x1),
get(
x0,
cons(
x1,
nil)),
x1,
nil)) at position [1,1] we obtained the following new rules [LPAR04]:
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
(88) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(89) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
half(
0),
if1(
ge(
x0,
x0),
get(
0,
cons(
x0,
cons(
x1,
x2))),
x0,
cons(
x1,
x2))) at position [0] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
(90) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(s(x0), cons(x1, cons(x2, x3))), x1, cons(x2, x3)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(91) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
s(
x0),
cons(
x1,
cons(
x2,
x3))) →
QS(
half(
s(
x0)),
if1(
ge(
get(
x0,
cons(
x2,
x3)),
x1),
get(
s(
x0),
cons(
x1,
cons(
x2,
x3))),
x1,
cons(
x2,
x3))) at position [1,1] we obtained the following new rules [LPAR04]:
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
(92) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(get(x0, cons(x1, nil)), x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(93) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
x0,
cons(
x1,
nil)) →
QS(
half(
x0),
if1(
ge(
get(
x0,
cons(
x1,
nil)),
x1),
x1,
x1,
nil)) at position [1,0,0] we obtained the following new rules [LPAR04]:
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil)) → QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
(94) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(half(0), if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(95) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
half(
0),
if1(
ge(
get(
0,
cons(
x0,
cons(
x1,
x2))),
x0),
x0,
x0,
cons(
x1,
x2))) at position [0] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
(96) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(s(x0), cons(x1, cons(x2, x3))), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(97) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
s(
x0),
cons(
x1,
cons(
x2,
x3))) →
QS(
half(
s(
x0)),
if1(
ge(
get(
s(
x0),
cons(
x1,
cons(
x2,
x3))),
x1),
get(
x0,
cons(
x2,
x3)),
x1,
cons(
x2,
x3))) at position [1,0,0] we obtained the following new rules [LPAR04]:
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3))) → QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
(98) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), get(0, cons(x0, cons(x1, x2))), x0, cons(x1, x2)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(99) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
0,
if1(
ge(
x0,
x0),
get(
0,
cons(
x0,
cons(
x1,
x2))),
x0,
cons(
x1,
x2))) at position [1,1] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
(100) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(get(0, cons(x0, cons(x1, x2))), x0), x0, x0, cons(x1, x2)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(101) TransformationProof (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
0,
if1(
ge(
get(
0,
cons(
x0,
cons(
x1,
x2))),
x0),
x0,
x0,
cons(
x1,
x2))) at position [1,0,0] we obtained the following new rules [LPAR04]:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2))) → QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
(102) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(103) QDPQMonotonicMRRProof (EQUIVALENT transformation)
By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.
Strictly oriented rules of the TRS R:
half(s(0)) → 0
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 2
POL(QS(x1, x2)) = 2·x1
POL(cons(x1, x2)) = x1 + 2·x2
POL(false) = 0
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = x1 + x2
POL(get(x1, x2)) = x2
POL(half(x1)) = x1
POL(if1(x1, x2, x3, x4)) = x3 + 2·x4
POL(if2(x1, x2, x3, x4)) = x3 + 2·x4
POL(nil) = 1
POL(s(x1)) = 2·x1
POL(true) = 0
(104) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
half(s(s(x))) → s(half(x))
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(105) QDPQMonotonicMRRProof (EQUIVALENT transformation)
By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.
Strictly oriented rules of the TRS R:
half(s(s(x))) → s(half(x))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 1
POL(QS(x1, x2)) = 2·x1
POL(cons(x1, x2)) = 1 + x1 + 2·x2
POL(false) = 0
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 0
POL(get(x1, x2)) = x2
POL(half(x1)) = x1
POL(if1(x1, x2, x3, x4)) = 1 + x3 + 2·x4
POL(if2(x1, x2, x3, x4)) = 1 + 2·x1 + x3 + 2·x4
POL(nil) = 2
POL(s(x1)) = 1 + 2·x1
POL(true) = 0
(106) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(107) QDPQMonotonicMRRProof (EQUIVALENT transformation)
By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.
Strictly oriented dependency pairs:
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if2(ge(x1, get(x0, cons(x2, x3))), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
QS(s(x0), cons(x1, cons(x2, x3))) → QS(half(s(x0)), if1(ge(get(x0, cons(x2, x3)), x1), get(x0, cons(x2, x3)), x1, cons(x2, x3)))
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(QS(x1, x2)) = x1
POL(cons(x1, x2)) = x1 + 2·x2
POL(false) = 0
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 2
POL(get(x1, x2)) = x2
POL(half(x1)) = 0
POL(if1(x1, x2, x3, x4)) = x3 + 2·x4
POL(if2(x1, x2, x3, x4)) = x3 + 2·x4
POL(nil) = 2
POL(s(x1)) = 1
POL(true) = 0
(108) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(109) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
QS(y0, cons(0, y2)) → QS(half(y0), filterlow(get(y0, cons(0, y2)), y2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
| POL( QS(x1, x2) ) = 2x1 + 2x2 + 2 |
| POL( if1(x1, ..., x4) ) = x1 + x3 + 2x4 + 1 |
| POL( if2(x1, ..., x4) ) = x3 + 2x4 + 1 |
| POL( filterhigh(x1, x2) ) = x2 |
| POL( cons(x1, x2) ) = x1 + 2x2 + 1 |
| POL( filterlow(x1, x2) ) = x2 |
| POL( get(x1, x2) ) = max{0, -2} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
half(0) → 0
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
filterlow(n, nil) → nil
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
ge(0, s(x)) → false
filterhigh(n, nil) → nil
(110) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
half(0) → 0
get(n, cons(x, nil)) → x
get(0, cons(x, cons(y, xs))) → x
get(s(n), cons(x, cons(y, xs))) → get(n, cons(y, xs))
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(111) 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.
(112) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
We have to consider all minimal (P,Q,R)-chains.
(113) 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].
get(x0, nil)
get(x0, cons(x1, nil))
get(0, cons(x0, cons(x1, x2)))
get(s(x0), cons(x1, cons(x2, x3)))
(114) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if2(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(115) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:QS(
x0,
cons(
x1,
nil)) →
QS(
half(
x0),
if2(
ge(
x1,
x1),
x1,
x1,
nil))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 0
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false_renamed) = 1
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(half(x1)) = 1
POL(if1(x1, x2, x3, x4)) = x1 + x4
POL(if2(x1, x2, x3, x4)) = x1 + x4
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true_renamed) = 1
At least one of these decreasing rules is always used after the deleted DP:if2(
true_renamed,
n2,
x6,
xs1) →
filterhigh(
n2,
xs1)
The following formula is valid:x1:sort[a0].
if2'(
ge(
x1 ,
x1 ),
x1 ,
x1 ,
nil)=
trueThe transformed set:if2'(
true_renamed,
n2,
x6,
xs1) →
truefilterhigh'(
n3,
cons(
x7,
xs2)) →
if2'(
ge(
x7,
n3),
n3,
x7,
xs2)
if2'(
false_renamed,
n4,
x8,
xs3) →
filterhigh'(
n4,
xs3)
filterhigh'(
n5,
nil) →
falsege(
x,
0) →
true_renamedge(
s(
x'),
s(
y)) →
ge(
x',
y)
if1(
true_renamed,
n,
x'',
xs) →
filterlow(
n,
xs)
filterlow(
n',
cons(
x3,
xs')) →
if1(
ge(
n',
x3),
n',
x3,
xs')
if1(
false_renamed,
n'',
x4,
xs'') →
cons(
x4,
filterlow(
n'',
xs''))
filterlow(
n1,
nil) →
nilge(
0,
s(
x5)) →
false_renamedhalf(
0) →
0if2(
true_renamed,
n2,
x6,
xs1) →
filterhigh(
n2,
xs1)
filterhigh(
n3,
cons(
x7,
xs2)) →
if2(
ge(
x7,
n3),
n3,
x7,
xs2)
if2(
false_renamed,
n4,
x8,
xs3) →
cons(
x8,
filterhigh(
n4,
xs3))
filterhigh(
n5,
nil) →
nilhalf(
s(
v14)) →
0equal_bool(
true,
false) →
falseequal_bool(
false,
true) →
falseequal_bool(
true,
true) →
trueequal_bool(
false,
false) →
trueand(
true,
x) →
xand(
false,
x) →
falseor(
true,
x) →
trueor(
false,
x) →
xnot(
false) →
truenot(
true) →
falseisa_true(
true) →
trueisa_true(
false) →
falseisa_false(
true) →
falseisa_false(
false) →
trueequal_sort[a0](
0,
0) →
trueequal_sort[a0](
0,
s(
v23)) →
falseequal_sort[a0](
s(
v24),
0) →
falseequal_sort[a0](
s(
v24),
s(
v25)) →
equal_sort[a0](
v24,
v25)
equal_sort[a5](
cons(
v26,
v27),
cons(
v28,
v29)) →
and(
equal_sort[a0](
v26,
v28),
equal_sort[a5](
v27,
v29))
equal_sort[a5](
cons(
v26,
v27),
nil) →
falseequal_sort[a5](
nil,
cons(
v30,
v31)) →
falseequal_sort[a5](
nil,
nil) →
trueequal_sort[a36](
true_renamed,
true_renamed) →
trueequal_sort[a36](
true_renamed,
false_renamed) →
falseequal_sort[a36](
false_renamed,
true_renamed) →
falseequal_sort[a36](
false_renamed,
false_renamed) →
trueequal_sort[a66](
witness_sort[a66],
witness_sort[a66]) →
trueThe proof given by the theorem prover:The following output was given by the internal theorem prover:
proof of internal
# AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished
Partial correctness of the following Program
[x, v23, v24, v25, v26, v27, v28, v29, v30, v31, n2, x6, xs1, n4, x8, x7, xs2, n5, n3, x', y, x5, n1, n', x3, xs', v14, n, x'', n'', x4]
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
true and x -> x
false and x -> false
true or x -> true
false or x -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v23)) -> false
equal_sort[a0](s(v24), 0) -> false
equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> equal_sort[a0](v26, v28) and equal_sort[a5](v27, v29)
equal_sort[a5](cons(v26, v27), nil) -> false
equal_sort[a5](nil, cons(v30, v31)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a36](true_renamed, true_renamed) -> true
equal_sort[a36](true_renamed, false_renamed) -> false
equal_sort[a36](false_renamed, true_renamed) -> false
equal_sort[a36](false_renamed, false_renamed) -> true
equal_sort[a66](witness_sort[a66], witness_sort[a66]) -> true
if2'(true_renamed, n2, x6, xs1) -> true
if2'(false_renamed, n4, x8, cons(x7, xs2)) -> if2'(ge(x7, n4), n4, x7, xs2)
if2'(false_renamed, n4, x8, nil) -> false
filterhigh'(n5, nil) -> false
equal_sort[a36](ge(x7, n3), true_renamed) -> true | filterhigh'(n3, cons(x7, xs2)) -> true
equal_sort[a36](ge(x7, n3), true_renamed) -> false | filterhigh'(n3, cons(x7, xs2)) -> filterhigh'(n3, xs2)
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
ge(0, s(x5)) -> false_renamed
filterlow(n1, nil) -> nil
equal_sort[a36](ge(n', x3), true_renamed) -> true | filterlow(n', cons(x3, xs')) -> filterlow(n', xs')
equal_sort[a36](ge(n', x3), true_renamed) -> false | filterlow(n', cons(x3, xs')) -> cons(x3, filterlow(n', xs'))
half(0) -> 0
half(s(v14)) -> 0
filterhigh(n5, nil) -> nil
equal_sort[a36](ge(x7, n3), true_renamed) -> true | filterhigh(n3, cons(x7, xs2)) -> filterhigh(n3, xs2)
equal_sort[a36](ge(x7, n3), true_renamed) -> false | filterhigh(n3, cons(x7, xs2)) -> cons(x7, filterhigh(n3, xs2))
if1(true_renamed, n, x'', cons(x3, xs')) -> if1(ge(n, x3), n, x3, xs')
if1(true_renamed, n, x'', nil) -> nil
if1(false_renamed, n'', x4, cons(x3, xs')) -> cons(x4, if1(ge(n'', x3), n'', x3, xs'))
if1(false_renamed, n'', x4, nil) -> cons(x4, nil)
if2(true_renamed, n2, x6, cons(x7, xs2)) -> if2(ge(x7, n2), n2, x7, xs2)
if2(true_renamed, n2, x6, nil) -> nil
if2(false_renamed, n4, x8, cons(x7, xs2)) -> cons(x8, if2(ge(x7, n4), n4, x7, xs2))
if2(false_renamed, n4, x8, nil) -> cons(x8, nil)
using the following formula:
x1:sort[a0].if2'(ge(x1, x1), x1, x1, nil)=true
could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
(3) Formula
(4) Symbolic evaluation [EQUIVALENT, 0 ms]
(5) YES
(6) Formula
(7) Symbolic evaluation [EQUIVALENT, 0 ms]
(8) Formula
(9) Hypothesis Lifting [EQUIVALENT, 0 ms]
(10) Formula
(11) Inverse Substitution [SOUND, 0 ms]
(12) Formula
(13) Inverse Substitution [SOUND, 0 ms]
(14) Formula
(15) Induction by data structure [EQUIVALENT, 0 ms]
(16) AND
(17) Formula
(18) Symbolic evaluation [EQUIVALENT, 0 ms]
(19) YES
(20) Formula
(21) Symbolic evaluation [EQUIVALENT, 0 ms]
(22) YES
----------------------------------------
(0)
Obligation:
Formula:
x1:sort[a0].if2'(ge(x1, x1), x1, x1, nil)=true
There are no hypotheses.
----------------------------------------
(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
if2'(ge(0, 0), 0, 0, nil)=true
There are no hypotheses.
1. Step Case:
Formula:
n:sort[a0].if2'(ge(s(n), s(n)), s(n), s(n), nil)=true
Hypotheses:
n:sort[a0].if2'(ge(n, n), n, n, nil)=true
----------------------------------------
(2)
Complex Obligation (AND)
----------------------------------------
(3)
Obligation:
Formula:
if2'(ge(0, 0), 0, 0, nil)=true
There are no hypotheses.
----------------------------------------
(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(5)
YES
----------------------------------------
(6)
Obligation:
Formula:
n:sort[a0].if2'(ge(s(n), s(n)), s(n), s(n), nil)=true
Hypotheses:
n:sort[a0].if2'(ge(n, n), n, n, nil)=true
----------------------------------------
(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------
(8)
Obligation:
Formula:
n:sort[a0].if2'(ge(n, n), s(n), s(n), nil)=true
Hypotheses:
n:sort[a0].if2'(ge(n, n), n, n, nil)=true
----------------------------------------
(9) Hypothesis Lifting (EQUIVALENT)
Formula could be generalised by hypothesis lifting to the following new obligation:
Formula:
n:sort[a0].(if2'(ge(n, n), n, n, nil)=true->if2'(ge(n, n), s(n), s(n), nil)=true)
There are no hypotheses.
----------------------------------------
(10)
Obligation:
Formula:
n:sort[a0].(if2'(ge(n, n), n, n, nil)=true->if2'(ge(n, n), s(n), s(n), nil)=true)
There are no hypotheses.
----------------------------------------
(11) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a36],n:sort[a0].(if2'(n', n, n, nil)=true->if2'(n', s(n), s(n), nil)=true)
Inverse substitution used:
[ge(n, n)/n']
----------------------------------------
(12)
Obligation:
Formula:
n':sort[a36],n:sort[a0].(if2'(n', n, n, nil)=true->if2'(n', s(n), s(n), nil)=true)
There are no hypotheses.
----------------------------------------
(13) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a36],n:sort[a0],n'':sort[a0].(if2'(n', n, n, nil)=true->if2'(n', n'', n'', nil)=true)
Inverse substitution used:
[s(n)/n'']
----------------------------------------
(14)
Obligation:
Formula:
n':sort[a36],n:sort[a0],n'':sort[a0].(if2'(n', n, n, nil)=true->if2'(n', n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(15) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a36] generates the following cases:
1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if2'(true_renamed, n, n, nil)=true->if2'(true_renamed, n'', n'', nil)=true)
There are no hypotheses.
1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if2'(false_renamed, n, n, nil)=true->if2'(false_renamed, n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(16)
Complex Obligation (AND)
----------------------------------------
(17)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if2'(true_renamed, n, n, nil)=true->if2'(true_renamed, n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(18) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(19)
YES
----------------------------------------
(20)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if2'(false_renamed, n, n, nil)=true->if2'(false_renamed, n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(21) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(22)
YES
(116) Complex Obligation (AND)
(117) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if2(ge(x0, x0), x0, x0, cons(x1, x2)))
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(118) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
0,
if2(
ge(
x0,
x0),
x0,
x0,
cons(
x1,
x2)))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 1
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false_renamed) = 1
POL(filterhigh(x1, x2)) = x2
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(half(x1)) = 1
POL(if1(x1, x2, x3, x4)) = 1 + x4
POL(if2(x1, x2, x3, x4)) = x1 + x4
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true_renamed) = 1
At least one of these decreasing rules is always used after the deleted DP:if2(
true_renamed,
n2,
x6,
xs1) →
filterhigh(
n2,
xs1)
The following formula is valid:x0:sort[a0],x1:sort[a0],x2:sort[a5].
if2'(
ge(
x0 ,
x0 ),
x0 ,
x0 ,
cons(
x1 ,
x2 ))=
trueThe transformed set:if2'(
true_renamed,
n2,
x6,
xs1) →
truefilterhigh'(
n3,
cons(
x7,
xs2)) →
if2'(
ge(
x7,
n3),
n3,
x7,
xs2)
if2'(
false_renamed,
n4,
x8,
xs3) →
filterhigh'(
n4,
xs3)
filterhigh'(
n5,
nil) →
falsege(
x,
0) →
true_renamedge(
s(
x'),
s(
y)) →
ge(
x',
y)
if1(
true_renamed,
n,
x'',
xs) →
filterlow(
n,
xs)
filterlow(
n',
cons(
x3,
xs')) →
if1(
ge(
n',
x3),
n',
x3,
xs')
if1(
false_renamed,
n'',
x4,
xs'') →
cons(
x4,
filterlow(
n'',
xs''))
filterlow(
n1,
nil) →
nilge(
0,
s(
x5)) →
false_renamedhalf(
0) →
0if2(
true_renamed,
n2,
x6,
xs1) →
filterhigh(
n2,
xs1)
filterhigh(
n3,
cons(
x7,
xs2)) →
if2(
ge(
x7,
n3),
n3,
x7,
xs2)
if2(
false_renamed,
n4,
x8,
xs3) →
cons(
x8,
filterhigh(
n4,
xs3))
filterhigh(
n5,
nil) →
nilhalf(
s(
v14)) →
0equal_bool(
true,
false) →
falseequal_bool(
false,
true) →
falseequal_bool(
true,
true) →
trueequal_bool(
false,
false) →
trueand(
true,
x) →
xand(
false,
x) →
falseor(
true,
x) →
trueor(
false,
x) →
xnot(
false) →
truenot(
true) →
falseisa_true(
true) →
trueisa_true(
false) →
falseisa_false(
true) →
falseisa_false(
false) →
trueequal_sort[a0](
0,
0) →
trueequal_sort[a0](
0,
s(
v23)) →
falseequal_sort[a0](
s(
v24),
0) →
falseequal_sort[a0](
s(
v24),
s(
v25)) →
equal_sort[a0](
v24,
v25)
equal_sort[a5](
cons(
v26,
v27),
cons(
v28,
v29)) →
and(
equal_sort[a0](
v26,
v28),
equal_sort[a5](
v27,
v29))
equal_sort[a5](
cons(
v26,
v27),
nil) →
falseequal_sort[a5](
nil,
cons(
v30,
v31)) →
falseequal_sort[a5](
nil,
nil) →
trueequal_sort[a34](
true_renamed,
true_renamed) →
trueequal_sort[a34](
true_renamed,
false_renamed) →
falseequal_sort[a34](
false_renamed,
true_renamed) →
falseequal_sort[a34](
false_renamed,
false_renamed) →
trueequal_sort[a64](
witness_sort[a64],
witness_sort[a64]) →
trueThe proof given by the theorem prover:The following output was given by the internal theorem prover:
proof of internal
# AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished
Partial correctness of the following Program
[x, v23, v24, v25, v26, v27, v28, v29, v30, v31, n2, x6, xs1, n4, x8, x7, xs2, n5, n3, x', y, x5, n1, n', x3, xs', v14, n, x'', n'', x4]
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
true and x -> x
false and x -> false
true or x -> true
false or x -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v23)) -> false
equal_sort[a0](s(v24), 0) -> false
equal_sort[a0](s(v24), s(v25)) -> equal_sort[a0](v24, v25)
equal_sort[a5](cons(v26, v27), cons(v28, v29)) -> equal_sort[a0](v26, v28) and equal_sort[a5](v27, v29)
equal_sort[a5](cons(v26, v27), nil) -> false
equal_sort[a5](nil, cons(v30, v31)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a34](true_renamed, true_renamed) -> true
equal_sort[a34](true_renamed, false_renamed) -> false
equal_sort[a34](false_renamed, true_renamed) -> false
equal_sort[a34](false_renamed, false_renamed) -> true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) -> true
if2'(true_renamed, n2, x6, xs1) -> true
if2'(false_renamed, n4, x8, cons(x7, xs2)) -> if2'(ge(x7, n4), n4, x7, xs2)
if2'(false_renamed, n4, x8, nil) -> false
filterhigh'(n5, nil) -> false
equal_sort[a34](ge(x7, n3), true_renamed) -> true | filterhigh'(n3, cons(x7, xs2)) -> true
equal_sort[a34](ge(x7, n3), true_renamed) -> false | filterhigh'(n3, cons(x7, xs2)) -> filterhigh'(n3, xs2)
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
ge(0, s(x5)) -> false_renamed
filterlow(n1, nil) -> nil
equal_sort[a34](ge(n', x3), true_renamed) -> true | filterlow(n', cons(x3, xs')) -> filterlow(n', xs')
equal_sort[a34](ge(n', x3), true_renamed) -> false | filterlow(n', cons(x3, xs')) -> cons(x3, filterlow(n', xs'))
half(0) -> 0
half(s(v14)) -> 0
filterhigh(n5, nil) -> nil
equal_sort[a34](ge(x7, n3), true_renamed) -> true | filterhigh(n3, cons(x7, xs2)) -> filterhigh(n3, xs2)
equal_sort[a34](ge(x7, n3), true_renamed) -> false | filterhigh(n3, cons(x7, xs2)) -> cons(x7, filterhigh(n3, xs2))
if1(true_renamed, n, x'', cons(x3, xs')) -> if1(ge(n, x3), n, x3, xs')
if1(true_renamed, n, x'', nil) -> nil
if1(false_renamed, n'', x4, cons(x3, xs')) -> cons(x4, if1(ge(n'', x3), n'', x3, xs'))
if1(false_renamed, n'', x4, nil) -> cons(x4, nil)
if2(true_renamed, n2, x6, cons(x7, xs2)) -> if2(ge(x7, n2), n2, x7, xs2)
if2(true_renamed, n2, x6, nil) -> nil
if2(false_renamed, n4, x8, cons(x7, xs2)) -> cons(x8, if2(ge(x7, n4), n4, x7, xs2))
if2(false_renamed, n4, x8, nil) -> cons(x8, nil)
using the following formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(x0, x0), x0, x0, cons(x1, x2))=true
could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
(3) Formula
(4) Symbolic evaluation [EQUIVALENT, 0 ms]
(5) YES
(6) Formula
(7) Symbolic evaluation [EQUIVALENT, 0 ms]
(8) Formula
(9) Case Analysis [EQUIVALENT, 0 ms]
(10) AND
(11) Formula
(12) Case Analysis [EQUIVALENT, 0 ms]
(13) AND
(14) Formula
(15) Inverse Substitution [SOUND, 0 ms]
(16) Formula
(17) Induction by data structure [SOUND, 0 ms]
(18) AND
(19) Formula
(20) Symbolic evaluation [EQUIVALENT, 0 ms]
(21) YES
(22) Formula
(23) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(24) YES
(25) Formula
(26) Inverse Substitution [SOUND, 0 ms]
(27) Formula
(28) Induction by data structure [SOUND, 0 ms]
(29) AND
(30) Formula
(31) Symbolic evaluation [EQUIVALENT, 0 ms]
(32) YES
(33) Formula
(34) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(35) YES
(36) Formula
(37) Case Analysis [EQUIVALENT, 0 ms]
(38) AND
(39) Formula
(40) Inverse Substitution [SOUND, 0 ms]
(41) Formula
(42) Induction by data structure [SOUND, 0 ms]
(43) AND
(44) Formula
(45) Symbolic evaluation [EQUIVALENT, 0 ms]
(46) YES
(47) Formula
(48) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(49) YES
(50) Formula
(51) Inverse Substitution [SOUND, 0 ms]
(52) Formula
(53) Induction by data structure [SOUND, 0 ms]
(54) AND
(55) Formula
(56) Symbolic evaluation [EQUIVALENT, 0 ms]
(57) YES
(58) Formula
(59) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(60) YES
----------------------------------------
(0)
Obligation:
Formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(x0, x0), x0, x0, cons(x1, x2))=true
There are no hypotheses.
----------------------------------------
(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
x1:sort[a0],x2:sort[a5].if2'(ge(0, 0), 0, 0, cons(x1, x2))=true
There are no hypotheses.
1. Step Case:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(2)
Complex Obligation (AND)
----------------------------------------
(3)
Obligation:
Formula:
x1:sort[a0],x2:sort[a5].if2'(ge(0, 0), 0, 0, cons(x1, x2))=true
There are no hypotheses.
----------------------------------------
(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(5)
YES
----------------------------------------
(6)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------
(8)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(x1, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(9) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:
Formula:
n:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(10)
Complex Obligation (AND)
----------------------------------------
(11)
Obligation:
Formula:
n:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(12) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:
Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
Formula:
n:sort[a0].if2'(ge(n, n), s(n), s(n), cons(0, nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(13)
Complex Obligation (AND)
----------------------------------------
(14)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(15) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(16)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(17) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true
----------------------------------------
(18)
Complex Obligation (AND)
----------------------------------------
(19)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true
There are no hypotheses.
----------------------------------------
(20) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(21)
YES
----------------------------------------
(22)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true
----------------------------------------
(23) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true
----------------------------------------
(24)
YES
----------------------------------------
(25)
Obligation:
Formula:
n:sort[a0].if2'(ge(n, n), s(n), s(n), cons(0, nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(26) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0].if2'(ge(n, n), n', n', cons(0, nil))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(27)
Obligation:
Formula:
n:sort[a0],n':sort[a0].if2'(ge(n, n), n', n', cons(0, nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(28) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0].if2'(ge(0, 0), n', n', cons(0, nil))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', cons(0, nil))=true
----------------------------------------
(29)
Complex Obligation (AND)
----------------------------------------
(30)
Obligation:
Formula:
n':sort[a0].if2'(ge(0, 0), n', n', cons(0, nil))=true
There are no hypotheses.
----------------------------------------
(31) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(32)
YES
----------------------------------------
(33)
Obligation:
Formula:
n'':sort[a0],n':sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', cons(0, nil))=true
----------------------------------------
(34) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0].if2'(ge(n'', n''), n', n', cons(0, nil))=true
----------------------------------------
(35)
YES
----------------------------------------
(36)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(37) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:
Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
Formula:
n:sort[a0],x_1:sort[a0].if2'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(38)
Complex Obligation (AND)
----------------------------------------
(39)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(40) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(41)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(42) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true
----------------------------------------
(43)
Complex Obligation (AND)
----------------------------------------
(44)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true
There are no hypotheses.
----------------------------------------
(45) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(46)
YES
----------------------------------------
(47)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true
----------------------------------------
(48) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if2'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true
----------------------------------------
(49)
YES
----------------------------------------
(50)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0].if2'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(51) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(n, n), n', n', cons(s(x_1), nil))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(52)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(n, n), n', n', cons(s(x_1), nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if2'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(53) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0].if2'(ge(0, 0), n', n', cons(s(x_1), nil))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if2'(ge(n'', n''), n', n', cons(s(x_1), nil))=true
----------------------------------------
(54)
Complex Obligation (AND)
----------------------------------------
(55)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0].if2'(ge(0, 0), n', n', cons(s(x_1), nil))=true
There are no hypotheses.
----------------------------------------
(56) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(57)
YES
----------------------------------------
(58)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if2'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if2'(ge(n'', n''), n', n', cons(s(x_1), nil))=true
----------------------------------------
(59) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if2'(ge(n'', n''), n', n', cons(s(x_1), nil))=true
----------------------------------------
(60)
YES
(119) Complex Obligation (AND)
(120) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(121) 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.
(122) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(123) 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].
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
(124) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(x0, cons(x1, nil)) → QS(half(x0), if1(ge(x1, x1), x1, x1, nil))
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(125) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:QS(
x0,
cons(
x1,
nil)) →
QS(
half(
x0),
if1(
ge(
x1,
x1),
x1,
x1,
nil))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 1
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false_renamed) = 1
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(half(x1)) = 1
POL(if1(x1, x2, x3, x4)) = x1 + x4
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true_renamed) = 1
At least one of these decreasing rules is always used after the deleted DP:if1(
true_renamed,
n,
x'',
xs) →
filterlow(
n,
xs)
The following formula is valid:x1:sort[a0].
if1'(
ge(
x1 ,
x1 ),
x1 ,
x1 ,
nil)=
trueThe transformed set:if1'(
true_renamed,
n,
x'',
xs) →
trueif1'(
false_renamed,
n',
x3,
xs') →
filterlow'(
n',
xs')
filterlow'(
n'',
nil) →
falsefilterlow'(
n1,
cons(
x5,
xs'')) →
if1'(
ge(
n1,
x5),
n1,
x5,
xs'')
ge(
x,
0) →
true_renamedge(
s(
x'),
s(
y)) →
ge(
x',
y)
if1(
true_renamed,
n,
x'',
xs) →
filterlow(
n,
xs)
if1(
false_renamed,
n',
x3,
xs') →
cons(
x3,
filterlow(
n',
xs'))
filterlow(
n'',
nil) →
nilge(
0,
s(
x4)) →
false_renamedhalf(
0) →
0filterlow(
n1,
cons(
x5,
xs'')) →
if1(
ge(
n1,
x5),
n1,
x5,
xs'')
half(
s(
v14)) →
0equal_bool(
true,
false) →
falseequal_bool(
false,
true) →
falseequal_bool(
true,
true) →
trueequal_bool(
false,
false) →
trueand(
true,
x) →
xand(
false,
x) →
falseor(
true,
x) →
trueor(
false,
x) →
xnot(
false) →
truenot(
true) →
falseisa_true(
true) →
trueisa_true(
false) →
falseisa_false(
true) →
falseisa_false(
false) →
trueequal_sort[a0](
0,
0) →
trueequal_sort[a0](
0,
s(
v15)) →
falseequal_sort[a0](
s(
v16),
0) →
falseequal_sort[a0](
s(
v16),
s(
v17)) →
equal_sort[a0](
v16,
v17)
equal_sort[a5](
cons(
v18,
v19),
cons(
v20,
v21)) →
and(
equal_sort[a0](
v18,
v20),
equal_sort[a5](
v19,
v21))
equal_sort[a5](
cons(
v18,
v19),
nil) →
falseequal_sort[a5](
nil,
cons(
v22,
v23)) →
falseequal_sort[a5](
nil,
nil) →
trueequal_sort[a21](
true_renamed,
true_renamed) →
trueequal_sort[a21](
true_renamed,
false_renamed) →
falseequal_sort[a21](
false_renamed,
true_renamed) →
falseequal_sort[a21](
false_renamed,
false_renamed) →
trueequal_sort[a43](
witness_sort[a43],
witness_sort[a43]) →
trueThe proof given by the theorem prover:The following output was given by the internal theorem prover:
proof of internal
# AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished
Partial correctness of the following Program
[x, v15, v16, v17, v18, v19, v20, v21, v22, v23, n, x'', xs, n', x3, x5, xs'', n'', n1, x', y, x4, v14]
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
true and x -> x
false and x -> false
true or x -> true
false or x -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v15)) -> false
equal_sort[a0](s(v16), 0) -> false
equal_sort[a0](s(v16), s(v17)) -> equal_sort[a0](v16, v17)
equal_sort[a5](cons(v18, v19), cons(v20, v21)) -> equal_sort[a0](v18, v20) and equal_sort[a5](v19, v21)
equal_sort[a5](cons(v18, v19), nil) -> false
equal_sort[a5](nil, cons(v22, v23)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a21](true_renamed, true_renamed) -> true
equal_sort[a21](true_renamed, false_renamed) -> false
equal_sort[a21](false_renamed, true_renamed) -> false
equal_sort[a21](false_renamed, false_renamed) -> true
equal_sort[a43](witness_sort[a43], witness_sort[a43]) -> true
if1'(true_renamed, n, x'', xs) -> true
if1'(false_renamed, n', x3, nil) -> false
if1'(false_renamed, n', x3, cons(x5, xs'')) -> if1'(ge(n', x5), n', x5, xs'')
filterlow'(n'', nil) -> false
equal_sort[a21](ge(n1, x5), true_renamed) -> true | filterlow'(n1, cons(x5, xs'')) -> true
equal_sort[a21](ge(n1, x5), true_renamed) -> false | filterlow'(n1, cons(x5, xs'')) -> filterlow'(n1, xs'')
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
ge(0, s(x4)) -> false_renamed
filterlow(n'', nil) -> nil
equal_sort[a21](ge(n1, x5), true_renamed) -> true | filterlow(n1, cons(x5, xs'')) -> filterlow(n1, xs'')
equal_sort[a21](ge(n1, x5), true_renamed) -> false | filterlow(n1, cons(x5, xs'')) -> cons(x5, filterlow(n1, xs''))
half(0) -> 0
half(s(v14)) -> 0
if1(true_renamed, n, x'', nil) -> nil
if1(true_renamed, n, x'', cons(x5, xs'')) -> if1(ge(n, x5), n, x5, xs'')
if1(false_renamed, n', x3, nil) -> cons(x3, nil)
if1(false_renamed, n', x3, cons(x5, xs'')) -> cons(x3, if1(ge(n', x5), n', x5, xs''))
using the following formula:
x1:sort[a0].if1'(ge(x1, x1), x1, x1, nil)=true
could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
(3) Formula
(4) Symbolic evaluation [EQUIVALENT, 0 ms]
(5) YES
(6) Formula
(7) Symbolic evaluation [EQUIVALENT, 0 ms]
(8) Formula
(9) Hypothesis Lifting [EQUIVALENT, 0 ms]
(10) Formula
(11) Inverse Substitution [SOUND, 0 ms]
(12) Formula
(13) Inverse Substitution [SOUND, 0 ms]
(14) Formula
(15) Induction by data structure [EQUIVALENT, 0 ms]
(16) AND
(17) Formula
(18) Symbolic evaluation [EQUIVALENT, 0 ms]
(19) YES
(20) Formula
(21) Symbolic evaluation [EQUIVALENT, 0 ms]
(22) YES
----------------------------------------
(0)
Obligation:
Formula:
x1:sort[a0].if1'(ge(x1, x1), x1, x1, nil)=true
There are no hypotheses.
----------------------------------------
(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
if1'(ge(0, 0), 0, 0, nil)=true
There are no hypotheses.
1. Step Case:
Formula:
n:sort[a0].if1'(ge(s(n), s(n)), s(n), s(n), nil)=true
Hypotheses:
n:sort[a0].if1'(ge(n, n), n, n, nil)=true
----------------------------------------
(2)
Complex Obligation (AND)
----------------------------------------
(3)
Obligation:
Formula:
if1'(ge(0, 0), 0, 0, nil)=true
There are no hypotheses.
----------------------------------------
(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(5)
YES
----------------------------------------
(6)
Obligation:
Formula:
n:sort[a0].if1'(ge(s(n), s(n)), s(n), s(n), nil)=true
Hypotheses:
n:sort[a0].if1'(ge(n, n), n, n, nil)=true
----------------------------------------
(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------
(8)
Obligation:
Formula:
n:sort[a0].if1'(ge(n, n), s(n), s(n), nil)=true
Hypotheses:
n:sort[a0].if1'(ge(n, n), n, n, nil)=true
----------------------------------------
(9) Hypothesis Lifting (EQUIVALENT)
Formula could be generalised by hypothesis lifting to the following new obligation:
Formula:
n:sort[a0].(if1'(ge(n, n), n, n, nil)=true->if1'(ge(n, n), s(n), s(n), nil)=true)
There are no hypotheses.
----------------------------------------
(10)
Obligation:
Formula:
n:sort[a0].(if1'(ge(n, n), n, n, nil)=true->if1'(ge(n, n), s(n), s(n), nil)=true)
There are no hypotheses.
----------------------------------------
(11) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a21],n:sort[a0].(if1'(n', n, n, nil)=true->if1'(n', s(n), s(n), nil)=true)
Inverse substitution used:
[ge(n, n)/n']
----------------------------------------
(12)
Obligation:
Formula:
n':sort[a21],n:sort[a0].(if1'(n', n, n, nil)=true->if1'(n', s(n), s(n), nil)=true)
There are no hypotheses.
----------------------------------------
(13) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n':sort[a21],n:sort[a0],n'':sort[a0].(if1'(n', n, n, nil)=true->if1'(n', n'', n'', nil)=true)
Inverse substitution used:
[s(n)/n'']
----------------------------------------
(14)
Obligation:
Formula:
n':sort[a21],n:sort[a0],n'':sort[a0].(if1'(n', n, n, nil)=true->if1'(n', n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(15) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a21] generates the following cases:
1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if1'(true_renamed, n, n, nil)=true->if1'(true_renamed, n'', n'', nil)=true)
There are no hypotheses.
1. Base Case:
Formula:
n:sort[a0],n'':sort[a0].(if1'(false_renamed, n, n, nil)=true->if1'(false_renamed, n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(16)
Complex Obligation (AND)
----------------------------------------
(17)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if1'(true_renamed, n, n, nil)=true->if1'(true_renamed, n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(18) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(19)
YES
----------------------------------------
(20)
Obligation:
Formula:
n:sort[a0],n'':sort[a0].(if1'(false_renamed, n, n, nil)=true->if1'(false_renamed, n'', n'', nil)=true)
There are no hypotheses.
----------------------------------------
(21) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(22)
YES
(126) Complex Obligation (AND)
(127) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
half(0) → 0
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(128) 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.
(129) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
half(0)
half(s(0))
half(s(s(x0)))
We have to consider all minimal (P,Q,R)-chains.
(130) 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].
half(0)
half(s(0))
half(s(s(x0)))
(131) Obligation:
Q DP problem:
The TRS P consists of the following rules:
QS(0, cons(x0, cons(x1, x2))) → QS(0, if1(ge(x0, x0), x0, x0, cons(x1, x2)))
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(132) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:QS(
0,
cons(
x0,
cons(
x1,
x2))) →
QS(
0,
if1(
ge(
x0,
x0),
x0,
x0,
cons(
x1,
x2)))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 1
POL(QS(x1, x2)) = x2
POL(cons(x1, x2)) = 1 + x2
POL(false_renamed) = 1
POL(filterlow(x1, x2)) = x2
POL(ge(x1, x2)) = 1
POL(if1(x1, x2, x3, x4)) = x1 + x4
POL(nil) = 0
POL(s(x1)) = x1
POL(true_renamed) = 1
At least one of these decreasing rules is always used after the deleted DP:if1(
true_renamed,
n,
x'',
xs) →
filterlow(
n,
xs)
The following formula is valid:x0:sort[a0],x1:sort[a0],x2:sort[a5].
if1'(
ge(
x0 ,
x0 ),
x0 ,
x0 ,
cons(
x1 ,
x2 ))=
trueThe transformed set:if1'(
true_renamed,
n,
x'',
xs) →
truefilterlow'(
n',
cons(
x3,
xs')) →
if1'(
ge(
n',
x3),
n',
x3,
xs')
if1'(
false_renamed,
n'',
x4,
xs'') →
filterlow'(
n'',
xs'')
filterlow'(
n1,
nil) →
falsege(
x,
0) →
true_renamedge(
s(
x'),
s(
y)) →
ge(
x',
y)
if1(
true_renamed,
n,
x'',
xs) →
filterlow(
n,
xs)
filterlow(
n',
cons(
x3,
xs')) →
if1(
ge(
n',
x3),
n',
x3,
xs')
if1(
false_renamed,
n'',
x4,
xs'') →
cons(
x4,
filterlow(
n'',
xs''))
filterlow(
n1,
nil) →
nilge(
0,
s(
x5)) →
false_renamedequal_bool(
true,
false) →
falseequal_bool(
false,
true) →
falseequal_bool(
true,
true) →
trueequal_bool(
false,
false) →
trueand(
true,
x) →
xand(
false,
x) →
falseor(
true,
x) →
trueor(
false,
x) →
xnot(
false) →
truenot(
true) →
falseisa_true(
true) →
trueisa_true(
false) →
falseisa_false(
true) →
falseisa_false(
false) →
trueequal_sort[a0](
0,
0) →
trueequal_sort[a0](
0,
s(
v13)) →
falseequal_sort[a0](
s(
v14),
0) →
falseequal_sort[a0](
s(
v14),
s(
v15)) →
equal_sort[a0](
v14,
v15)
equal_sort[a5](
cons(
v16,
v17),
cons(
v18,
v19)) →
and(
equal_sort[a0](
v16,
v18),
equal_sort[a5](
v17,
v19))
equal_sort[a5](
cons(
v16,
v17),
nil) →
falseequal_sort[a5](
nil,
cons(
v20,
v21)) →
falseequal_sort[a5](
nil,
nil) →
trueequal_sort[a19](
true_renamed,
true_renamed) →
trueequal_sort[a19](
true_renamed,
false_renamed) →
falseequal_sort[a19](
false_renamed,
true_renamed) →
falseequal_sort[a19](
false_renamed,
false_renamed) →
trueequal_sort[a39](
witness_sort[a39],
witness_sort[a39]) →
trueThe proof given by the theorem prover:The following output was given by the internal theorem prover:
proof of internal
# AProVE Commit ID: 3a20a6ef7432c3f292db1a8838479c42bf5e3b22 root 20240618 unpublished
Partial correctness of the following Program
[x, v13, v14, v15, v16, v17, v18, v19, v20, v21, n, x'', xs, n'', x4, x3, xs', n1, n', x', y, x5]
equal_bool(true, false) -> false
equal_bool(false, true) -> false
equal_bool(true, true) -> true
equal_bool(false, false) -> true
true and x -> x
false and x -> false
true or x -> true
false or x -> x
not(false) -> true
not(true) -> false
isa_true(true) -> true
isa_true(false) -> false
isa_false(true) -> false
isa_false(false) -> true
equal_sort[a0](0, 0) -> true
equal_sort[a0](0, s(v13)) -> false
equal_sort[a0](s(v14), 0) -> false
equal_sort[a0](s(v14), s(v15)) -> equal_sort[a0](v14, v15)
equal_sort[a5](cons(v16, v17), cons(v18, v19)) -> equal_sort[a0](v16, v18) and equal_sort[a5](v17, v19)
equal_sort[a5](cons(v16, v17), nil) -> false
equal_sort[a5](nil, cons(v20, v21)) -> false
equal_sort[a5](nil, nil) -> true
equal_sort[a19](true_renamed, true_renamed) -> true
equal_sort[a19](true_renamed, false_renamed) -> false
equal_sort[a19](false_renamed, true_renamed) -> false
equal_sort[a19](false_renamed, false_renamed) -> true
equal_sort[a39](witness_sort[a39], witness_sort[a39]) -> true
if1'(true_renamed, n, x'', xs) -> true
if1'(false_renamed, n'', x4, cons(x3, xs')) -> if1'(ge(n'', x3), n'', x3, xs')
if1'(false_renamed, n'', x4, nil) -> false
filterlow'(n1, nil) -> false
equal_sort[a19](ge(n', x3), true_renamed) -> true | filterlow'(n', cons(x3, xs')) -> true
equal_sort[a19](ge(n', x3), true_renamed) -> false | filterlow'(n', cons(x3, xs')) -> filterlow'(n', xs')
ge(x, 0) -> true_renamed
ge(s(x'), s(y)) -> ge(x', y)
ge(0, s(x5)) -> false_renamed
filterlow(n1, nil) -> nil
equal_sort[a19](ge(n', x3), true_renamed) -> true | filterlow(n', cons(x3, xs')) -> filterlow(n', xs')
equal_sort[a19](ge(n', x3), true_renamed) -> false | filterlow(n', cons(x3, xs')) -> cons(x3, filterlow(n', xs'))
if1(true_renamed, n, x'', cons(x3, xs')) -> if1(ge(n, x3), n, x3, xs')
if1(true_renamed, n, x'', nil) -> nil
if1(false_renamed, n'', x4, cons(x3, xs')) -> cons(x4, if1(ge(n'', x3), n'', x3, xs'))
if1(false_renamed, n'', x4, nil) -> cons(x4, nil)
using the following formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(x0, x0), x0, x0, cons(x1, x2))=true
could be successfully shown:
(0) Formula
(1) Induction by data structure [EQUIVALENT, 0 ms]
(2) AND
(3) Formula
(4) Symbolic evaluation [EQUIVALENT, 0 ms]
(5) YES
(6) Formula
(7) Symbolic evaluation [EQUIVALENT, 0 ms]
(8) Formula
(9) Case Analysis [EQUIVALENT, 0 ms]
(10) AND
(11) Formula
(12) Case Analysis [EQUIVALENT, 0 ms]
(13) AND
(14) Formula
(15) Inverse Substitution [SOUND, 0 ms]
(16) Formula
(17) Induction by data structure [SOUND, 0 ms]
(18) AND
(19) Formula
(20) Symbolic evaluation [EQUIVALENT, 0 ms]
(21) YES
(22) Formula
(23) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(24) YES
(25) Formula
(26) Inverse Substitution [SOUND, 0 ms]
(27) Formula
(28) Induction by data structure [SOUND, 0 ms]
(29) AND
(30) Formula
(31) Symbolic evaluation [EQUIVALENT, 0 ms]
(32) YES
(33) Formula
(34) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(35) YES
(36) Formula
(37) Case Analysis [EQUIVALENT, 0 ms]
(38) AND
(39) Formula
(40) Inverse Substitution [SOUND, 0 ms]
(41) Formula
(42) Induction by data structure [SOUND, 0 ms]
(43) AND
(44) Formula
(45) Symbolic evaluation [EQUIVALENT, 0 ms]
(46) YES
(47) Formula
(48) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(49) YES
(50) Formula
(51) Inverse Substitution [SOUND, 0 ms]
(52) Formula
(53) Induction by data structure [SOUND, 0 ms]
(54) AND
(55) Formula
(56) Symbolic evaluation [EQUIVALENT, 0 ms]
(57) YES
(58) Formula
(59) Symbolic evaluation under hypothesis [EQUIVALENT, 0 ms]
(60) YES
----------------------------------------
(0)
Obligation:
Formula:
x0:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(x0, x0), x0, x0, cons(x1, x2))=true
There are no hypotheses.
----------------------------------------
(1) Induction by data structure (EQUIVALENT)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
x1:sort[a0],x2:sort[a5].if1'(ge(0, 0), 0, 0, cons(x1, x2))=true
There are no hypotheses.
1. Step Case:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(2)
Complex Obligation (AND)
----------------------------------------
(3)
Obligation:
Formula:
x1:sort[a0],x2:sort[a5].if1'(ge(0, 0), 0, 0, cons(x1, x2))=true
There are no hypotheses.
----------------------------------------
(4) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(5)
YES
----------------------------------------
(6)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(s(n), s(n)), s(n), s(n), cons(x1, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(7) Symbolic evaluation (EQUIVALENT)
Could be shown by simple symbolic evaluation.
----------------------------------------
(8)
Obligation:
Formula:
n:sort[a0],x1:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(x1, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(9) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:
Formula:
n:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(10)
Complex Obligation (AND)
----------------------------------------
(11)
Obligation:
Formula:
n:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(12) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:
Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
Formula:
n:sort[a0].if1'(ge(n, n), s(n), s(n), cons(0, nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(13)
Complex Obligation (AND)
----------------------------------------
(14)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(0, cons(x_1, x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(15) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(16)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(0, cons(x_1, x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(17) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true
----------------------------------------
(18)
Complex Obligation (AND)
----------------------------------------
(19)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(0, cons(x_1, x_2)))=true
There are no hypotheses.
----------------------------------------
(20) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(21)
YES
----------------------------------------
(22)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(0, cons(x_1, x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true
----------------------------------------
(23) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(0, cons(x_1, x_2)))=true
----------------------------------------
(24)
YES
----------------------------------------
(25)
Obligation:
Formula:
n:sort[a0].if1'(ge(n, n), s(n), s(n), cons(0, nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(26) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0].if1'(ge(n, n), n', n', cons(0, nil))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(27)
Obligation:
Formula:
n:sort[a0],n':sort[a0].if1'(ge(n, n), n', n', cons(0, nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(28) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0].if1'(ge(0, 0), n', n', cons(0, nil))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', cons(0, nil))=true
----------------------------------------
(29)
Complex Obligation (AND)
----------------------------------------
(30)
Obligation:
Formula:
n':sort[a0].if1'(ge(0, 0), n', n', cons(0, nil))=true
There are no hypotheses.
----------------------------------------
(31) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(32)
YES
----------------------------------------
(33)
Obligation:
Formula:
n'':sort[a0],n':sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(0, nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', cons(0, nil))=true
----------------------------------------
(34) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0].if1'(ge(n'', n''), n', n', cons(0, nil))=true
----------------------------------------
(35)
YES
----------------------------------------
(36)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), x2))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(37) Case Analysis (EQUIVALENT)
Case analysis leads to the following new obligations:
Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
Formula:
n:sort[a0],x_1:sort[a0].if1'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(38)
Complex Obligation (AND)
----------------------------------------
(39)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), s(n), s(n), cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(40) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(41)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(n, n), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(42) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true
----------------------------------------
(43)
Complex Obligation (AND)
----------------------------------------
(44)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(0, 0), n', n', cons(s(x_1), cons(x_1', x_2)))=true
There are no hypotheses.
----------------------------------------
(45) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(46)
YES
----------------------------------------
(47)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0],x_1':sort[a0],x_2:sort[a5].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), cons(x_1', x_2)))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true
----------------------------------------
(48) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0],!x_1':sort[a0],!x_2:sort[a5].if1'(ge(n'', n''), n', n', cons(s(x_1), cons(x_1', x_2)))=true
----------------------------------------
(49)
YES
----------------------------------------
(50)
Obligation:
Formula:
n:sort[a0],x_1:sort[a0].if1'(ge(n, n), s(n), s(n), cons(s(x_1), nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(51) Inverse Substitution (SOUND)
The formula could be generalised by inverse substitution to:
n:sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(n, n), n', n', cons(s(x_1), nil))=true
Inverse substitution used:
[s(n)/n']
----------------------------------------
(52)
Obligation:
Formula:
n:sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(n, n), n', n', cons(s(x_1), nil))=true
Hypotheses:
n:sort[a0],!x1:sort[a0],!x2:sort[a5].if1'(ge(n, n), n, n, cons(x1, x2))=true
----------------------------------------
(53) Induction by data structure (SOUND)
Induction by data structure sort[a0] generates the following cases:
1. Base Case:
Formula:
n':sort[a0],x_1:sort[a0].if1'(ge(0, 0), n', n', cons(s(x_1), nil))=true
There are no hypotheses.
1. Step Case:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if1'(ge(n'', n''), n', n', cons(s(x_1), nil))=true
----------------------------------------
(54)
Complex Obligation (AND)
----------------------------------------
(55)
Obligation:
Formula:
n':sort[a0],x_1:sort[a0].if1'(ge(0, 0), n', n', cons(s(x_1), nil))=true
There are no hypotheses.
----------------------------------------
(56) Symbolic evaluation (EQUIVALENT)
Could be reduced to the following new obligation by simple symbolic evaluation:
True
----------------------------------------
(57)
YES
----------------------------------------
(58)
Obligation:
Formula:
n'':sort[a0],n':sort[a0],x_1:sort[a0].if1'(ge(s(n''), s(n'')), n', n', cons(s(x_1), nil))=true
Hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if1'(ge(n'', n''), n', n', cons(s(x_1), nil))=true
----------------------------------------
(59) Symbolic evaluation under hypothesis (EQUIVALENT)
Could be shown using symbolic evaluation under hypothesis, by using the following hypotheses:
n'':sort[a0],!n':sort[a0],!x_1:sort[a0].if1'(ge(n'', n''), n', n', cons(s(x_1), nil))=true
----------------------------------------
(60)
YES
(133) Complex Obligation (AND)
(134) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false
The set Q consists of the following terms:
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
We have to consider all minimal (P,Q,R)-chains.
(135) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(136) YES
(137) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
if1'(true_renamed, n, x'', xs) → true
filterlow'(n', cons(x3, xs')) → if1'(ge(n', x3), n', x3, xs')
if1'(false_renamed, n'', x4, xs'') → filterlow'(n'', xs'')
filterlow'(n1, nil) → false
ge(x, 0) → true_renamed
ge(s(x'), s(y)) → ge(x', y)
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
filterlow(n', cons(x3, xs')) → if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') → cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) → nil
ge(0, s(x5)) → false_renamed
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v13)) → false
equal_sort[a0](s(v14), 0) → false
equal_sort[a0](s(v14), s(v15)) → equal_sort[a0](v14, v15)
equal_sort[a5](cons(v16, v17), cons(v18, v19)) → and(equal_sort[a0](v16, v18), equal_sort[a5](v17, v19))
equal_sort[a5](cons(v16, v17), nil) → false
equal_sort[a5](nil, cons(v20, v21)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a19](true_renamed, true_renamed) → true
equal_sort[a19](true_renamed, false_renamed) → false
equal_sort[a19](false_renamed, true_renamed) → false
equal_sort[a19](false_renamed, false_renamed) → true
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
Q is empty.
(138) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
if1'(
x1,
x2,
x3,
x4) =
if1'(
x1,
x2,
x3,
x4)
true_renamed =
true_renamed
true =
true
filterlow'(
x1,
x2) =
filterlow'(
x1,
x2)
cons(
x1,
x2) =
cons(
x1,
x2)
ge(
x1,
x2) =
ge(
x1,
x2)
false_renamed =
false_renamed
nil =
nil
false =
false
0 =
0
s(
x1) =
s(
x1)
if1(
x1,
x2,
x3,
x4) =
if1(
x1,
x2,
x3,
x4)
filterlow(
x1,
x2) =
filterlow(
x1,
x2)
equal_bool(
x1,
x2) =
equal_bool(
x1,
x2)
and(
x1,
x2) =
and(
x1,
x2)
or(
x1,
x2) =
or(
x1,
x2)
not(
x1) =
not(
x1)
isa_true(
x1) =
x1
isa_false(
x1) =
isa_false(
x1)
equal_sort[a0](
x1,
x2) =
equal_sort[a0](
x1,
x2)
equal_sort[a5](
x1,
x2) =
equal_sort[a5](
x1,
x2)
equal_sort[a19](
x1,
x2) =
equal_sort[a19](
x1,
x2)
equal_sort[a39](
x1,
x2) =
equal_sort[a39](
x1,
x2)
witness_sort[a39] =
witness_sort[a39]
Recursive path order with status [RPO].
Quasi-Precedence:
[truerenamed, 0] > [nil, false, if14, filterlow2, isafalse1] > [if1'4, true, filterlow'2, equalsort[a39]2, witnesssort[a39]] > ge2
[truerenamed, 0] > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > ge2
[truerenamed, 0] > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > and2
[truerenamed, 0] > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > equalsort[a0]2
s1 > ge2
s1 > equalsort[a0]2
or2 > [if1'4, true, filterlow'2, equalsort[a39]2, witnesssort[a39]] > ge2
not1 > [nil, false, if14, filterlow2, isafalse1] > [if1'4, true, filterlow'2, equalsort[a39]2, witnesssort[a39]] > ge2
not1 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > ge2
not1 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > and2
not1 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > equalsort[a0]2
equalsort[a5]2 > [nil, false, if14, filterlow2, isafalse1] > [if1'4, true, filterlow'2, equalsort[a39]2, witnesssort[a39]] > ge2
equalsort[a5]2 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > ge2
equalsort[a5]2 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > and2
equalsort[a5]2 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > equalsort[a0]2
equalsort[a19]2 > [nil, false, if14, filterlow2, isafalse1] > [if1'4, true, filterlow'2, equalsort[a39]2, witnesssort[a39]] > ge2
equalsort[a19]2 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > ge2
equalsort[a19]2 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > and2
equalsort[a19]2 > [nil, false, if14, filterlow2, isafalse1] > [cons2, falserenamed] > equalsort[a0]2
Status:
if1'4: [4,2,3,1]
truerenamed: multiset
true: multiset
filterlow'2: [2,1]
cons2: multiset
ge2: multiset
falserenamed: multiset
nil: multiset
false: multiset
0: multiset
s1: multiset
if14: [2,4,3,1]
filterlow2: [1,2]
equalbool2: [1,2]
and2: multiset
or2: multiset
not1: [1]
isafalse1: [1]
equalsort[a0]2: multiset
equalsort[a5]2: multiset
equalsort[a19]2: [1,2]
equalsort[a39]2: [1,2]
witnesssort[a39]: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
if1'(true_renamed, n, x'', xs) → true
filterlow'(n', cons(x3, xs')) → if1'(ge(n', x3), n', x3, xs')
if1'(false_renamed, n'', x4, xs'') → filterlow'(n'', xs'')
filterlow'(n1, nil) → false
ge(x, 0) → true_renamed
ge(s(x'), s(y)) → ge(x', y)
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
filterlow(n', cons(x3, xs')) → if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') → cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) → nil
ge(0, s(x5)) → false_renamed
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v13)) → false
equal_sort[a0](s(v14), 0) → false
equal_sort[a0](s(v14), s(v15)) → equal_sort[a0](v14, v15)
equal_sort[a5](cons(v16, v17), cons(v18, v19)) → and(equal_sort[a0](v16, v18), equal_sort[a5](v17, v19))
equal_sort[a5](cons(v16, v17), nil) → false
equal_sort[a5](nil, cons(v20, v21)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a19](true_renamed, true_renamed) → true
equal_sort[a19](true_renamed, false_renamed) → false
equal_sort[a19](false_renamed, true_renamed) → false
equal_sort[a19](false_renamed, false_renamed) → true
equal_sort[a39](witness_sort[a39], witness_sort[a39]) → true
(139) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
isa_true(true) → true
isa_true(false) → false
Q is empty.
(140) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Knuth-Bendix order [KBO] with precedence:
isatrue1 > false > true
and weight map:
true=1
false=1
isa_true_1=0
The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
isa_true(true) → true
isa_true(false) → false
(141) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(142) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(143) YES
(144) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
if1'(true_renamed, n, x'', xs) → true
if1'(false_renamed, n', x3, xs') → filterlow'(n', xs')
filterlow'(n'', nil) → false
filterlow'(n1, cons(x5, xs'')) → if1'(ge(n1, x5), n1, x5, xs'')
ge(x, 0) → true_renamed
ge(s(x'), s(y)) → ge(x', y)
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
if1(false_renamed, n', x3, xs') → cons(x3, filterlow(n', xs'))
filterlow(n'', nil) → nil
ge(0, s(x4)) → false_renamed
half(0) → 0
filterlow(n1, cons(x5, xs'')) → if1(ge(n1, x5), n1, x5, xs'')
half(s(v14)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v15)) → false
equal_sort[a0](s(v16), 0) → false
equal_sort[a0](s(v16), s(v17)) → equal_sort[a0](v16, v17)
equal_sort[a5](cons(v18, v19), cons(v20, v21)) → and(equal_sort[a0](v18, v20), equal_sort[a5](v19, v21))
equal_sort[a5](cons(v18, v19), nil) → false
equal_sort[a5](nil, cons(v22, v23)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a21](true_renamed, true_renamed) → true
equal_sort[a21](true_renamed, false_renamed) → false
equal_sort[a21](false_renamed, true_renamed) → false
equal_sort[a21](false_renamed, false_renamed) → true
equal_sort[a43](witness_sort[a43], witness_sort[a43]) → true
Q is empty.
(145) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
if1'(
x1,
x2,
x3,
x4) =
if1'(
x1,
x2,
x3,
x4)
true_renamed =
true_renamed
true =
true
false_renamed =
false_renamed
filterlow'(
x1,
x2) =
filterlow'(
x1,
x2)
nil =
nil
false =
false
cons(
x1,
x2) =
cons(
x1,
x2)
ge(
x1,
x2) =
ge(
x1,
x2)
0 =
0
s(
x1) =
x1
if1(
x1,
x2,
x3,
x4) =
if1(
x1,
x2,
x3,
x4)
filterlow(
x1,
x2) =
filterlow(
x1,
x2)
half(
x1) =
half(
x1)
equal_bool(
x1,
x2) =
equal_bool(
x1,
x2)
and(
x1,
x2) =
and(
x1,
x2)
or(
x1,
x2) =
or(
x1,
x2)
not(
x1) =
not(
x1)
isa_true(
x1) =
isa_true(
x1)
isa_false(
x1) =
isa_false(
x1)
equal_sort[a0](
x1,
x2) =
equal_sort[a0](
x1,
x2)
equal_sort[a5](
x1,
x2) =
equal_sort[a5](
x1,
x2)
equal_sort[a21](
x1,
x2) =
equal_sort[a21](
x1,
x2)
equal_sort[a43](
x1,
x2) =
equal_sort[a43](
x1,
x2)
witness_sort[a43] =
witness_sort[a43]
Recursive path order with status [RPO].
Quasi-Precedence:
[if14, filterlow2] > nil > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
[if14, filterlow2] > nil > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
[if14, filterlow2] > cons2 > [if1'4, filterlow'2] > ge2 > [falserenamed, 0] > truerenamed > [false, isatrue1]
[if14, filterlow2] > cons2 > [if1'4, filterlow'2] > ge2 > [falserenamed, 0] > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
[if14, filterlow2] > cons2 > [if1'4, filterlow'2] > ge2 > [falserenamed, 0] > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
half1 > [falserenamed, 0] > truerenamed > [false, isatrue1]
half1 > [falserenamed, 0] > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
half1 > [falserenamed, 0] > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
equalbool2 > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
equalbool2 > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
or2 > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
or2 > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
isafalse1 > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
isafalse1 > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
equalsort[a21]2 > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
equalsort[a21]2 > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
equalsort[a43]2 > [false, isatrue1]
witnesssort[a43] > [true, not1, equalsort[a5]2] > and2 > [false, isatrue1]
witnesssort[a43] > [true, not1, equalsort[a5]2] > equalsort[a0]2 > [false, isatrue1]
Status:
if1'4: [2,4,1,3]
truerenamed: multiset
true: multiset
falserenamed: multiset
filterlow'2: [1,2]
nil: multiset
false: multiset
cons2: multiset
ge2: multiset
0: multiset
if14: [4,2,1,3]
filterlow2: [2,1]
half1: multiset
equalbool2: [1,2]
and2: multiset
or2: multiset
not1: multiset
isatrue1: [1]
isafalse1: [1]
equalsort[a0]2: multiset
equalsort[a5]2: [1,2]
equalsort[a21]2: [1,2]
equalsort[a43]2: [1,2]
witnesssort[a43]: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
if1'(true_renamed, n, x'', xs) → true
if1'(false_renamed, n', x3, xs') → filterlow'(n', xs')
filterlow'(n'', nil) → false
filterlow'(n1, cons(x5, xs'')) → if1'(ge(n1, x5), n1, x5, xs'')
ge(x, 0) → true_renamed
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
if1(false_renamed, n', x3, xs') → cons(x3, filterlow(n', xs'))
filterlow(n'', nil) → nil
ge(0, s(x4)) → false_renamed
half(0) → 0
filterlow(n1, cons(x5, xs'')) → if1(ge(n1, x5), n1, x5, xs'')
half(s(v14)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v15)) → false
equal_sort[a0](s(v16), 0) → false
equal_sort[a5](cons(v18, v19), cons(v20, v21)) → and(equal_sort[a0](v18, v20), equal_sort[a5](v19, v21))
equal_sort[a5](cons(v18, v19), nil) → false
equal_sort[a5](nil, cons(v22, v23)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a21](true_renamed, true_renamed) → true
equal_sort[a21](true_renamed, false_renamed) → false
equal_sort[a21](false_renamed, true_renamed) → false
equal_sort[a21](false_renamed, false_renamed) → true
equal_sort[a43](witness_sort[a43], witness_sort[a43]) → true
(146) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
ge(s(x'), s(y)) → ge(x', y)
equal_sort[a0](s(v16), s(v17)) → equal_sort[a0](v16, v17)
Q is empty.
(147) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Knuth-Bendix order [KBO] with precedence:
s1 > equalsort[a0]2 > ge2
and weight map:
s_1=0
ge_2=0
equal_sort[a0]_2=0
The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
ge(s(x'), s(y)) → ge(x', y)
equal_sort[a0](s(v16), s(v17)) → equal_sort[a0](v16, v17)
(148) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(149) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(150) YES
(151) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
if2'(true_renamed, n2, x6, xs1) → true
filterhigh'(n3, cons(x7, xs2)) → if2'(ge(x7, n3), n3, x7, xs2)
if2'(false_renamed, n4, x8, xs3) → filterhigh'(n4, xs3)
filterhigh'(n5, nil) → false
ge(x, 0) → true_renamed
ge(s(x'), s(y)) → ge(x', y)
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
filterlow(n', cons(x3, xs')) → if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') → cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) → nil
ge(0, s(x5)) → false_renamed
half(0) → 0
if2(true_renamed, n2, x6, xs1) → filterhigh(n2, xs1)
filterhigh(n3, cons(x7, xs2)) → if2(ge(x7, n3), n3, x7, xs2)
if2(false_renamed, n4, x8, xs3) → cons(x8, filterhigh(n4, xs3))
filterhigh(n5, nil) → nil
half(s(v14)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v23)) → false
equal_sort[a0](s(v24), 0) → false
equal_sort[a0](s(v24), s(v25)) → equal_sort[a0](v24, v25)
equal_sort[a5](cons(v26, v27), cons(v28, v29)) → and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
equal_sort[a5](cons(v26, v27), nil) → false
equal_sort[a5](nil, cons(v30, v31)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a34](true_renamed, true_renamed) → true
equal_sort[a34](true_renamed, false_renamed) → false
equal_sort[a34](false_renamed, true_renamed) → false
equal_sort[a34](false_renamed, false_renamed) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true
Q is empty.
(152) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
if2'(
x1,
x2,
x3,
x4) =
if2'(
x1,
x2,
x3,
x4)
true_renamed =
true_renamed
true =
true
filterhigh'(
x1,
x2) =
filterhigh'(
x1,
x2)
cons(
x1,
x2) =
cons(
x1,
x2)
ge(
x1,
x2) =
ge(
x1,
x2)
false_renamed =
false_renamed
nil =
nil
false =
false
0 =
0
s(
x1) =
x1
if1(
x1,
x2,
x3,
x4) =
if1(
x1,
x2,
x3,
x4)
filterlow(
x1,
x2) =
filterlow(
x1,
x2)
half(
x1) =
half(
x1)
if2(
x1,
x2,
x3,
x4) =
if2(
x1,
x2,
x3,
x4)
filterhigh(
x1,
x2) =
filterhigh(
x1,
x2)
equal_bool(
x1,
x2) =
equal_bool(
x1,
x2)
and(
x1,
x2) =
and(
x1,
x2)
or(
x1,
x2) =
or(
x1,
x2)
not(
x1) =
not(
x1)
isa_true(
x1) =
x1
isa_false(
x1) =
isa_false(
x1)
equal_sort[a0](
x1,
x2) =
equal_sort[a0](
x1,
x2)
equal_sort[a5](
x1,
x2) =
equal_sort[a5](
x1,
x2)
equal_sort[a34](
x1,
x2) =
equal_sort[a34](
x1,
x2)
equal_sort[a64](
x1,
x2) =
equal_sort[a64](
x1,
x2)
witness_sort[a64] =
witness_sort[a64]
Recursive path order with status [RPO].
Quasi-Precedence:
nil > [if2'4, true, filterhigh'2, equalsort[a64]2] > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
[if14, filterlow2] > ge2 > cons2
half1 > 0 > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
equalbool2 > [if2'4, true, filterhigh'2, equalsort[a64]2] > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
or2 > cons2
not1 > [if2'4, true, filterhigh'2, equalsort[a64]2] > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
isafalse1 > [if2'4, true, filterhigh'2, equalsort[a64]2] > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
equalsort[a5]2 > and2 > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
equalsort[a5]2 > equalsort[a0]2 > [if2'4, true, filterhigh'2, equalsort[a64]2] > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
equalsort[a34]2 > [if2'4, true, filterhigh'2, equalsort[a64]2] > [truerenamed, falserenamed, false] > [if24, filterhigh2] > ge2 > cons2
witnesssort[a64] > cons2
Status:
if2'4: [2,4,3,1]
truerenamed: multiset
true: multiset
filterhigh'2: [1,2]
cons2: [1,2]
ge2: [1,2]
falserenamed: multiset
nil: multiset
false: multiset
0: multiset
if14: [4,2,3,1]
filterlow2: [2,1]
half1: multiset
if24: [2,4,3,1]
filterhigh2: [1,2]
equalbool2: multiset
and2: multiset
or2: multiset
not1: multiset
isafalse1: multiset
equalsort[a0]2: [1,2]
equalsort[a5]2: multiset
equalsort[a34]2: multiset
equalsort[a64]2: [1,2]
witnesssort[a64]: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
if2'(true_renamed, n2, x6, xs1) → true
filterhigh'(n3, cons(x7, xs2)) → if2'(ge(x7, n3), n3, x7, xs2)
if2'(false_renamed, n4, x8, xs3) → filterhigh'(n4, xs3)
filterhigh'(n5, nil) → false
ge(x, 0) → true_renamed
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
filterlow(n', cons(x3, xs')) → if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') → cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) → nil
ge(0, s(x5)) → false_renamed
half(0) → 0
if2(true_renamed, n2, x6, xs1) → filterhigh(n2, xs1)
filterhigh(n3, cons(x7, xs2)) → if2(ge(x7, n3), n3, x7, xs2)
if2(false_renamed, n4, x8, xs3) → cons(x8, filterhigh(n4, xs3))
filterhigh(n5, nil) → nil
half(s(v14)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v23)) → false
equal_sort[a0](s(v24), 0) → false
equal_sort[a5](cons(v26, v27), cons(v28, v29)) → and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
equal_sort[a5](cons(v26, v27), nil) → false
equal_sort[a5](nil, cons(v30, v31)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a34](true_renamed, true_renamed) → true
equal_sort[a34](true_renamed, false_renamed) → false
equal_sort[a34](false_renamed, true_renamed) → false
equal_sort[a34](false_renamed, false_renamed) → true
equal_sort[a64](witness_sort[a64], witness_sort[a64]) → true
(153) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
ge(s(x'), s(y)) → ge(x', y)
isa_true(true) → true
isa_true(false) → false
equal_sort[a0](s(v24), s(v25)) → equal_sort[a0](v24, v25)
Q is empty.
(154) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Knuth-Bendix order [KBO] with precedence:
s1 > equalsort[a0]2 > false > true > isatrue1 > ge2
and weight map:
true=1
false=1
s_1=0
isa_true_1=1
ge_2=0
equal_sort[a0]_2=0
The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
ge(s(x'), s(y)) → ge(x', y)
isa_true(true) → true
isa_true(false) → false
equal_sort[a0](s(v24), s(v25)) → equal_sort[a0](v24, v25)
(155) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(156) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(157) YES
(158) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
if2'(true_renamed, n2, x6, xs1) → true
filterhigh'(n3, cons(x7, xs2)) → if2'(ge(x7, n3), n3, x7, xs2)
if2'(false_renamed, n4, x8, xs3) → filterhigh'(n4, xs3)
filterhigh'(n5, nil) → false
ge(x, 0) → true_renamed
ge(s(x'), s(y)) → ge(x', y)
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
filterlow(n', cons(x3, xs')) → if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') → cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) → nil
ge(0, s(x5)) → false_renamed
half(0) → 0
if2(true_renamed, n2, x6, xs1) → filterhigh(n2, xs1)
filterhigh(n3, cons(x7, xs2)) → if2(ge(x7, n3), n3, x7, xs2)
if2(false_renamed, n4, x8, xs3) → cons(x8, filterhigh(n4, xs3))
filterhigh(n5, nil) → nil
half(s(v14)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v23)) → false
equal_sort[a0](s(v24), 0) → false
equal_sort[a0](s(v24), s(v25)) → equal_sort[a0](v24, v25)
equal_sort[a5](cons(v26, v27), cons(v28, v29)) → and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
equal_sort[a5](cons(v26, v27), nil) → false
equal_sort[a5](nil, cons(v30, v31)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a36](true_renamed, true_renamed) → true
equal_sort[a36](true_renamed, false_renamed) → false
equal_sort[a36](false_renamed, true_renamed) → false
equal_sort[a36](false_renamed, false_renamed) → true
equal_sort[a66](witness_sort[a66], witness_sort[a66]) → true
Q is empty.
(159) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Combined order from the following AFS and order.
if2'(
x1,
x2,
x3,
x4) =
if2'(
x1,
x2,
x3,
x4)
true_renamed =
true_renamed
true =
true
filterhigh'(
x1,
x2) =
filterhigh'(
x1,
x2)
cons(
x1,
x2) =
cons(
x1,
x2)
ge(
x1,
x2) =
ge(
x1,
x2)
false_renamed =
false_renamed
nil =
nil
false =
false
0 =
0
s(
x1) =
s(
x1)
if1(
x1,
x2,
x3,
x4) =
if1(
x1,
x2,
x3,
x4)
filterlow(
x1,
x2) =
filterlow(
x1,
x2)
half(
x1) =
x1
if2(
x1,
x2,
x3,
x4) =
if2(
x1,
x2,
x3,
x4)
filterhigh(
x1,
x2) =
filterhigh(
x1,
x2)
equal_bool(
x1,
x2) =
equal_bool(
x1,
x2)
and(
x1,
x2) =
and(
x1,
x2)
or(
x1,
x2) =
or(
x1,
x2)
not(
x1) =
not(
x1)
isa_true(
x1) =
x1
isa_false(
x1) =
isa_false(
x1)
equal_sort[a0](
x1,
x2) =
equal_sort[a0](
x1,
x2)
equal_sort[a5](
x1,
x2) =
equal_sort[a5](
x1,
x2)
equal_sort[a36](
x1,
x2) =
equal_sort[a36](
x1,
x2)
equal_sort[a66](
x1,
x2) =
equal_sort[a66](
x1,
x2)
witness_sort[a66] =
witness_sort[a66]
Recursive path order with status [RPO].
Quasi-Precedence:
[if2'4, filterhigh'2] > [false, not1] > true > [cons2, ge2, equalsort[a0]2]
s1 > [false, not1] > true > [cons2, ge2, equalsort[a0]2]
s1 > 0 > truerenamed > [falserenamed, if14, filterlow2] > [cons2, ge2, equalsort[a0]2]
s1 > 0 > true > [cons2, ge2, equalsort[a0]2]
[if24, filterhigh2] > nil > [cons2, ge2, equalsort[a0]2]
equalbool2 > true > [cons2, ge2, equalsort[a0]2]
or2 > true > [cons2, ge2, equalsort[a0]2]
isafalse1 > [false, not1] > true > [cons2, ge2, equalsort[a0]2]
equalsort[a5]2 > [false, not1] > true > [cons2, ge2, equalsort[a0]2]
equalsort[a5]2 > and2 > [cons2, ge2, equalsort[a0]2]
equalsort[a36]2 > [false, not1] > true > [cons2, ge2, equalsort[a0]2]
equalsort[a66]2 > true > [cons2, ge2, equalsort[a0]2]
witnesssort[a66] > [cons2, ge2, equalsort[a0]2]
Status:
if2'4: [2,4,1,3]
truerenamed: multiset
true: multiset
filterhigh'2: [1,2]
cons2: multiset
ge2: multiset
falserenamed: multiset
nil: multiset
false: multiset
0: multiset
s1: multiset
if14: [2,4,3,1]
filterlow2: [1,2]
if24: [4,2,3,1]
filterhigh2: [2,1]
equalbool2: multiset
and2: multiset
or2: multiset
not1: multiset
isafalse1: multiset
equalsort[a0]2: multiset
equalsort[a5]2: multiset
equalsort[a36]2: [1,2]
equalsort[a66]2: multiset
witnesssort[a66]: multiset
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
if2'(true_renamed, n2, x6, xs1) → true
filterhigh'(n3, cons(x7, xs2)) → if2'(ge(x7, n3), n3, x7, xs2)
if2'(false_renamed, n4, x8, xs3) → filterhigh'(n4, xs3)
filterhigh'(n5, nil) → false
ge(x, 0) → true_renamed
ge(s(x'), s(y)) → ge(x', y)
if1(true_renamed, n, x'', xs) → filterlow(n, xs)
filterlow(n', cons(x3, xs')) → if1(ge(n', x3), n', x3, xs')
if1(false_renamed, n'', x4, xs'') → cons(x4, filterlow(n'', xs''))
filterlow(n1, nil) → nil
ge(0, s(x5)) → false_renamed
if2(true_renamed, n2, x6, xs1) → filterhigh(n2, xs1)
filterhigh(n3, cons(x7, xs2)) → if2(ge(x7, n3), n3, x7, xs2)
if2(false_renamed, n4, x8, xs3) → cons(x8, filterhigh(n4, xs3))
filterhigh(n5, nil) → nil
half(s(v14)) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(v23)) → false
equal_sort[a0](s(v24), 0) → false
equal_sort[a0](s(v24), s(v25)) → equal_sort[a0](v24, v25)
equal_sort[a5](cons(v26, v27), cons(v28, v29)) → and(equal_sort[a0](v26, v28), equal_sort[a5](v27, v29))
equal_sort[a5](cons(v26, v27), nil) → false
equal_sort[a5](nil, cons(v30, v31)) → false
equal_sort[a5](nil, nil) → true
equal_sort[a36](true_renamed, true_renamed) → true
equal_sort[a36](true_renamed, false_renamed) → false
equal_sort[a36](false_renamed, true_renamed) → false
equal_sort[a36](false_renamed, false_renamed) → true
equal_sort[a66](witness_sort[a66], witness_sort[a66]) → true
(160) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
half(0) → 0
isa_true(true) → true
isa_true(false) → false
Q is empty.
(161) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Knuth-Bendix order [KBO] with precedence:
isatrue1 > false > true > 0 > half1
and weight map:
0=1
true=1
false=1
half_1=1
isa_true_1=0
The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
half(0) → 0
isa_true(true) → true
isa_true(false) → false
(162) Obligation:
Q restricted rewrite system:
R is empty.
Q is empty.
(163) RisEmptyProof (EQUIVALENT transformation)
The TRS R is empty. Hence, termination is trivially proven.
(164) YES