MAYBE
Time: 1.053933
TRS:
{ permute(x, y, a()) -> permute(isZero x, x, b()),
permute(y, x, c()) -> s s permute(x, y, a()),
permute(false(), x, b()) -> permute(ack(x, x), p x, c()),
permute(true(), x, b()) -> 0(),
double x -> permute(x, x, a()),
isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y)}
DP:
DP:
{ permute#(x, y, a()) -> permute#(isZero x, x, b()),
permute#(x, y, a()) -> isZero# x,
permute#(y, x, c()) -> permute#(x, y, a()),
permute#(false(), x, b()) -> permute#(ack(x, x), p x, c()),
permute#(false(), x, b()) -> ack#(x, x),
permute#(false(), x, b()) -> p# x,
double# x -> permute#(x, x, a()),
ack#(0(), x) -> plus#(x, s 0()),
ack#(s x, 0()) -> ack#(x, s 0()),
ack#(s x, s y) -> ack#(x, ack(s x, y)),
ack#(s x, s y) -> ack#(s x, y),
plus#(x, s s y) -> plus#(s x, y),
plus#(s x, y) -> plus#(x, s y)}
TRS:
{ permute(x, y, a()) -> permute(isZero x, x, b()),
permute(y, x, c()) -> s s permute(x, y, a()),
permute(false(), x, b()) -> permute(ack(x, x), p x, c()),
permute(true(), x, b()) -> 0(),
double x -> permute(x, x, a()),
isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y)}
UR:
{ isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y),
d(z, w) -> z,
d(z, w) -> w}
EDG:
{(ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y))
(ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y)))
(ack#(s x, 0()) -> ack#(x, s 0()), ack#(0(), x) -> plus#(x, s 0()))
(permute#(y, x, c()) -> permute#(x, y, a()), permute#(x, y, a()) -> isZero# x)
(permute#(y, x, c()) -> permute#(x, y, a()), permute#(x, y, a()) -> permute#(isZero x, x, b()))
(double# x -> permute#(x, x, a()), permute#(x, y, a()) -> isZero# x)
(double# x -> permute#(x, x, a()), permute#(x, y, a()) -> permute#(isZero x, x, b()))
(plus#(x, s s y) -> plus#(s x, y), plus#(s x, y) -> plus#(x, s y))
(plus#(x, s s y) -> plus#(s x, y), plus#(x, s s y) -> plus#(s x, y))
(permute#(false(), x, b()) -> ack#(x, x), ack#(s x, s y) -> ack#(s x, y))
(permute#(false(), x, b()) -> ack#(x, x), ack#(s x, s y) -> ack#(x, ack(s x, y)))
(permute#(false(), x, b()) -> ack#(x, x), ack#(s x, 0()) -> ack#(x, s 0()))
(permute#(false(), x, b()) -> ack#(x, x), ack#(0(), x) -> plus#(x, s 0()))
(ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(0(), x) -> plus#(x, s 0()))
(ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, 0()) -> ack#(x, s 0()))
(ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y)))
(ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y))
(plus#(s x, y) -> plus#(x, s y), plus#(x, s s y) -> plus#(s x, y))
(plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, s y))
(ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0()))
(ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, ack(s x, y)))
(ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y))
(permute#(false(), x, b()) -> permute#(ack(x, x), p x, c()), permute#(y, x, c()) -> permute#(x, y, a()))
(permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(false(), x, b()) -> permute#(ack(x, x), p x, c()))
(permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(false(), x, b()) -> ack#(x, x))
(permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(false(), x, b()) -> p# x)
(ack#(0(), x) -> plus#(x, s 0()), plus#(s x, y) -> plus#(x, s y))}
STATUS:
arrows: 0.840237
SCCS (3):
Scc:
{ permute#(x, y, a()) -> permute#(isZero x, x, b()),
permute#(y, x, c()) -> permute#(x, y, a()),
permute#(false(), x, b()) -> permute#(ack(x, x), p x, c())}
Scc:
{ack#(s x, 0()) -> ack#(x, s 0()),
ack#(s x, s y) -> ack#(x, ack(s x, y)),
ack#(s x, s y) -> ack#(s x, y)}
Scc:
{plus#(x, s s y) -> plus#(s x, y),
plus#(s x, y) -> plus#(x, s y)}
SCC (3):
Strict:
{ permute#(x, y, a()) -> permute#(isZero x, x, b()),
permute#(y, x, c()) -> permute#(x, y, a()),
permute#(false(), x, b()) -> permute#(ack(x, x), p x, c())}
Weak:
{ permute(x, y, a()) -> permute(isZero x, x, b()),
permute(y, x, c()) -> s s permute(x, y, a()),
permute(false(), x, b()) -> permute(ack(x, x), p x, c()),
permute(true(), x, b()) -> 0(),
double x -> permute(x, x, a()),
isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y)}
Fail
SCC (3):
Strict:
{ack#(s x, 0()) -> ack#(x, s 0()),
ack#(s x, s y) -> ack#(x, ack(s x, y)),
ack#(s x, s y) -> ack#(s x, y)}
Weak:
{ permute(x, y, a()) -> permute(isZero x, x, b()),
permute(y, x, c()) -> s s permute(x, y, a()),
permute(false(), x, b()) -> permute(ack(x, x), p x, c()),
permute(true(), x, b()) -> 0(),
double x -> permute(x, x, a()),
isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[permute](x0, x1, x2) = x0 + x1,
[ack](x0, x1) = 0,
[plus](x0, x1) = 0,
[double](x0) = 0,
[isZero](x0) = x0,
[p](x0) = 0,
[s](x0) = x0 + 1,
[a] = 0,
[b] = 0,
[c] = 0,
[false] = 0,
[0] = 0,
[true] = 0,
[ack#](x0, x1) = x0
Strict:
ack#(s x, s y) -> ack#(s x, y)
1 + 1x + 0y >= 1 + 1x + 0y
ack#(s x, s y) -> ack#(x, ack(s x, y))
1 + 1x + 0y >= 0 + 1x + 0y
ack#(s x, 0()) -> ack#(x, s 0())
1 + 1x >= 0 + 1x
Weak:
plus(s x, y) -> plus(x, s y)
0 + 0x + 0y >= 0 + 0x + 0y
plus(0(), y) -> y
0 + 0y >= 1y
plus(x, s s y) -> s plus(s x, y)
0 + 0x + 0y >= 1 + 0x + 0y
plus(x, s 0()) -> s x
0 + 0x >= 1 + 1x
plus(x, 0()) -> x
0 + 0x >= 1x
p s x -> x
0 + 0x >= 1x
p 0() -> 0()
0 >= 0
ack(s x, s y) -> ack(x, ack(s x, y))
0 + 0x + 0y >= 0 + 0x + 0y
ack(s x, 0()) -> ack(x, s 0())
0 + 0x >= 0 + 0x
ack(0(), x) -> plus(x, s 0())
0 + 0x >= 0 + 0x
isZero s x -> false()
1 + 1x >= 0
isZero 0() -> true()
0 >= 0
double x -> permute(x, x, a())
0 + 0x >= 0 + 2x
permute(true(), x, b()) -> 0()
0 + 1x >= 0
permute(false(), x, b()) -> permute(ack(x, x), p x, c())
0 + 1x >= 0 + 0x
permute(y, x, c()) -> s s permute(x, y, a())
0 + 1x + 1y >= 2 + 1x + 1y
permute(x, y, a()) -> permute(isZero x, x, b())
0 + 1x + 1y >= 0 + 2x
SCCS (1):
Scc:
{ack#(s x, s y) -> ack#(s x, y)}
SCC (1):
Strict:
{ack#(s x, s y) -> ack#(s x, y)}
Weak:
{ permute(x, y, a()) -> permute(isZero x, x, b()),
permute(y, x, c()) -> s s permute(x, y, a()),
permute(false(), x, b()) -> permute(ack(x, x), p x, c()),
permute(true(), x, b()) -> 0(),
double x -> permute(x, x, a()),
isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[permute](x0, x1, x2) = x0 + x1,
[ack](x0, x1) = 1,
[plus](x0, x1) = 0,
[double](x0) = 0,
[isZero](x0) = x0,
[p](x0) = x0 + 1,
[s](x0) = x0 + 1,
[a] = 0,
[b] = 0,
[c] = 0,
[false] = 0,
[0] = 0,
[true] = 0,
[ack#](x0, x1) = x0 + 1
Strict:
ack#(s x, s y) -> ack#(s x, y)
2 + 0x + 1y >= 1 + 0x + 1y
Weak:
plus(s x, y) -> plus(x, s y)
0 + 0x + 0y >= 0 + 0x + 0y
plus(0(), y) -> y
0 + 0y >= 1y
plus(x, s s y) -> s plus(s x, y)
0 + 0x + 0y >= 1 + 0x + 0y
plus(x, s 0()) -> s x
0 + 0x >= 1 + 1x
plus(x, 0()) -> x
0 + 0x >= 1x
p s x -> x
2 + 1x >= 1x
p 0() -> 0()
1 >= 0
ack(s x, s y) -> ack(x, ack(s x, y))
1 + 0x + 0y >= 1 + 0x + 0y
ack(s x, 0()) -> ack(x, s 0())
1 + 0x >= 1 + 0x
ack(0(), x) -> plus(x, s 0())
1 + 0x >= 0 + 0x
isZero s x -> false()
1 + 1x >= 0
isZero 0() -> true()
0 >= 0
double x -> permute(x, x, a())
0 + 0x >= 0 + 2x
permute(true(), x, b()) -> 0()
0 + 1x >= 0
permute(false(), x, b()) -> permute(ack(x, x), p x, c())
0 + 1x >= 2 + 1x
permute(y, x, c()) -> s s permute(x, y, a())
0 + 1x + 1y >= 2 + 1x + 1y
permute(x, y, a()) -> permute(isZero x, x, b())
0 + 1x + 1y >= 0 + 2x
Qed
SCC (2):
Strict:
{plus#(x, s s y) -> plus#(s x, y),
plus#(s x, y) -> plus#(x, s y)}
Weak:
{ permute(x, y, a()) -> permute(isZero x, x, b()),
permute(y, x, c()) -> s s permute(x, y, a()),
permute(false(), x, b()) -> permute(ack(x, x), p x, c()),
permute(true(), x, b()) -> 0(),
double x -> permute(x, x, a()),
isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[permute](x0, x1, x2) = x0 + x1,
[ack](x0, x1) = 1,
[plus](x0, x1) = 0,
[double](x0) = 0,
[isZero](x0) = x0,
[p](x0) = x0 + 1,
[s](x0) = x0 + 1,
[a] = 0,
[b] = 0,
[c] = 0,
[false] = 0,
[0] = 0,
[true] = 0,
[plus#](x0, x1) = x0 + x1
Strict:
plus#(s x, y) -> plus#(x, s y)
1 + 1x + 1y >= 1 + 1x + 1y
plus#(x, s s y) -> plus#(s x, y)
2 + 1x + 1y >= 1 + 1x + 1y
Weak:
plus(s x, y) -> plus(x, s y)
0 + 0x + 0y >= 0 + 0x + 0y
plus(0(), y) -> y
0 + 0y >= 1y
plus(x, s s y) -> s plus(s x, y)
0 + 0x + 0y >= 1 + 0x + 0y
plus(x, s 0()) -> s x
0 + 0x >= 1 + 1x
plus(x, 0()) -> x
0 + 0x >= 1x
p s x -> x
2 + 1x >= 1x
p 0() -> 0()
1 >= 0
ack(s x, s y) -> ack(x, ack(s x, y))
1 + 0x + 0y >= 1 + 0x + 0y
ack(s x, 0()) -> ack(x, s 0())
1 + 0x >= 1 + 0x
ack(0(), x) -> plus(x, s 0())
1 + 0x >= 0 + 0x
isZero s x -> false()
1 + 1x >= 0
isZero 0() -> true()
0 >= 0
double x -> permute(x, x, a())
0 + 0x >= 0 + 2x
permute(true(), x, b()) -> 0()
0 + 1x >= 0
permute(false(), x, b()) -> permute(ack(x, x), p x, c())
0 + 1x >= 2 + 1x
permute(y, x, c()) -> s s permute(x, y, a())
0 + 1x + 1y >= 2 + 1x + 1y
permute(x, y, a()) -> permute(isZero x, x, b())
0 + 1x + 1y >= 0 + 2x
SCCS (1):
Scc:
{plus#(s x, y) -> plus#(x, s y)}
SCC (1):
Strict:
{plus#(s x, y) -> plus#(x, s y)}
Weak:
{ permute(x, y, a()) -> permute(isZero x, x, b()),
permute(y, x, c()) -> s s permute(x, y, a()),
permute(false(), x, b()) -> permute(ack(x, x), p x, c()),
permute(true(), x, b()) -> 0(),
double x -> permute(x, x, a()),
isZero 0() -> true(),
isZero s x -> false(),
ack(0(), x) -> plus(x, s 0()),
ack(s x, 0()) -> ack(x, s 0()),
ack(s x, s y) -> ack(x, ack(s x, y)),
p 0() -> 0(),
p s x -> x,
plus(x, 0()) -> x,
plus(x, s 0()) -> s x,
plus(x, s s y) -> s plus(s x, y),
plus(0(), y) -> y,
plus(s x, y) -> plus(x, s y)}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[permute](x0, x1, x2) = x0 + x1,
[ack](x0, x1) = 1,
[plus](x0, x1) = 0,
[double](x0) = 0,
[isZero](x0) = x0,
[p](x0) = x0 + 1,
[s](x0) = x0 + 1,
[a] = 0,
[b] = 0,
[c] = 0,
[false] = 0,
[0] = 0,
[true] = 0,
[plus#](x0, x1) = x0 + 1
Strict:
plus#(s x, y) -> plus#(x, s y)
2 + 1x + 0y >= 1 + 1x + 0y
Weak:
plus(s x, y) -> plus(x, s y)
0 + 0x + 0y >= 0 + 0x + 0y
plus(0(), y) -> y
0 + 0y >= 1y
plus(x, s s y) -> s plus(s x, y)
0 + 0x + 0y >= 1 + 0x + 0y
plus(x, s 0()) -> s x
0 + 0x >= 1 + 1x
plus(x, 0()) -> x
0 + 0x >= 1x
p s x -> x
2 + 1x >= 1x
p 0() -> 0()
1 >= 0
ack(s x, s y) -> ack(x, ack(s x, y))
1 + 0x + 0y >= 1 + 0x + 0y
ack(s x, 0()) -> ack(x, s 0())
1 + 0x >= 1 + 0x
ack(0(), x) -> plus(x, s 0())
1 + 0x >= 0 + 0x
isZero s x -> false()
1 + 1x >= 0
isZero 0() -> true()
0 >= 0
double x -> permute(x, x, a())
0 + 0x >= 0 + 2x
permute(true(), x, b()) -> 0()
0 + 1x >= 0
permute(false(), x, b()) -> permute(ack(x, x), p x, c())
0 + 1x >= 2 + 1x
permute(y, x, c()) -> s s permute(x, y, a())
0 + 1x + 1y >= 2 + 1x + 1y
permute(x, y, a()) -> permute(isZero x, x, b())
0 + 1x + 1y >= 0 + 2x
Qed