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 AND
↳30 QDP
↳31 DependencyGraphProof (⇔)
↳32 TRUE
↳33 QDP
↳34 DependencyGraphProof (⇔)
↳35 TRUE
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
NTHTAIL(n, l) → GE(n, length(l))
NTHTAIL(n, l) → LENGTH(l)
COND(false, n, l) → TAIL(nthtail(s(n), l))
COND(false, n, l) → NTHTAIL(s(n), l)
LENGTH(cons(x, l)) → LENGTH(l)
GE(s(u), s(v)) → GE(u, v)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
GE(s(u), s(v)) → GE(u, v)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
GE(s(u), s(v)) → GE(u, v)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
GE(s(u), s(v)) → GE(u, v)
From the DPs we obtained the following set of size-change graphs:
LENGTH(cons(x, l)) → LENGTH(l)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
LENGTH(cons(x, l)) → LENGTH(l)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
LENGTH(cons(x, l)) → LENGTH(l)
From the DPs we obtained the following set of size-change graphs:
COND(false, n, l) → NTHTAIL(s(n), l)
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
nthtail(n, l) → cond(ge(n, length(l)), n, l)
cond(true, n, l) → l
cond(false, n, l) → tail(nthtail(s(n), l))
tail(nil) → nil
tail(cons(x, l)) → l
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
COND(false, n, l) → NTHTAIL(s(n), l)
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
nthtail(x0, x1)
cond(true, x0, x1)
cond(false, x0, x1)
tail(nil)
tail(cons(x0, x1))
COND(false, n, l) → NTHTAIL(s(n), l)
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
NTHTAIL(s(z0), z1) → COND(ge(s(z0), length(z1)), s(z0), z1)
COND(false, n, l) → NTHTAIL(s(n), l)
NTHTAIL(s(z0), z1) → COND(ge(s(z0), length(z1)), s(z0), z1)
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
(1) (COND(ge(x2, length(x3)), x2, x3)=COND(false, x4, x5) ⇒ COND(false, x4, x5)≥NTHTAIL(s(x4), x5))
(2) (length(x3)=x12∧ge(x2, x12)=false ⇒ COND(false, x2, x3)≥NTHTAIL(s(x2), x3))
(3) (false=false∧length(x3)=s(x14) ⇒ COND(false, 0, x3)≥NTHTAIL(s(0), x3))
(4) (ge(x16, x15)=false∧length(x3)=s(x15)∧(∀x17:ge(x16, x15)=false∧length(x17)=x15 ⇒ COND(false, x16, x17)≥NTHTAIL(s(x16), x17)) ⇒ COND(false, s(x16), x3)≥NTHTAIL(s(s(x16)), x3))
(5) (length(x3)=s(x14) ⇒ COND(false, 0, x3)≥NTHTAIL(s(0), x3))
(6) (s(length(x21))=s(x15)∧ge(x16, x15)=false∧(∀x17:ge(x16, x15)=false∧length(x17)=x15 ⇒ COND(false, x16, x17)≥NTHTAIL(s(x16), x17))∧(∀x23,x24,x25:length(x21)=s(x23)∧ge(x24, x23)=false∧(∀x25:ge(x24, x23)=false∧length(x25)=x23 ⇒ COND(false, x24, x25)≥NTHTAIL(s(x24), x25)) ⇒ COND(false, s(x24), x21)≥NTHTAIL(s(s(x24)), x21)) ⇒ COND(false, s(x16), cons(x22, x21))≥NTHTAIL(s(s(x16)), cons(x22, x21)))
(7) (s(length(x18))=s(x14)∧(∀x20:length(x18)=s(x20) ⇒ COND(false, 0, x18)≥NTHTAIL(s(0), x18)) ⇒ COND(false, 0, cons(x19, x18))≥NTHTAIL(s(0), cons(x19, x18)))
(8) (COND(false, 0, cons(x19, x18))≥NTHTAIL(s(0), cons(x19, x18)))
(9) (length(x21)=x15∧ge(x16, x15)=false∧(∀x17:ge(x16, x15)=false∧length(x17)=x15 ⇒ COND(false, x16, x17)≥NTHTAIL(s(x16), x17))∧(∀x23,x24,x25:length(x21)=s(x23)∧ge(x24, x23)=false∧(∀x25:ge(x24, x23)=false∧length(x25)=x23 ⇒ COND(false, x24, x25)≥NTHTAIL(s(x24), x25)) ⇒ COND(false, s(x24), x21)≥NTHTAIL(s(s(x24)), x21)) ⇒ COND(false, s(x16), cons(x22, x21))≥NTHTAIL(s(s(x16)), cons(x22, x21)))
(10) (COND(false, x16, x21)≥NTHTAIL(s(x16), x21)∧(∀x23,x24,x25:length(x21)=s(x23)∧ge(x24, x23)=false∧(∀x25:ge(x24, x23)=false∧length(x25)=x23 ⇒ COND(false, x24, x25)≥NTHTAIL(s(x24), x25)) ⇒ COND(false, s(x24), x21)≥NTHTAIL(s(s(x24)), x21)) ⇒ COND(false, s(x16), cons(x22, x21))≥NTHTAIL(s(s(x16)), cons(x22, x21)))
(11) (COND(false, x16, x21)≥NTHTAIL(s(x16), x21) ⇒ COND(false, s(x16), cons(x22, x21))≥NTHTAIL(s(s(x16)), cons(x22, x21)))
(12) (NTHTAIL(s(x6), x7)=NTHTAIL(x8, x9) ⇒ NTHTAIL(x8, x9)≥COND(ge(x8, length(x9)), x8, x9))
(13) (NTHTAIL(s(x6), x7)≥COND(ge(s(x6), length(x7)), s(x6), x7))
POL(0) = 0
POL(COND(x1, x2, x3)) = -1 - x1 - x2 + x3
POL(NTHTAIL(x1, x2)) = -x1 + x2
POL(c) = -1
POL(cons(x1, x2)) = 1 + x2
POL(false) = 0
POL(ge(x1, x2)) = 0
POL(length(x1)) = 0
POL(nil) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
The following rules are usable:
COND(false, n, l) → NTHTAIL(s(n), l)
false → ge(0, s(v))
true → ge(u, 0)
ge(u, v) → ge(s(u), s(v))
COND(false, n, l) → NTHTAIL(s(n), l)
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
NTHTAIL(n, l) → COND(ge(n, length(l)), n, l)
length(nil) → 0
length(cons(x, l)) → s(length(l))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
length(nil)
length(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))