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