MAYBE
Time: 0.062237
TRS:
{ prodIter(xs, x) -> ifProd(isempty xs, xs, x),
prod xs -> prodIter(xs, s 0()),
ifProd(true(), xs, x) -> x,
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,
times(x, y) -> timesIter(x, y, 0(), 0()),
head nil() -> error(),
head cons(x, xs) -> x,
plus(s x, y) -> s plus(x, y),
plus(0(), y) -> y,
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),
ge(x, 0()) -> true(),
ge(s x, s y) -> ge(x, y),
ge(0(), s y) -> false(),
a() -> b(),
a() -> c()}
DP:
DP:
{ prodIter#(xs, x) -> ifProd#(isempty xs, xs, x),
prodIter#(xs, x) -> isempty# xs,
prod# xs -> prodIter#(xs, s 0()),
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,
times#(x, y) -> timesIter#(x, y, 0(), 0()),
plus#(s x, y) -> plus#(x, y),
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) -> plus#(y, z),
ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u),
ge#(s x, s y) -> ge#(x, y)}
TRS:
{ prodIter(xs, x) -> ifProd(isempty xs, xs, x),
prod xs -> prodIter(xs, s 0()),
ifProd(true(), xs, x) -> x,
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,
times(x, y) -> timesIter(x, y, 0(), 0()),
head nil() -> error(),
head cons(x, xs) -> x,
plus(s x, y) -> s plus(x, y),
plus(0(), y) -> y,
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),
ge(x, 0()) -> true(),
ge(s x, s y) -> ge(x, y),
ge(0(), s y) -> false(),
a() -> b(),
a() -> c()}
UR:
{ isempty nil() -> true(),
isempty cons(x, xs) -> false(),
tail nil() -> nil(),
tail cons(x, xs) -> xs,
times(x, y) -> timesIter(x, y, 0(), 0()),
head nil() -> error(),
head cons(x, xs) -> x,
plus(s x, y) -> s plus(x, y),
plus(0(), y) -> y,
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),
ge(x, 0()) -> true(),
ge(s x, s y) -> ge(x, y),
ge(0(), s y) -> false(),
d(w, v) -> w,
d(w, v) -> v}
EDG:
{(timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u), 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), ifTimes#(false(), x, y, z, u) -> plus#(y, z))
(plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
(ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)), prodIter#(xs, x) -> isempty# xs)
(ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)), prodIter#(xs, x) -> ifProd#(isempty xs, xs, x))
(ifProd#(false(), xs, x) -> times#(x, head xs), 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) -> ge#(u, x))
(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))
(prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs)))
(prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> tail# xs)
(prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> times#(x, head xs))
(prodIter#(xs, x) -> ifProd#(isempty xs, xs, x), ifProd#(false(), xs, x) -> head# xs)
(times#(x, y) -> timesIter#(x, y, 0(), 0()), timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u))
(times#(x, y) -> timesIter#(x, y, 0(), 0()), timesIter#(x, y, z, u) -> ge#(u, x))
(ifTimes#(false(), x, y, z, u) -> plus#(y, z), plus#(s x, y) -> plus#(x, y))
(ge#(s x, s y) -> ge#(x, y), ge#(s x, s y) -> ge#(x, y))
(timesIter#(x, y, z, u) -> ge#(u, x), ge#(s x, s y) -> ge#(x, y))
(prod# xs -> prodIter#(xs, s 0()), prodIter#(xs, x) -> ifProd#(isempty xs, xs, x))
(prod# xs -> prodIter#(xs, s 0()), prodIter#(xs, x) -> isempty# xs)}
STATUS:
arrows: 0.903061
SCCS (4):
Scc:
{ prodIter#(xs, x) -> ifProd#(isempty xs, xs, x),
ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs))}
Scc:
{ timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u),
ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u)}
Scc:
{ge#(s x, s y) -> ge#(x, y)}
Scc:
{plus#(s x, y) -> plus#(x, y)}
SCC (2):
Strict:
{ prodIter#(xs, x) -> ifProd#(isempty xs, xs, x),
ifProd#(false(), xs, x) -> prodIter#(tail xs, times(x, head xs))}
Weak:
{ prodIter(xs, x) -> ifProd(isempty xs, xs, x),
prod xs -> prodIter(xs, s 0()),
ifProd(true(), xs, x) -> x,
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,
times(x, y) -> timesIter(x, y, 0(), 0()),
head nil() -> error(),
head cons(x, xs) -> x,
plus(s x, y) -> s plus(x, y),
plus(0(), y) -> y,
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),
ge(x, 0()) -> true(),
ge(s x, s y) -> ge(x, y),
ge(0(), s y) -> false(),
a() -> b(),
a() -> c()}
Fail
SCC (2):
Strict:
{ timesIter#(x, y, z, u) -> ifTimes#(ge(u, x), x, y, z, u),
ifTimes#(false(), x, y, z, u) -> timesIter#(x, y, plus(y, z), s u)}
Weak:
{ prodIter(xs, x) -> ifProd(isempty xs, xs, x),
prod xs -> prodIter(xs, s 0()),
ifProd(true(), xs, x) -> x,
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,
times(x, y) -> timesIter(x, y, 0(), 0()),
head nil() -> error(),
head cons(x, xs) -> x,
plus(s x, y) -> s plus(x, y),
plus(0(), y) -> y,
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),
ge(x, 0()) -> true(),
ge(s x, s y) -> ge(x, y),
ge(0(), s y) -> false(),
a() -> b(),
a() -> c()}
Fail
SCC (1):
Strict:
{ge#(s x, s y) -> ge#(x, y)}
Weak:
{ prodIter(xs, x) -> ifProd(isempty xs, xs, x),
prod xs -> prodIter(xs, s 0()),
ifProd(true(), xs, x) -> x,
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,
times(x, y) -> timesIter(x, y, 0(), 0()),
head nil() -> error(),
head cons(x, xs) -> x,
plus(s x, y) -> s plus(x, y),
plus(0(), y) -> y,
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),
ge(x, 0()) -> true(),
ge(s x, s y) -> ge(x, y),
ge(0(), s y) -> false(),
a() -> b(),
a() -> c()}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[ifTimes](x0, x1, x2, x3, x4) = x0 + x1 + x2,
[timesIter](x0, x1, x2, x3) = x0 + x1 + x2,
[ifProd](x0, x1, x2) = x0 + x1 + 1,
[prodIter](x0, x1) = 0,
[times](x0, x1) = x0,
[plus](x0, x1) = x0 + 1,
[ge](x0, x1) = x0 + x1,
[cons](x0, x1) = 1,
[s](x0) = x0 + 1,
[prod](x0) = 0,
[isempty](x0) = x0 + 1,
[tail](x0) = x0 + 1,
[head](x0) = 1,
[0] = 1,
[true] = 0,
[false] = 1,
[nil] = 1,
[error] = 0,
[b] = 0,
[a] = 0,
[c] = 0,
[ge#](x0, x1) = x0
Strict:
ge#(s x, s y) -> ge#(x, y)
1 + 0x + 1y >= 0 + 0x + 1y
Weak:
a() -> c()
0 >= 0
a() -> b()
0 >= 0
ge(0(), s y) -> false()
2 + 1y >= 1
ge(s x, s y) -> ge(x, y)
2 + 1x + 1y >= 0 + 1x + 1y
ge(x, 0()) -> true()
1 + 1x >= 0
ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u)
1 + 1x + 0y + 1u + 0z >= 2 + 0x + 2y + 1u + 0z
ifTimes(true(), x, y, z, u) -> z
0 + 1x + 0y + 1u + 0z >= 1z
timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u)
0 + 0x + 1y + 1u + 1z >= 0 + 2x + 0y + 2u + 0z
plus(0(), y) -> y
2 + 0y >= 1y
plus(s x, y) -> s plus(x, y)
2 + 1x + 0y >= 2 + 1x + 0y
head cons(x, xs) -> x
1 + 0xs + 0x >= 1x
head nil() -> error()
1 >= 0
times(x, y) -> timesIter(x, y, 0(), 0())
0 + 0x + 1y >= 2 + 0x + 1y
tail cons(x, xs) -> xs
2 + 0xs + 0x >= 1xs
tail nil() -> nil()
2 >= 1
isempty cons(x, xs) -> false()
2 + 0xs + 0x >= 1
isempty nil() -> true()
2 >= 0
ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs))
2 + 1xs + 0x >= 0 + 0xs + 0x
ifProd(true(), xs, x) -> x
1 + 1xs + 0x >= 1x
prod xs -> prodIter(xs, s 0())
0 + 0xs >= 0 + 0xs
prodIter(xs, x) -> ifProd(isempty xs, xs, x)
0 + 0xs + 0x >= 2 + 2xs + 0x
Qed
SCC (1):
Strict:
{plus#(s x, y) -> plus#(x, y)}
Weak:
{ prodIter(xs, x) -> ifProd(isempty xs, xs, x),
prod xs -> prodIter(xs, s 0()),
ifProd(true(), xs, x) -> x,
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,
times(x, y) -> timesIter(x, y, 0(), 0()),
head nil() -> error(),
head cons(x, xs) -> x,
plus(s x, y) -> s plus(x, y),
plus(0(), y) -> y,
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),
ge(x, 0()) -> true(),
ge(s x, s y) -> ge(x, y),
ge(0(), s y) -> false(),
a() -> b(),
a() -> c()}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[ifTimes](x0, x1, x2, x3, x4) = x0 + x1 + x2 + 1,
[timesIter](x0, x1, x2, x3) = 0,
[ifProd](x0, x1, x2) = x0 + x1 + 1,
[prodIter](x0, x1) = 0,
[times](x0, x1) = x0 + 1,
[plus](x0, x1) = x0 + 1,
[ge](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = 1,
[s](x0) = x0 + 1,
[prod](x0) = 0,
[isempty](x0) = x0 + 1,
[tail](x0) = x0 + 1,
[head](x0) = 1,
[0] = 1,
[true] = 0,
[false] = 1,
[nil] = 1,
[error] = 0,
[b] = 0,
[a] = 0,
[c] = 0,
[plus#](x0, x1) = x0
Strict:
plus#(s x, y) -> plus#(x, y)
1 + 1x + 0y >= 0 + 1x + 0y
Weak:
a() -> c()
0 >= 0
a() -> b()
0 >= 0
ge(0(), s y) -> false()
3 + 1y >= 1
ge(s x, s y) -> ge(x, y)
3 + 1x + 1y >= 1 + 1x + 1y
ge(x, 0()) -> true()
2 + 1x >= 0
ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s u)
2 + 1x + 0y + 1u + 0z >= 0 + 0x + 0y + 0u + 0z
ifTimes(true(), x, y, z, u) -> z
1 + 1x + 0y + 1u + 0z >= 1z
timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u)
0 + 0x + 0y + 0u + 0z >= 2 + 2x + 0y + 2u + 0z
plus(0(), y) -> y
2 + 0y >= 1y
plus(s x, y) -> s plus(x, y)
2 + 1x + 0y >= 2 + 1x + 0y
head cons(x, xs) -> x
1 + 0xs + 0x >= 1x
head nil() -> error()
1 >= 0
times(x, y) -> timesIter(x, y, 0(), 0())
1 + 0x + 1y >= 0 + 0x + 0y
tail cons(x, xs) -> xs
2 + 0xs + 0x >= 1xs
tail nil() -> nil()
2 >= 1
isempty cons(x, xs) -> false()
2 + 0xs + 0x >= 1
isempty nil() -> true()
2 >= 0
ifProd(false(), xs, x) -> prodIter(tail xs, times(x, head xs))
2 + 1xs + 0x >= 0 + 0xs + 0x
ifProd(true(), xs, x) -> x
1 + 1xs + 0x >= 1x
prod xs -> prodIter(xs, s 0())
0 + 0xs >= 0 + 0xs
prodIter(xs, x) -> ifProd(isempty xs, xs, x)
0 + 0xs + 0x >= 2 + 2xs + 0x
Qed