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 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
↳36 QDP
↳37 UsableRulesProof (⇔)
↳38 QDP
↳39 QReductionProof (⇔)
↳40 QDP
↳41 QDPOrderProof (⇔)
↳42 QDP
↳43 DependencyGraphProof (⇔)
↳44 TRUE
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
a → b
a → c
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
PROD(xs) → PRODITER(xs, s(0))
PRODITER(xs, x) → IFPROD(isempty(xs), xs, x)
PRODITER(xs, x) → ISEMPTY(xs)
IFPROD(false, xs, x) → PRODITER(tail(xs), times(x, head(xs)))
IFPROD(false, xs, x) → TAIL(xs)
IFPROD(false, xs, x) → TIMES(x, head(xs))
IFPROD(false, xs, x) → HEAD(xs)
PLUS(s(x), y) → PLUS(x, y)
TIMES(x, y) → TIMESITER(x, y, 0, 0)
TIMESITER(x, y, z, u) → IFTIMES(ge(u, x), x, y, z, u)
TIMESITER(x, y, z, u) → GE(u, x)
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, plus(y, z), s(u))
IFTIMES(false, x, y, z, u) → PLUS(y, z)
GE(s(x), s(y)) → GE(x, y)
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
GE(s(x), s(y)) → GE(x, y)
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
GE(s(x), s(y)) → GE(x, y)
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
PLUS(s(x), y) → PLUS(x, y)
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
PLUS(s(x), y) → PLUS(x, y)
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
PLUS(s(x), y) → PLUS(x, y)
From the DPs we obtained the following set of size-change graphs:
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, plus(y, z), s(u))
TIMESITER(x, y, z, u) → IFTIMES(ge(u, x), x, y, z, u)
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, plus(y, z), s(u))
TIMESITER(x, y, z, u) → IFTIMES(ge(u, x), x, y, z, u)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
a
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, plus(y, z), s(u))
TIMESITER(x, y, z, u) → IFTIMES(ge(u, x), x, y, z, u)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
TIMESITER(z0, z1, y_0, s(z3)) → IFTIMES(ge(s(z3), z0), z0, z1, y_0, s(z3))
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, plus(y, z), s(u))
TIMESITER(z0, z1, y_0, s(z3)) → IFTIMES(ge(s(z3), z0), z0, z1, y_0, s(z3))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
(1) (IFTIMES(ge(x7, x4), x4, x5, x6, x7)=IFTIMES(false, x8, x9, x10, x11) ⇒ IFTIMES(false, x8, x9, x10, x11)≥TIMESITER(x8, x9, plus(x9, x10), s(x11)))
(2) (ge(x7, x4)=false ⇒ IFTIMES(false, x4, x5, x6, x7)≥TIMESITER(x4, x5, plus(x5, x6), s(x7)))
(3) (false=false ⇒ IFTIMES(false, s(x25), x5, x6, 0)≥TIMESITER(s(x25), x5, plus(x5, x6), s(0)))
(4) (ge(x27, x26)=false∧(∀x28,x29:ge(x27, x26)=false ⇒ IFTIMES(false, x26, x28, x29, x27)≥TIMESITER(x26, x28, plus(x28, x29), s(x27))) ⇒ IFTIMES(false, s(x26), x5, x6, s(x27))≥TIMESITER(s(x26), x5, plus(x5, x6), s(s(x27))))
(5) (IFTIMES(false, s(x25), x5, x6, 0)≥TIMESITER(s(x25), x5, plus(x5, x6), s(0)))
(6) (IFTIMES(false, x26, x5, x6, x27)≥TIMESITER(x26, x5, plus(x5, x6), s(x27)) ⇒ IFTIMES(false, s(x26), x5, x6, s(x27))≥TIMESITER(s(x26), x5, plus(x5, x6), s(s(x27))))
(7) (TIMESITER(x12, x13, plus(x13, x14), s(x15))=TIMESITER(x16, x17, x18, x19) ⇒ TIMESITER(x16, x17, x18, x19)≥IFTIMES(ge(x19, x16), x16, x17, x18, x19))
(8) (TIMESITER(x12, x13, x18, s(x15))≥IFTIMES(ge(s(x15), x12), x12, x13, x18, s(x15)))
POL(0) = 1
POL(IFTIMES(x1, x2, x3, x4, x5)) = -1 - x1 + x2 + x3 - x5
POL(TIMESITER(x1, x2, x3, x4)) = -1 + x1 + x2 - x4
POL(c) = -2
POL(false) = 1
POL(ge(x1, x2)) = 1
POL(plus(x1, x2)) = 1
POL(s(x1)) = 1 + x1
POL(true) = 1
The following pairs are in Pbound:
TIMESITER(x, y, z, u) → IFTIMES(ge(u, x), x, y, z, u)
The following rules are usable:
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, plus(y, z), s(u))
false → ge(0, s(y))
ge(x, y) → ge(s(x), s(y))
true → ge(x, 0)
IFTIMES(false, x, y, z, u) → TIMESITER(x, y, plus(y, z), s(u))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
TIMESITER(x, y, z, u) → IFTIMES(ge(u, x), x, y, z, u)
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(0, x0)
plus(s(x0), x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IFPROD(false, xs, x) → PRODITER(tail(xs), times(x, head(xs)))
PRODITER(xs, x) → IFPROD(isempty(xs), xs, x)
prod(xs) → prodIter(xs, s(0))
prodIter(xs, x) → ifProd(isempty(xs), xs, x)
ifProd(true, xs, x) → x
ifProd(false, xs, x) → prodIter(tail(xs), times(x, head(xs)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(x, y) → timesIter(x, y, 0, 0)
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
ifTimes(true, x, y, z, u) → z
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
isempty(nil) → true
isempty(cons(x, xs)) → false
head(nil) → error
head(cons(x, xs)) → x
tail(nil) → nil
tail(cons(x, xs)) → xs
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
a → b
a → c
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
IFPROD(false, xs, x) → PRODITER(tail(xs), times(x, head(xs)))
PRODITER(xs, x) → IFPROD(isempty(xs), xs, x)
isempty(nil) → true
isempty(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(nil) → error
head(cons(x, xs)) → x
times(x, y) → timesIter(x, y, 0, 0)
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ifTimes(true, x, y, z, u) → z
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
a
prod(x0)
prodIter(x0, x1)
ifProd(true, x0, x1)
ifProd(false, x0, x1)
a
IFPROD(false, xs, x) → PRODITER(tail(xs), times(x, head(xs)))
PRODITER(xs, x) → IFPROD(isempty(xs), xs, x)
isempty(nil) → true
isempty(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(nil) → error
head(cons(x, xs)) → x
times(x, y) → timesIter(x, y, 0, 0)
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ifTimes(true, x, y, z, u) → z
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PRODITER(xs, x) → IFPROD(isempty(xs), xs, x)
The value of delta used in the strict ordering is 1/16.
POL(IFPROD(x1, x2, x3)) = (1/4)x1 + x2
POL(false) = 1
POL(PRODITER(x1, x2)) = 1/4 + (4)x1
POL(tail(x1)) = (1/4)x1
POL(times(x1, x2)) = 7/4 + (4)x1
POL(head(x1)) = 5/4 + (5/4)x1
POL(isempty(x1)) = 3/4 + (1/4)x1
POL(nil) = 0
POL(true) = 3/4
POL(cons(x1, x2)) = 1 + (5/4)x1 + (4)x2
POL(error) = 3/4
POL(ge(x1, x2)) = 5/4 + (7/4)x1 + (1/4)x2
POL(s(x1)) = 1
POL(ifTimes(x1, x2, x3, x4, x5)) = 9/4 + (1/4)x1 + (4)x2 + (5/4)x3 + (7/4)x4 + (11/4)x5
POL(timesIter(x1, x2, x3, x4)) = 1/4 + (4)x1 + (15/4)x2 + (5/2)x4
POL(0) = 15/4
POL(plus(x1, x2)) = 4 + x1 + (1/4)x2
isempty(nil) → true
tail(nil) → nil
isempty(cons(x, xs)) → false
tail(cons(x, xs)) → xs
IFPROD(false, xs, x) → PRODITER(tail(xs), times(x, head(xs)))
isempty(nil) → true
isempty(cons(x, xs)) → false
tail(nil) → nil
tail(cons(x, xs)) → xs
head(nil) → error
head(cons(x, xs)) → x
times(x, y) → timesIter(x, y, 0, 0)
ifTimes(false, x, y, z, u) → timesIter(x, y, plus(y, z), s(u))
timesIter(x, y, z, u) → ifTimes(ge(u, x), x, y, z, u)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
ge(x, 0) → true
ge(0, s(y)) → false
ge(s(x), s(y)) → ge(x, y)
ifTimes(true, x, y, z, u) → z
plus(0, x0)
plus(s(x0), x1)
times(x0, x1)
timesIter(x0, x1, x2, x3)
ifTimes(true, x0, x1, x2, x3)
ifTimes(false, x0, x1, x2, x3)
isempty(nil)
isempty(cons(x0, x1))
head(nil)
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))