0 QTRS
↳1 AAECC Innermost (⇔)
↳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 Instantiation (⇔)
↳20 QDP
↳21 NonInfProof (⇔)
↳22 QDP
↳23 DependencyGraphProof (⇔)
↳24 TRUE
↳25 QDP
↳26 UsableRulesProof (⇔)
↳27 QDP
↳28 QReductionProof (⇔)
↳29 QDP
↳30 QDPOrderProof (⇔)
↳31 QDP
↳32 DependencyGraphProof (⇔)
↳33 TRUE
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
a → b
a → c
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
a → b
a → c
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
a → b
a → c
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
PLUS(x, y) → PLUSITER(x, y, 0)
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
PLUSITER(x, y, z) → LE(x, z)
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
LE(s(x), s(y)) → LE(x, y)
SUM(xs) → SUMITER(xs, 0)
SUMITER(xs, x) → IFSUM(isempty(xs), xs, x, plus(x, head(xs)))
SUMITER(xs, x) → ISEMPTY(xs)
SUMITER(xs, x) → PLUS(x, head(xs))
SUMITER(xs, x) → HEAD(xs)
IFSUM(false, xs, x, y) → SUMITER(tail(xs), y)
IFSUM(false, xs, x, y) → TAIL(xs)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
a → b
a → c
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
LE(s(x), s(y)) → LE(x, y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
a → b
a → c
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
LE(s(x), s(y)) → LE(x, y)
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
a → b
a → c
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
PLUSITER(z0, s(z1), s(z2)) → IFPLUS(le(z0, s(z2)), z0, s(z1), s(z2))
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
PLUSITER(z0, s(z1), s(z2)) → IFPLUS(le(z0, s(z2)), z0, s(z1), s(z2))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
(1) (IFPLUS(le(x3, x5), x3, x4, x5)=IFPLUS(false, x6, x7, x8) ⇒ IFPLUS(false, x6, x7, x8)≥PLUSITER(x6, s(x7), s(x8)))
(2) (le(x3, x5)=false ⇒ IFPLUS(false, x3, x4, x5)≥PLUSITER(x3, s(x4), s(x5)))
(3) (false=false ⇒ IFPLUS(false, s(x18), x4, 0)≥PLUSITER(s(x18), s(x4), s(0)))
(4) (le(x21, x20)=false∧(∀x22:le(x21, x20)=false ⇒ IFPLUS(false, x21, x22, x20)≥PLUSITER(x21, s(x22), s(x20))) ⇒ IFPLUS(false, s(x21), x4, s(x20))≥PLUSITER(s(x21), s(x4), s(s(x20))))
(5) (IFPLUS(false, s(x18), x4, 0)≥PLUSITER(s(x18), s(x4), s(0)))
(6) (IFPLUS(false, x21, x4, x20)≥PLUSITER(x21, s(x4), s(x20)) ⇒ IFPLUS(false, s(x21), x4, s(x20))≥PLUSITER(s(x21), s(x4), s(s(x20))))
(7) (PLUSITER(x9, s(x10), s(x11))=PLUSITER(x12, x13, x14) ⇒ PLUSITER(x12, x13, x14)≥IFPLUS(le(x12, x14), x12, x13, x14))
(8) (PLUSITER(x9, s(x10), s(x11))≥IFPLUS(le(x9, s(x11)), x9, s(x10), s(x11)))
POL(0) = 0
POL(IFPLUS(x1, x2, x3, x4)) = -1 - x1 + x2 - x4
POL(PLUSITER(x1, x2, x3)) = -1 + x1 - x3
POL(c) = -2
POL(false) = 0
POL(le(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
The following rules are usable:
IFPLUS(false, x, y, z) → PLUSITER(x, s(y), s(z))
true → le(0, y)
false → le(s(x), 0)
le(x, y) → le(s(x), s(y))
PLUSITER(x, y, z) → IFPLUS(le(x, z), x, y, z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
SUMITER(xs, x) → IFSUM(isempty(xs), xs, x, plus(x, head(xs)))
IFSUM(false, xs, x, y) → SUMITER(tail(xs), y)
plus(x, y) → plusIter(x, y, 0)
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
ifPlus(true, x, y, z) → y
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
sum(xs) → sumIter(xs, 0)
sumIter(xs, x) → ifSum(isempty(xs), xs, x, plus(x, head(xs)))
ifSum(true, xs, x, y) → x
ifSum(false, xs, x, y) → sumIter(tail(xs), y)
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
a → b
a → c
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
SUMITER(xs, x) → IFSUM(isempty(xs), xs, x, plus(x, head(xs)))
IFSUM(false, xs, x, y) → SUMITER(tail(xs), y)
tail(nil) → nil
tail(cons(x, xs)) → xs
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
plus(x, y) → plusIter(x, y, 0)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(true, x, y, z) → y
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
sum(x0)
sumIter(x0, x1)
ifSum(true, x0, x1, x2)
ifSum(false, x0, x1, x2)
a
SUMITER(xs, x) → IFSUM(isempty(xs), xs, x, plus(x, head(xs)))
IFSUM(false, xs, x, y) → SUMITER(tail(xs), y)
tail(nil) → nil
tail(cons(x, xs)) → xs
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
plus(x, y) → plusIter(x, y, 0)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(true, x, y, z) → y
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SUMITER(xs, x) → IFSUM(isempty(xs), xs, x, plus(x, head(xs)))
The value of delta used in the strict ordering is 3/16.
POL(SUMITER(x1, x2)) = 1/2 + (3/4)x1
POL(IFSUM(x1, x2, x3, x4)) = 1/4 + (1/4)x1 + (1/2)x2
POL(isempty(x1)) = 1/4 + x1
POL(plus(x1, x2)) = 1/4 + (3/4)x1 + (1/2)x2
POL(head(x1)) = 2 + (1/4)x1
POL(false) = 7/4
POL(tail(x1)) = 1/4 + (1/4)x1
POL(nil) = 1/4
POL(true) = 1/2
POL(cons(x1, x2)) = 3/2 + (4)x1 + (4)x2
POL(error) = 7/4
POL(plusIter(x1, x2, x3)) = 13/4 + (1/2)x1 + (3)x2 + (7/4)x3
POL(0) = 0
POL(le(x1, x2)) = 2 + (1/4)x1 + (7/4)x2
POL(s(x1)) = (7/2)x1
POL(ifPlus(x1, x2, x3, x4)) = 3/2 + (4)x1 + (7/4)x2 + (3)x3 + (1/2)x4
tail(nil) → nil
isempty(nil) → true
tail(cons(x, xs)) → xs
isempty(cons(x, xs)) → false
IFSUM(false, xs, x, y) → SUMITER(tail(xs), y)
tail(nil) → nil
tail(cons(x, xs)) → xs
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
plus(x, y) → plusIter(x, y, 0)
ifPlus(false, x, y, z) → plusIter(x, s(y), s(z))
plusIter(x, y, z) → ifPlus(le(x, z), x, y, z)
le(s(x), 0) → false
le(0, y) → true
le(s(x), s(y)) → le(x, y)
ifPlus(true, x, y, z) → y
plus(x0, x1)
plusIter(x0, x1, x2)
ifPlus(true, x0, x1, x2)
ifPlus(false, x0, x1, x2)
le(s(x0), 0)
le(0, x0)
le(s(x0), s(x1))
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))