(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
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:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REV(cons(x, l)) → REV2(x, l)
LAST(x, l) → IF(empty(l), x, l)
LAST(x, l) → EMPTY(l)
IF(false, x, l) → LAST(head(l), tail(l))
IF(false, x, l) → HEAD(l)
IF(false, x, l) → TAIL(l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV2(x, cons(y, l)) → REV2(y, l)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 3 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
The TRS R consists of the following rules:
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.