0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 Instantiation (⇔)
↳27 QDP
↳28 NonInfProof (⇔)
↳29 QDP
↳30 DependencyGraphProof (⇔)
↳31 TRUE
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)
LT(s(x), s(y)) → LT(x, y)
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(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)
From the DPs we obtained the following set of size-change graphs:
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)
LENGTH(cons(x, l)) → LENGTH(l)
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(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)
From the DPs we obtained the following set of size-change graphs:
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)
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)
tail(nil) → nil
tail(cons(x, l)) → l
head(cons(x, l)) → x
head(nil) → undefined
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)
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)
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)
tail(nil) → nil
tail(cons(x, l)) → l
head(cons(x, l)) → x
head(nil) → undefined
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)
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))
REV(s(z0), y_0, cons(y_1, z2), z3) → IF(lt(s(z0), length(z3)), s(z0), y_0, cons(y_1, z2), z3)
IF(true, x, l, accu, orig) → REV(s(x), tail(l), cons(head(l), accu), orig)
REV(s(z0), y_0, cons(y_1, z2), z3) → IF(lt(s(z0), length(z3)), s(z0), y_0, cons(y_1, z2), z3)
tail(nil) → nil
tail(cons(x, l)) → l
head(cons(x, l)) → x
head(nil) → undefined
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)
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))
(1) (REV(s(x4), tail(x5), cons(head(x5), x6), x7)=REV(x8, x9, x10, x11) ⇒ REV(x8, x9, x10, x11)≥IF(lt(x8, length(x11)), x8, x9, x10, x11))
(2) (REV(s(x4), x9, x10, x7)≥IF(lt(s(x4), length(x7)), s(x4), x9, x10, x7))
(3) (IF(lt(x12, length(x15)), x12, x13, x14, x15)=IF(true, x16, x17, x18, x19) ⇒ IF(true, x16, x17, x18, x19)≥REV(s(x16), tail(x17), cons(head(x17), x18), x19))
(4) (length(x15)=x24∧lt(x12, x24)=true ⇒ IF(true, x12, x13, x14, x15)≥REV(s(x12), tail(x13), cons(head(x13), x14), x15))
(5) (true=true∧length(x15)=s(x26) ⇒ IF(true, 0, x13, x14, x15)≥REV(s(0), tail(x13), cons(head(x13), x14), x15))
(6) (lt(x28, x27)=true∧length(x15)=s(x27)∧(∀x29,x30,x31:lt(x28, x27)=true∧length(x29)=x27 ⇒ IF(true, x28, x30, x31, x29)≥REV(s(x28), tail(x30), cons(head(x30), x31), x29)) ⇒ IF(true, s(x28), x13, x14, x15)≥REV(s(s(x28)), tail(x13), cons(head(x13), x14), x15))
(7) (length(x15)=s(x26) ⇒ IF(true, 0, x13, x14, x15)≥REV(s(0), tail(x13), cons(head(x13), x14), x15))
(8) (s(length(x37))=s(x27)∧lt(x28, x27)=true∧(∀x29,x30,x31:lt(x28, x27)=true∧length(x29)=x27 ⇒ IF(true, x28, x30, x31, x29)≥REV(s(x28), tail(x30), cons(head(x30), x31), x29))∧(∀x39,x40,x41,x42,x43,x44,x45:length(x37)=s(x39)∧lt(x40, x39)=true∧(∀x41,x42,x43:lt(x40, x39)=true∧length(x41)=x39 ⇒ IF(true, x40, x42, x43, x41)≥REV(s(x40), tail(x42), cons(head(x42), x43), x41)) ⇒ IF(true, s(x40), x44, x45, x37)≥REV(s(s(x40)), tail(x44), cons(head(x44), x45), x37)) ⇒ IF(true, s(x28), x13, x14, cons(x38, x37))≥REV(s(s(x28)), tail(x13), cons(head(x13), x14), cons(x38, x37)))
(9) (s(length(x32))=s(x26)∧(∀x34,x35,x36:length(x32)=s(x34) ⇒ IF(true, 0, x35, x36, x32)≥REV(s(0), tail(x35), cons(head(x35), x36), x32)) ⇒ IF(true, 0, x13, x14, cons(x33, x32))≥REV(s(0), tail(x13), cons(head(x13), x14), cons(x33, x32)))
(10) (IF(true, 0, x13, x14, cons(x33, x32))≥REV(s(0), tail(x13), cons(head(x13), x14), cons(x33, x32)))
(11) (length(x37)=x27∧lt(x28, x27)=true∧(∀x29,x30,x31:lt(x28, x27)=true∧length(x29)=x27 ⇒ IF(true, x28, x30, x31, x29)≥REV(s(x28), tail(x30), cons(head(x30), x31), x29))∧(∀x39,x40,x41,x42,x43,x44,x45:length(x37)=s(x39)∧lt(x40, x39)=true∧(∀x41,x42,x43:lt(x40, x39)=true∧length(x41)=x39 ⇒ IF(true, x40, x42, x43, x41)≥REV(s(x40), tail(x42), cons(head(x42), x43), x41)) ⇒ IF(true, s(x40), x44, x45, x37)≥REV(s(s(x40)), tail(x44), cons(head(x44), x45), x37)) ⇒ IF(true, s(x28), x13, x14, cons(x38, x37))≥REV(s(s(x28)), tail(x13), cons(head(x13), x14), cons(x38, x37)))
(12) (IF(true, x28, x13, x14, x37)≥REV(s(x28), tail(x13), cons(head(x13), x14), x37)∧(∀x39,x40,x41,x42,x43,x44,x45:length(x37)=s(x39)∧lt(x40, x39)=true∧(∀x41,x42,x43:lt(x40, x39)=true∧length(x41)=x39 ⇒ IF(true, x40, x42, x43, x41)≥REV(s(x40), tail(x42), cons(head(x42), x43), x41)) ⇒ IF(true, s(x40), x44, x45, x37)≥REV(s(s(x40)), tail(x44), cons(head(x44), x45), x37)) ⇒ IF(true, s(x28), x13, x14, cons(x38, x37))≥REV(s(s(x28)), tail(x13), cons(head(x13), x14), cons(x38, x37)))
(13) (IF(true, x28, x13, x14, x37)≥REV(s(x28), tail(x13), cons(head(x13), x14), x37) ⇒ IF(true, s(x28), x13, x14, cons(x38, x37))≥REV(s(s(x28)), tail(x13), cons(head(x13), x14), cons(x38, x37)))
POL(0) = 1
POL(IF(x1, x2, x3, x4, x5)) = -x1 - x2 + x5
POL(REV(x1, x2, x3, x4)) = -x1 + x4
POL(c) = -1
POL(cons(x1, x2)) = 1 + x2
POL(false) = 0
POL(head(x1)) = x1
POL(length(x1)) = 0
POL(lt(x1, x2)) = 0
POL(nil) = 1
POL(s(x1)) = 1 + x1
POL(tail(x1)) = 0
POL(true) = 0
POL(undefined) = 1
The following pairs are in Pbound:
IF(true, x, l, accu, orig) → REV(s(x), tail(l), cons(head(l), accu), orig)
The following rules are usable:
IF(true, x, l, accu, orig) → REV(s(x), tail(l), cons(head(l), accu), orig)
true → lt(0, s(y))
lt(x, y) → lt(s(x), s(y))
false → lt(x, 0)
REV(x, l, accu, orig) → IF(lt(x, length(orig)), x, l, accu, orig)
tail(nil) → nil
tail(cons(x, l)) → l
head(cons(x, l)) → x
head(nil) → undefined
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)
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))