0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
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
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
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)
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)
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
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)
LT(s(x), s(y)) → LT(x, y)
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
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LT(s(x), s(y)) → LT(x, y)
s1 > LT1
LT1: multiset
s1: multiset
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
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)
LENGTH(cons(x, l)) → LENGTH(l)
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
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LENGTH(cons(x, l)) → LENGTH(l)
cons2 > LENGTH1
LENGTH1: multiset
cons2: multiset
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
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)
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)
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
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)