(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) 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:
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
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.
(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].
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))
(11) 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
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(12) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
IF(false, x, l) → LAST(head(l), tail(l))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
POL(IF(x1, x2, x3)) = (4)x1 + (3/4)x3
POL(false) = 2
POL(LAST(x1, x2)) = (11/4)x2
POL(head(x1)) = 5/2
POL(tail(x1)) = (1/4)x1
POL(empty(x1)) = (1/2)x1
POL(cons(x1, x2)) = 4 + (1/2)x1 + (4)x2
POL(nil) = 0
POL(true) = 0
The value of delta used in the strict ordering is 8.
The following usable rules [FROCOS05] were oriented:
empty(cons(x, l)) → false
empty(nil) → true
tail(nil) → nil
tail(cons(x, l)) → l
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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
The set Q consists of the following terms:
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(14) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(15) TRUE
(16) 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.
(17) 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.
(18) 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:
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, 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.
(19) 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].
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
(20) 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:
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
The set Q consists of the following terms:
rev(nil)
rev(cons(x0, x1))
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(21) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV2(x, cons(y, l)) → REV2(y, l)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(REV2(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(rev2(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(rev1(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
rev2(x, nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
REV(cons(x, l)) → REV2(x, l)
The TRS R consists of the following rules:
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
The set Q consists of the following terms:
rev(nil)
rev(cons(x0, x1))
rev2(x0, nil)
rev2(x0, cons(x1, x2))
We have to consider all minimal (P,Q,R)-chains.
(23) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(24) TRUE