MAYBE
Time: 0.178989
TRS:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X,
top mark X -> top proper X,
top ok X -> top active X}
DP:
DP:
{ cons#(mark X1, X2) -> cons#(X1, X2),
cons#(ok X1, ok X2) -> cons#(X1, X2),
active# cons(X1, X2) -> cons#(active X1, X2),
active# cons(X1, X2) -> active# X1,
active# zeros() -> cons#(0(), zeros()),
active# and(X1, X2) -> active# X1,
active# and(X1, X2) -> and#(active X1, X2),
active# length X -> active# X,
active# length X -> length# active X,
active# length cons(N, L) -> length# L,
active# length cons(N, L) -> s# length L,
active# s X -> active# X,
active# s X -> s# active X,
and#(mark X1, X2) -> and#(X1, X2),
and#(ok X1, ok X2) -> and#(X1, X2),
length# mark X -> length# X,
length# ok X -> length# X,
s# mark X -> s# X,
s# ok X -> s# X,
proper# cons(X1, X2) -> cons#(proper X1, proper X2),
proper# cons(X1, X2) -> proper# X1,
proper# cons(X1, X2) -> proper# X2,
proper# and(X1, X2) -> and#(proper X1, proper X2),
proper# and(X1, X2) -> proper# X1,
proper# and(X1, X2) -> proper# X2,
proper# length X -> length# proper X,
proper# length X -> proper# X,
proper# s X -> s# proper X,
proper# s X -> proper# X,
top# mark X -> proper# X,
top# mark X -> top# proper X,
top# ok X -> active# X,
top# ok X -> top# active X}
TRS:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X,
top mark X -> top proper X,
top ok X -> top active X}
UR:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X}
EDG:
{(active# s X -> active# X, active# s X -> s# active X)
(active# s X -> active# X, active# s X -> active# X)
(active# s X -> active# X, active# length cons(N, L) -> s# length L)
(active# s X -> active# X, active# length cons(N, L) -> length# L)
(active# s X -> active# X, active# length X -> length# active X)
(active# s X -> active# X, active# length X -> active# X)
(active# s X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
(active# s X -> active# X, active# and(X1, X2) -> active# X1)
(active# s X -> active# X, active# cons(X1, X2) -> active# X1)
(active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(top# ok X -> active# X, active# s X -> s# active X)
(top# ok X -> active# X, active# s X -> active# X)
(top# ok X -> active# X, active# length cons(N, L) -> s# length L)
(top# ok X -> active# X, active# length cons(N, L) -> length# L)
(top# ok X -> active# X, active# length X -> length# active X)
(top# ok X -> active# X, active# length X -> active# X)
(top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
(top# ok X -> active# X, active# and(X1, X2) -> active# X1)
(top# ok X -> active# X, active# cons(X1, X2) -> active# X1)
(top# ok X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# s X -> s# active X)
(active# and(X1, X2) -> active# X1, active# s X -> active# X)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# and(X1, X2) -> active# X1, active# length X -> length# active X)
(active# and(X1, X2) -> active# X1, active# length X -> active# X)
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
(active# length X -> length# active X, length# ok X -> length# X)
(active# length X -> length# active X, length# mark X -> length# X)
(proper# length X -> length# proper X, length# ok X -> length# X)
(top# mark X -> top# proper X, top# ok X -> top# active X)
(top# mark X -> top# proper X, top# ok X -> active# X)
(top# mark X -> top# proper X, top# mark X -> top# proper X)
(top# mark X -> top# proper X, top# mark X -> proper# X)
(top# ok X -> top# active X, top# mark X -> proper# X)
(top# ok X -> top# active X, top# mark X -> top# proper X)
(top# ok X -> top# active X, top# ok X -> active# X)
(top# ok X -> top# active X, top# ok X -> top# active X)
(proper# s X -> s# proper X, s# ok X -> s# X)
(active# s X -> s# active X, s# mark X -> s# X)
(active# s X -> s# active X, s# ok X -> s# X)
(active# length cons(N, L) -> s# length L, s# mark X -> s# X)
(active# length cons(N, L) -> s# length L, s# ok X -> s# X)
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# length X -> active# X)
(active# cons(X1, X2) -> active# X1, active# length X -> length# active X)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# cons(X1, X2) -> active# X1, active# s X -> active# X)
(active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
(active# length X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(active# length X -> active# X, active# cons(X1, X2) -> active# X1)
(active# length X -> active# X, active# and(X1, X2) -> active# X1)
(active# length X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
(active# length X -> active# X, active# length X -> active# X)
(active# length X -> active# X, active# length X -> length# active X)
(active# length X -> active# X, active# length cons(N, L) -> length# L)
(active# length X -> active# X, active# length cons(N, L) -> s# length L)
(active# length X -> active# X, active# s X -> active# X)
(active# length X -> active# X, active# s X -> s# active X)}
STATUS:
arrows: 0.935721
SCCS (2):
Scc:
{top# mark X -> top# proper X,
top# ok X -> top# active X}
Scc:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1,
active# length X -> active# X,
active# s X -> active# X}
SCC (2):
Strict:
{top# mark X -> top# proper X,
top# ok X -> top# active X}
Weak:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X,
top mark X -> top proper X,
top ok X -> top active X}
Fail
SCC (4):
Strict:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1,
active# length X -> active# X,
active# s X -> active# X}
Weak:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[cons](x0, x1) = x0 + x1,
[and](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[length](x0) = x0,
[s](x0) = x0 + 1,
[ok](x0) = x0 + 1,
[proper](x0) = 0,
[top](x0) = 0,
[0] = 0,
[zeros] = 0,
[tt] = 0,
[nil] = 0,
[active#](x0) = x0
Strict:
active# s X -> active# X
1 + 1X >= 0 + 1X
active# length X -> active# X
0 + 1X >= 0 + 1X
active# and(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
active# cons(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 1
proper length X -> length proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper and(X1, X2) -> and(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper zeros() -> ok zeros()
0 >= 1
proper 0() -> ok 0()
0 >= 1
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
1 + 0X >= 0 + 0X
length ok X -> ok length X
1 + 1X >= 1 + 1X
length mark X -> mark length X
0 + 0X >= 0 + 0X
and(ok X1, ok X2) -> ok and(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
and(mark X1, X2) -> mark and(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
active s X -> s active X
0 + 0X >= 1 + 0X
active length nil() -> mark 0()
0 >= 0
active length cons(N, L) -> mark s length L
0 + 0L + 0N >= 0 + 0L
active length X -> length active X
0 + 0X >= 0 + 0X
active and(tt(), X) -> mark X
0 + 0X >= 0 + 0X
active and(X1, X2) -> and(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active zeros() -> mark cons(0(), zeros())
0 >= 0
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1,
active# length X -> active# X}
SCC (3):
Strict:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1,
active# length X -> active# X}
Weak:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[cons](x0, x1) = x0 + x1,
[and](x0, x1) = x0 + x1,
[mark](x0) = 0,
[active](x0) = 0,
[length](x0) = x0 + 1,
[s](x0) = x0 + 1,
[ok](x0) = x0 + 1,
[proper](x0) = 0,
[top](x0) = 0,
[0] = 1,
[zeros] = 1,
[tt] = 0,
[nil] = 1,
[active#](x0) = x0
Strict:
active# length X -> active# X
1 + 1X >= 0 + 1X
active# and(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
active# cons(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper s X -> s proper X
0 + 0X >= 1 + 0X
proper nil() -> ok nil()
0 >= 2
proper length X -> length proper X
0 + 0X >= 1 + 0X
proper tt() -> ok tt()
0 >= 1
proper and(X1, X2) -> and(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
proper zeros() -> ok zeros()
0 >= 2
proper 0() -> ok 0()
0 >= 2
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
s ok X -> ok s X
2 + 1X >= 2 + 1X
s mark X -> mark s X
1 + 0X >= 0 + 0X
length ok X -> ok length X
2 + 1X >= 2 + 1X
length mark X -> mark length X
1 + 0X >= 0 + 0X
and(ok X1, ok X2) -> ok and(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
and(mark X1, X2) -> mark and(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
active s X -> s active X
0 + 0X >= 1 + 0X
active length nil() -> mark 0()
0 >= 0
active length cons(N, L) -> mark s length L
0 + 0L + 0N >= 0 + 0L
active length X -> length active X
0 + 0X >= 1 + 0X
active and(tt(), X) -> mark X
0 + 0X >= 0 + 0X
active and(X1, X2) -> and(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
active zeros() -> mark cons(0(), zeros())
0 >= 0
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1}
SCC (2):
Strict:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1}
Weak:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[cons](x0, x1) = x0 + x1,
[and](x0, x1) = x0 + 1,
[mark](x0) = 0,
[active](x0) = 0,
[length](x0) = 0,
[s](x0) = 0,
[ok](x0) = 1,
[proper](x0) = 0,
[top](x0) = 0,
[0] = 1,
[zeros] = 1,
[tt] = 1,
[nil] = 0,
[active#](x0) = x0
Strict:
active# and(X1, X2) -> active# X1
1 + 1X1 + 0X2 >= 0 + 1X1
active# cons(X1, X2) -> active# X1
0 + 1X1 + 1X2 >= 0 + 1X1
Weak:
top ok X -> top active X
0 + 0X >= 0 + 0X
top mark X -> top proper X
0 + 0X >= 0 + 0X
proper s X -> s proper X
0 + 0X >= 0 + 0X
proper nil() -> ok nil()
0 >= 1
proper length X -> length proper X
0 + 0X >= 0 + 0X
proper tt() -> ok tt()
0 >= 1
proper and(X1, X2) -> and(proper X1, proper X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
proper zeros() -> ok zeros()
0 >= 1
proper 0() -> ok 0()
0 >= 1
proper cons(X1, X2) -> cons(proper X1, proper X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
s ok X -> ok s X
0 + 0X >= 1 + 0X
s mark X -> mark s X
0 + 0X >= 0 + 0X
length ok X -> ok length X
0 + 0X >= 1 + 0X
length mark X -> mark length X
0 + 0X >= 0 + 0X
and(ok X1, ok X2) -> ok and(X1, X2)
2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
and(mark X1, X2) -> mark and(X1, X2)
1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
active s X -> s active X
0 + 0X >= 0 + 0X
active length nil() -> mark 0()
0 >= 0
active length cons(N, L) -> mark s length L
0 + 0L + 0N >= 0 + 0L
active length X -> length active X
0 + 0X >= 0 + 0X
active and(tt(), X) -> mark X
0 + 0X >= 0 + 0X
active and(X1, X2) -> and(active X1, X2)
0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
active zeros() -> mark cons(0(), zeros())
0 >= 0
active cons(X1, X2) -> cons(active X1, X2)
0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
SCCS (1):
Scc:
{active# cons(X1, X2) -> active# X1}
SCC (1):
Strict:
{active# cons(X1, X2) -> active# X1}
Weak:
{ cons(mark X1, X2) -> mark cons(X1, X2),
cons(ok X1, ok X2) -> ok cons(X1, X2),
active cons(X1, X2) -> cons(active X1, X2),
active zeros() -> mark cons(0(), zeros()),
active and(X1, X2) -> and(active X1, X2),
active and(tt(), X) -> mark X,
active length X -> length active X,
active length cons(N, L) -> mark s length L,
active length nil() -> mark 0(),
active s X -> s active X,
and(mark X1, X2) -> mark and(X1, X2),
and(ok X1, ok X2) -> ok and(X1, X2),
length mark X -> mark length X,
length ok X -> ok length X,
s mark X -> mark s X,
s ok X -> ok s X,
proper cons(X1, X2) -> cons(proper X1, proper X2),
proper 0() -> ok 0(),
proper zeros() -> ok zeros(),
proper and(X1, X2) -> and(proper X1, proper X2),
proper tt() -> ok tt(),
proper length X -> length proper X,
proper nil() -> ok nil(),
proper s X -> s proper X,
top mark X -> top proper X,
top ok X -> top active X}
POLY:
Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
Interpretation:
[cons](x0, x1) = x0 + 1,
[and](x0, x1) = x0 + 1,
[mark](x0) = x0 + 1,
[active](x0) = x0 + 1,
[length](x0) = x0 + 1,
[s](x0) = x0 + 1,
[ok](x0) = 1,
[proper](x0) = x0 + 1,
[top](x0) = x0 + 1,
[0] = 1,
[zeros] = 1,
[tt] = 0,
[nil] = 0,
[active#](x0) = x0
Strict:
active# cons(X1, X2) -> active# X1
1 + 1X1 + 0X2 >= 0 + 1X1
Weak:
top ok X -> top active X
2 + 0X >= 2 + 1X
top mark X -> top proper X
2 + 1X >= 2 + 1X
proper s X -> s proper X
2 + 1X >= 2 + 1X
proper nil() -> ok nil()
1 >= 1
proper length X -> length proper X
2 + 1X >= 2 + 1X
proper tt() -> ok tt()
1 >= 1
proper and(X1, X2) -> and(proper X1, proper X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
proper zeros() -> ok zeros()
2 >= 1
proper 0() -> ok 0()
2 >= 1
proper cons(X1, X2) -> cons(proper X1, proper X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
s ok X -> ok s X
2 + 0X >= 1 + 0X
s mark X -> mark s X
2 + 1X >= 2 + 1X
length ok X -> ok length X
2 + 0X >= 1 + 0X
length mark X -> mark length X
2 + 1X >= 2 + 1X
and(ok X1, ok X2) -> ok and(X1, X2)
2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
and(mark X1, X2) -> mark and(X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
active s X -> s active X
2 + 1X >= 2 + 1X
active length nil() -> mark 0()
2 >= 2
active length cons(N, L) -> mark s length L
3 + 0L + 1N >= 3 + 1L
active length X -> length active X
2 + 1X >= 2 + 1X
active and(tt(), X) -> mark X
2 + 0X >= 1 + 1X
active and(X1, X2) -> and(active X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
active zeros() -> mark cons(0(), zeros())
2 >= 3
active cons(X1, X2) -> cons(active X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
cons(ok X1, ok X2) -> ok cons(X1, X2)
2 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
cons(mark X1, X2) -> mark cons(X1, X2)
2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
Qed