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 QDPOrderProof (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 TRUE
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
zero(0) → true
zero(s(x)) → false
conv(x) → conviter(x, cons(0, nil))
conviter(x, l) → if(zero(x), x, l)
if(true, x, l) → l
if(false, x, l) → conviter(half(x), cons(lastbit(x), l))
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
zero(0) → true
zero(s(x)) → false
conv(x) → conviter(x, cons(0, nil))
conviter(x, l) → if(zero(x), x, l)
if(true, x, l) → l
if(false, x, l) → conviter(half(x), cons(lastbit(x), l))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
HALF(s(s(x))) → HALF(x)
LASTBIT(s(s(x))) → LASTBIT(x)
CONV(x) → CONVITER(x, cons(0, nil))
CONVITER(x, l) → IF(zero(x), x, l)
CONVITER(x, l) → ZERO(x)
IF(false, x, l) → CONVITER(half(x), cons(lastbit(x), l))
IF(false, x, l) → HALF(x)
IF(false, x, l) → LASTBIT(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
zero(0) → true
zero(s(x)) → false
conv(x) → conviter(x, cons(0, nil))
conviter(x, l) → if(zero(x), x, l)
if(true, x, l) → l
if(false, x, l) → conviter(half(x), cons(lastbit(x), l))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
LASTBIT(s(s(x))) → LASTBIT(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
zero(0) → true
zero(s(x)) → false
conv(x) → conviter(x, cons(0, nil))
conviter(x, l) → if(zero(x), x, l)
if(true, x, l) → l
if(false, x, l) → conviter(half(x), cons(lastbit(x), l))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
LASTBIT(s(s(x))) → LASTBIT(x)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
LASTBIT(s(s(x))) → LASTBIT(x)
From the DPs we obtained the following set of size-change graphs:
HALF(s(s(x))) → HALF(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
zero(0) → true
zero(s(x)) → false
conv(x) → conviter(x, cons(0, nil))
conviter(x, l) → if(zero(x), x, l)
if(true, x, l) → l
if(false, x, l) → conviter(half(x), cons(lastbit(x), l))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
HALF(s(s(x))) → HALF(x)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
HALF(s(s(x))) → HALF(x)
From the DPs we obtained the following set of size-change graphs:
IF(false, x, l) → CONVITER(half(x), cons(lastbit(x), l))
CONVITER(x, l) → IF(zero(x), x, l)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
zero(0) → true
zero(s(x)) → false
conv(x) → conviter(x, cons(0, nil))
conviter(x, l) → if(zero(x), x, l)
if(true, x, l) → l
if(false, x, l) → conviter(half(x), cons(lastbit(x), l))
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
IF(false, x, l) → CONVITER(half(x), cons(lastbit(x), l))
CONVITER(x, l) → IF(zero(x), x, l)
zero(0) → true
zero(s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
conv(x0)
conviter(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
IF(false, x, l) → CONVITER(half(x), cons(lastbit(x), l))
CONVITER(x, l) → IF(zero(x), x, l)
zero(0) → true
zero(s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONVITER(x, l) → IF(zero(x), x, l)
The value of delta used in the strict ordering is 1/8.
POL(IF(x1, x2, x3)) = (1/2)x1 + (7/4)x2 + (1/2)x3
POL(false) = 1/2
POL(CONVITER(x1, x2)) = 1/4 + (2)x1 + (1/2)x2
POL(half(x1)) = (1/2)x1
POL(cons(x1, x2)) = (1/2)x2
POL(lastbit(x1)) = 1/2
POL(zero(x1)) = 1/4 + (1/2)x1
POL(0) = 0
POL(true) = 1/4
POL(s(x1)) = 1/2 + (9/4)x1
zero(0) → true
zero(s(x)) → false
half(s(s(x))) → s(half(x))
half(0) → 0
half(s(0)) → 0
IF(false, x, l) → CONVITER(half(x), cons(lastbit(x), l))
zero(0) → true
zero(s(x)) → false
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
lastbit(0) → 0
lastbit(s(0)) → s(0)
lastbit(s(s(x))) → lastbit(x)
half(0)
half(s(0))
half(s(s(x0)))
lastbit(0)
lastbit(s(0))
lastbit(s(s(x0)))
zero(0)
zero(s(x0))