MAYBE
Time: 0.563600
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
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,
active# take(X1, X2) -> active# X1,
active# take(X1, X2) -> active# X2,
active# take(X1, X2) -> take#(X1, active X2),
active# take(X1, X2) -> take#(active X1, X2),
active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)),
active# take(s M, cons(N, IL)) -> take#(M, IL),
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,
take#(X1, mark X2) -> take#(X1, X2),
take#(mark X1, X2) -> take#(X1, X2),
take#(ok X1, ok X2) -> take#(X1, X2),
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,
proper# take(X1, X2) -> take#(proper X1, proper X2),
proper# take(X1, X2) -> proper# X1,
proper# take(X1, X2) -> proper# X2,
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2)}
EDG:
{
(active# s X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# s X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# s X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(active# s X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(active# s X -> active# X, active# take(X1, X2) -> active# X2)
(active# s X -> active# X, active# take(X1, X2) -> active# X1)
(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# zeros() -> cons#(0(), zeros()))
(active# s X -> active# X, active# cons(X1, X2) -> active# X1)
(active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(length# ok X -> length# X, length# ok X -> length# X)
(length# ok X -> length# X, length# mark X -> length# X)
(s# ok X -> s# X, s# ok X -> s# X)
(s# ok X -> s# X, s# mark X -> s# X)
(proper# s X -> proper# X, proper# take(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# take(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# s X -> proper# X, proper# s X -> proper# X)
(proper# s X -> proper# X, proper# s X -> s# proper X)
(proper# s X -> proper# X, proper# length X -> proper# X)
(proper# s X -> proper# X, proper# length X -> length# proper X)
(proper# s X -> proper# X, proper# and(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# and(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(top# ok X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
(top# ok X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(top# ok X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(top# ok X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(top# ok X -> active# X, active# take(X1, X2) -> active# X2)
(top# ok X -> active# X, active# take(X1, X2) -> active# X1)
(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# zeros() -> cons#(0(), zeros()))
(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# length cons(N, L) -> length# L, length# ok X -> length# X)
(active# length cons(N, L) -> length# L, length# mark X -> length# X)
(active# take(X1, X2) -> take#(X1, active X2), take#(ok X1, ok X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(X1, active X2), take#(mark X1, X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(X1, active X2), take#(X1, mark X2) -> take#(X1, X2))
(proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
(proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
(active# length cons(N, L) -> s# length L, s# ok X -> s# X)
(active# length cons(N, L) -> s# length L, s# mark X -> s# X)
(active# s X -> s# active X, s# ok X -> s# X)
(active# s X -> s# active X, s# mark X -> s# X)
(proper# s X -> s# proper X, s# ok X -> s# X)
(proper# s X -> s# proper X, s# mark X -> s# X)
(top# ok X -> top# active X, top# ok X -> top# active X)
(top# ok X -> top# active X, top# ok X -> active# X)
(top# ok X -> top# active X, top# mark X -> top# proper X)
(top# ok X -> top# active X, top# mark X -> proper# X)
(active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(active# cons(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# cons(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
(active# cons(X1, X2) -> active# X1, active# s X -> active# X)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# cons(X1, X2) -> active# X1, active# length X -> length# active X)
(active# cons(X1, X2) -> active# X1, active# length X -> active# X)
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# s X -> s# active X)
(active# take(X1, X2) -> active# X1, active# s X -> active# X)
(active# take(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# take(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# take(X1, X2) -> active# X1, active# length X -> length# active X)
(active# take(X1, X2) -> active# X1, active# length X -> active# X)
(active# take(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# take(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# and(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# and(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# and(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(active# take(X1, X2) -> active# X2, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> active# X2, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> take#(active X1, X2))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> take#(X1, active X2))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> active# X2)
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# s X -> s# active X)
(active# take(X1, X2) -> active# X2, active# s X -> active# X)
(active# take(X1, X2) -> active# X2, active# length cons(N, L) -> s# length L)
(active# take(X1, X2) -> active# X2, active# length cons(N, L) -> length# L)
(active# take(X1, X2) -> active# X2, active# length X -> length# active X)
(active# take(X1, X2) -> active# X2, active# length X -> active# X)
(active# take(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
(active# take(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# zeros() -> cons#(0(), zeros()))
(active# take(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
(proper# and(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# and(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# and(X1, X2) -> proper# X2, proper# length X -> proper# X)
(proper# and(X1, X2) -> proper# X2, proper# length X -> length# proper X)
(proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X2, proper# length X -> length# proper X)
(proper# take(X1, X2) -> proper# X2, proper# length X -> proper# X)
(proper# take(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# take(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# length X -> length# proper X)
(proper# cons(X1, X2) -> proper# X2, proper# length X -> proper# X)
(proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# cons(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2)
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(X1, mark X2) -> take#(X1, X2))
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(mark X1, X2) -> take#(X1, X2))
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# take(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# take(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# take(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# length X -> active# X)
(active# and(X1, X2) -> active# X1, active# length X -> length# active X)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# and(X1, X2) -> active# X1, active# s X -> active# X)
(active# and(X1, X2) -> active# X1, active# s X -> s# active X)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# and(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> take#(active X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(active X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(active X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(top# mark X -> top# proper X, top# mark X -> proper# X)
(top# mark X -> top# proper X, top# mark X -> top# proper X)
(top# mark X -> top# proper X, top# ok X -> active# X)
(top# mark X -> top# proper X, top# ok X -> top# active X)
(proper# length X -> length# proper X, length# mark X -> length# X)
(proper# length X -> length# proper X, length# ok X -> length# X)
(active# length X -> length# active X, length# mark X -> length# X)
(active# length X -> length# active X, length# ok X -> length# X)
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(X1, mark X2) -> take#(X1, X2))
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(mark X1, X2) -> take#(X1, X2))
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(ok X1, ok X2) -> take#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(mark X1, X2) -> cons#(X1, X2))
(active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(ok X1, ok X2) -> cons#(X1, X2))
(active# zeros() -> cons#(0(), zeros()), cons#(mark X1, X2) -> cons#(X1, X2))
(active# zeros() -> cons#(0(), zeros()), cons#(ok X1, ok X2) -> cons#(X1, X2))
(top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# length X -> length# proper X)
(top# mark X -> proper# X, proper# length X -> proper# X)
(top# mark X -> proper# X, proper# s X -> s# proper X)
(top# mark X -> proper# X, proper# s X -> proper# X)
(top# mark X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(top# mark X -> proper# X, proper# take(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# take(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# length X -> proper# X, proper# and(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# and(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# length X -> length# proper X)
(proper# length X -> proper# X, proper# length X -> proper# X)
(proper# length X -> proper# X, proper# s X -> s# proper X)
(proper# length X -> proper# X, proper# s X -> proper# X)
(proper# length X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# length X -> proper# X, proper# take(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# take(X1, X2) -> proper# X2)
(s# mark X -> s# X, s# mark X -> s# X)
(s# mark X -> s# X, s# ok X -> s# X)
(length# mark X -> length# X, length# mark X -> length# X)
(length# mark X -> length# X, length# ok X -> length# 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# zeros() -> cons#(0(), zeros()))
(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)
(active# length X -> active# X, active# take(X1, X2) -> active# X1)
(active# length X -> active# X, active# take(X1, X2) -> active# X2)
(active# length X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(active# length X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(active# length X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# length X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
}
EDG:
{
(active# s X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# s X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# s X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(active# s X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(active# s X -> active# X, active# take(X1, X2) -> active# X2)
(active# s X -> active# X, active# take(X1, X2) -> active# X1)
(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# zeros() -> cons#(0(), zeros()))
(active# s X -> active# X, active# cons(X1, X2) -> active# X1)
(active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(length# ok X -> length# X, length# ok X -> length# X)
(length# ok X -> length# X, length# mark X -> length# X)
(s# ok X -> s# X, s# ok X -> s# X)
(s# ok X -> s# X, s# mark X -> s# X)
(proper# s X -> proper# X, proper# take(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# take(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# s X -> proper# X, proper# s X -> proper# X)
(proper# s X -> proper# X, proper# s X -> s# proper X)
(proper# s X -> proper# X, proper# length X -> proper# X)
(proper# s X -> proper# X, proper# length X -> length# proper X)
(proper# s X -> proper# X, proper# and(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# and(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(top# ok X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
(top# ok X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(top# ok X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(top# ok X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(top# ok X -> active# X, active# take(X1, X2) -> active# X2)
(top# ok X -> active# X, active# take(X1, X2) -> active# X1)
(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# zeros() -> cons#(0(), zeros()))
(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# length cons(N, L) -> length# L, length# ok X -> length# X)
(active# length cons(N, L) -> length# L, length# mark X -> length# X)
(active# take(X1, X2) -> take#(X1, active X2), take#(ok X1, ok X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(X1, active X2), take#(mark X1, X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(X1, active X2), take#(X1, mark X2) -> take#(X1, X2))
(proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
(proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
(active# length cons(N, L) -> s# length L, s# ok X -> s# X)
(active# length cons(N, L) -> s# length L, s# mark X -> s# X)
(active# s X -> s# active X, s# ok X -> s# X)
(active# s X -> s# active X, s# mark X -> s# X)
(proper# s X -> s# proper X, s# ok X -> s# X)
(proper# s X -> s# proper X, s# mark X -> s# X)
(top# ok X -> top# active X, top# ok X -> top# active X)
(top# ok X -> top# active X, top# ok X -> active# X)
(top# ok X -> top# active X, top# mark X -> top# proper X)
(top# ok X -> top# active X, top# mark X -> proper# X)
(active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(active# cons(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# cons(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
(active# cons(X1, X2) -> active# X1, active# s X -> active# X)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# cons(X1, X2) -> active# X1, active# length X -> length# active X)
(active# cons(X1, X2) -> active# X1, active# length X -> active# X)
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# s X -> s# active X)
(active# take(X1, X2) -> active# X1, active# s X -> active# X)
(active# take(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# take(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# take(X1, X2) -> active# X1, active# length X -> length# active X)
(active# take(X1, X2) -> active# X1, active# length X -> active# X)
(active# take(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# take(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# and(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# and(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# and(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(active# take(X1, X2) -> active# X2, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> active# X2, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> take#(active X1, X2))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> take#(X1, active X2))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> active# X2)
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# s X -> s# active X)
(active# take(X1, X2) -> active# X2, active# s X -> active# X)
(active# take(X1, X2) -> active# X2, active# length cons(N, L) -> s# length L)
(active# take(X1, X2) -> active# X2, active# length cons(N, L) -> length# L)
(active# take(X1, X2) -> active# X2, active# length X -> length# active X)
(active# take(X1, X2) -> active# X2, active# length X -> active# X)
(active# take(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
(active# take(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# zeros() -> cons#(0(), zeros()))
(active# take(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
(proper# and(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# and(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# and(X1, X2) -> proper# X2, proper# length X -> proper# X)
(proper# and(X1, X2) -> proper# X2, proper# length X -> length# proper X)
(proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X2, proper# length X -> length# proper X)
(proper# take(X1, X2) -> proper# X2, proper# length X -> proper# X)
(proper# take(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# take(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# cons(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X2, proper# length X -> length# proper X)
(proper# cons(X1, X2) -> proper# X2, proper# length X -> proper# X)
(proper# cons(X1, X2) -> proper# X2, proper# s X -> s# proper X)
(proper# cons(X1, X2) -> proper# X2, proper# s X -> proper# X)
(proper# cons(X1, X2) -> proper# X2, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X2, proper# take(X1, X2) -> proper# X2)
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(X1, mark X2) -> take#(X1, X2))
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(mark X1, X2) -> take#(X1, X2))
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# take(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# take(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# take(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# length X -> active# X)
(active# and(X1, X2) -> active# X1, active# length X -> length# active X)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# and(X1, X2) -> active# X1, active# s X -> active# X)
(active# and(X1, X2) -> active# X1, active# s X -> s# active X)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# and(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> take#(active X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(active X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(active X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(top# mark X -> top# proper X, top# mark X -> proper# X)
(top# mark X -> top# proper X, top# mark X -> top# proper X)
(top# mark X -> top# proper X, top# ok X -> active# X)
(top# mark X -> top# proper X, top# ok X -> top# active X)
(proper# length X -> length# proper X, length# mark X -> length# X)
(proper# length X -> length# proper X, length# ok X -> length# X)
(active# length X -> length# active X, length# mark X -> length# X)
(active# length X -> length# active X, length# ok X -> length# X)
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(X1, mark X2) -> take#(X1, X2))
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(mark X1, X2) -> take#(X1, X2))
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(ok X1, ok X2) -> take#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(mark X1, X2) -> cons#(X1, X2))
(active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(ok X1, ok X2) -> cons#(X1, X2))
(top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# length X -> length# proper X)
(top# mark X -> proper# X, proper# length X -> proper# X)
(top# mark X -> proper# X, proper# s X -> s# proper X)
(top# mark X -> proper# X, proper# s X -> proper# X)
(top# mark X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(top# mark X -> proper# X, proper# take(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# take(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# length X -> proper# X, proper# and(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# and(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# length X -> length# proper X)
(proper# length X -> proper# X, proper# length X -> proper# X)
(proper# length X -> proper# X, proper# s X -> s# proper X)
(proper# length X -> proper# X, proper# s X -> proper# X)
(proper# length X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# length X -> proper# X, proper# take(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# take(X1, X2) -> proper# X2)
(s# mark X -> s# X, s# mark X -> s# X)
(s# mark X -> s# X, s# ok X -> s# X)
(length# mark X -> length# X, length# mark X -> length# X)
(length# mark X -> length# X, length# ok X -> length# 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# zeros() -> cons#(0(), zeros()))
(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)
(active# length X -> active# X, active# take(X1, X2) -> active# X1)
(active# length X -> active# X, active# take(X1, X2) -> active# X2)
(active# length X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(active# length X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(active# length X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# length X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
}
EDG:
{
(active# s X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# s X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# s X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(active# s X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(active# s X -> active# X, active# take(X1, X2) -> active# X2)
(active# s X -> active# X, active# take(X1, X2) -> active# X1)
(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# zeros() -> cons#(0(), zeros()))
(active# s X -> active# X, active# cons(X1, X2) -> active# X1)
(active# s X -> active# X, active# cons(X1, X2) -> cons#(active X1, X2))
(length# ok X -> length# X, length# ok X -> length# X)
(length# ok X -> length# X, length# mark X -> length# X)
(s# ok X -> s# X, s# ok X -> s# X)
(s# ok X -> s# X, s# mark X -> s# X)
(proper# s X -> proper# X, proper# take(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# take(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# s X -> proper# X, proper# s X -> proper# X)
(proper# s X -> proper# X, proper# s X -> s# proper X)
(proper# s X -> proper# X, proper# length X -> proper# X)
(proper# s X -> proper# X, proper# length X -> length# proper X)
(proper# s X -> proper# X, proper# and(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# and(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# s X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# s X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(top# ok X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
(top# ok X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(top# ok X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(top# ok X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(top# ok X -> active# X, active# take(X1, X2) -> active# X2)
(top# ok X -> active# X, active# take(X1, X2) -> active# X1)
(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# zeros() -> cons#(0(), zeros()))
(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# length cons(N, L) -> length# L, length# ok X -> length# X)
(active# length cons(N, L) -> length# L, length# mark X -> length# X)
(active# take(X1, X2) -> take#(X1, active X2), take#(ok X1, ok X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(X1, active X2), take#(mark X1, X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(X1, active X2), take#(X1, mark X2) -> take#(X1, X2))
(proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
(proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
(active# length cons(N, L) -> s# length L, s# ok X -> s# X)
(active# length cons(N, L) -> s# length L, s# mark X -> s# X)
(active# s X -> s# active X, s# ok X -> s# X)
(active# s X -> s# active X, s# mark X -> s# X)
(proper# s X -> s# proper X, s# ok X -> s# X)
(proper# s X -> s# proper X, s# mark X -> s# X)
(top# ok X -> top# active X, top# ok X -> top# active X)
(top# ok X -> top# active X, top# ok X -> active# X)
(top# ok X -> top# active X, top# mark X -> top# proper X)
(top# ok X -> top# active X, top# mark X -> proper# X)
(active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(active# cons(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# cons(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# cons(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# s X -> s# active X)
(active# cons(X1, X2) -> active# X1, active# s X -> active# X)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# cons(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# cons(X1, X2) -> active# X1, active# length X -> length# active X)
(active# cons(X1, X2) -> active# X1, active# length X -> active# X)
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# cons(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# cons(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# take(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# s X -> s# active X)
(active# take(X1, X2) -> active# X1, active# s X -> active# X)
(active# take(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# take(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# take(X1, X2) -> active# X1, active# length X -> length# active X)
(active# take(X1, X2) -> active# X1, active# length X -> active# X)
(active# take(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# take(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# take(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# and(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# and(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# and(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# and(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(X1, mark X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(ok X1, ok X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(active# take(X1, X2) -> active# X2, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> active# X2, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> take#(active X1, X2))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> take#(X1, active X2))
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> active# X2)
(active# take(X1, X2) -> active# X2, active# take(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# s X -> s# active X)
(active# take(X1, X2) -> active# X2, active# s X -> active# X)
(active# take(X1, X2) -> active# X2, active# length cons(N, L) -> s# length L)
(active# take(X1, X2) -> active# X2, active# length cons(N, L) -> length# L)
(active# take(X1, X2) -> active# X2, active# length X -> length# active X)
(active# take(X1, X2) -> active# X2, active# length X -> active# X)
(active# take(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
(active# take(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# zeros() -> cons#(0(), zeros()))
(active# take(X1, X2) -> active# X2, active# cons(X1, X2) -> active# X1)
(active# take(X1, X2) -> active# X2, active# cons(X1, X2) -> cons#(active X1, X2))
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(X1, mark X2) -> take#(X1, X2))
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(mark X1, X2) -> take#(X1, X2))
(active# take(s M, cons(N, IL)) -> take#(M, IL), take#(ok X1, ok X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(take#(mark X1, X2) -> take#(X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
(and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(cons#(ok X1, ok X2) -> cons#(X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# take(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# take(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# take(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# take(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# take(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# cons(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
(proper# cons(X1, X2) -> proper# X1, proper# length X -> length# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# length X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> s# proper X)
(proper# cons(X1, X2) -> proper# X1, proper# s X -> proper# X)
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X1)
(proper# cons(X1, X2) -> proper# X1, proper# take(X1, X2) -> proper# X2)
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> cons#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# cons(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# zeros() -> cons#(0(), zeros()))
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# length X -> active# X)
(active# and(X1, X2) -> active# X1, active# length X -> length# active X)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> length# L)
(active# and(X1, X2) -> active# X1, active# length cons(N, L) -> s# length L)
(active# and(X1, X2) -> active# X1, active# s X -> active# X)
(active# and(X1, X2) -> active# X1, active# s X -> s# active X)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> active# X1)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> active# X2)
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> take#(X1, active X2))
(active# and(X1, X2) -> active# X1, active# take(X1, X2) -> take#(active X1, X2))
(active# and(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# and(X1, X2) -> active# X1, active# take(s M, cons(N, IL)) -> take#(M, IL))
(active# take(X1, X2) -> take#(active X1, X2), take#(X1, mark X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(active X1, X2), take#(mark X1, X2) -> take#(X1, X2))
(active# take(X1, X2) -> take#(active X1, X2), take#(ok X1, ok X2) -> take#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(mark X1, X2) -> cons#(X1, X2))
(active# cons(X1, X2) -> cons#(active X1, X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(top# mark X -> top# proper X, top# mark X -> proper# X)
(top# mark X -> top# proper X, top# mark X -> top# proper X)
(top# mark X -> top# proper X, top# ok X -> active# X)
(top# mark X -> top# proper X, top# ok X -> top# active X)
(proper# length X -> length# proper X, length# mark X -> length# X)
(proper# length X -> length# proper X, length# ok X -> length# X)
(active# length X -> length# active X, length# mark X -> length# X)
(active# length X -> length# active X, length# ok X -> length# X)
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(X1, mark X2) -> take#(X1, X2))
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(mark X1, X2) -> take#(X1, X2))
(proper# take(X1, X2) -> take#(proper X1, proper X2), take#(ok X1, ok X2) -> take#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(mark X1, X2) -> cons#(X1, X2))
(proper# cons(X1, X2) -> cons#(proper X1, proper X2), cons#(ok X1, ok X2) -> cons#(X1, X2))
(active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(mark X1, X2) -> cons#(X1, X2))
(active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)), cons#(ok X1, ok X2) -> cons#(X1, X2))
(top# mark X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
(top# mark X -> proper# X, proper# length X -> length# proper X)
(top# mark X -> proper# X, proper# length X -> proper# X)
(top# mark X -> proper# X, proper# s X -> s# proper X)
(top# mark X -> proper# X, proper# s X -> proper# X)
(top# mark X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(top# mark X -> proper# X, proper# take(X1, X2) -> proper# X1)
(top# mark X -> proper# X, proper# take(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# cons(X1, X2) -> cons#(proper X1, proper X2))
(proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# cons(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
(proper# length X -> proper# X, proper# and(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# and(X1, X2) -> proper# X2)
(proper# length X -> proper# X, proper# length X -> length# proper X)
(proper# length X -> proper# X, proper# length X -> proper# X)
(proper# length X -> proper# X, proper# s X -> s# proper X)
(proper# length X -> proper# X, proper# s X -> proper# X)
(proper# length X -> proper# X, proper# take(X1, X2) -> take#(proper X1, proper X2))
(proper# length X -> proper# X, proper# take(X1, X2) -> proper# X1)
(proper# length X -> proper# X, proper# take(X1, X2) -> proper# X2)
(s# mark X -> s# X, s# mark X -> s# X)
(s# mark X -> s# X, s# ok X -> s# X)
(length# mark X -> length# X, length# mark X -> length# X)
(length# mark X -> length# X, length# ok X -> length# 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# zeros() -> cons#(0(), zeros()))
(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)
(active# length X -> active# X, active# take(X1, X2) -> active# X1)
(active# length X -> active# X, active# take(X1, X2) -> active# X2)
(active# length X -> active# X, active# take(X1, X2) -> take#(X1, active X2))
(active# length X -> active# X, active# take(X1, X2) -> take#(active X1, X2))
(active# length X -> active# X, active# take(s M, cons(N, IL)) -> cons#(N, take(M, IL)))
(active# length X -> active# X, active# take(s M, cons(N, IL)) -> take#(M, IL))
}
STATUS:
arrows: 0.869630
SCCS (8):
Scc:
{top# mark X -> top# proper X,
top# ok X -> top# active X}
Scc:
{proper# cons(X1, X2) -> proper# X1,
proper# and(X1, X2) -> proper# X1,
proper# length X -> proper# X,
proper# s X -> proper# X,
proper# take(X1, X2) -> proper# X1}
Scc:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1,
active# length X -> active# X,
active# s X -> active# X,
active# take(X1, X2) -> active# X1,
active# take(X1, X2) -> active# X2}
Scc:
{ take#(X1, mark X2) -> take#(X1, X2),
take#(mark X1, X2) -> take#(X1, X2),
take#(ok X1, ok X2) -> take#(X1, X2)}
Scc:
{s# mark X -> s# X,
s# ok X -> s# X}
Scc:
{length# mark X -> length# X,
length# ok X -> length# X}
Scc:
{ and#(mark X1, X2) -> and#(X1, X2),
and#(ok X1, ok X2) -> and#(X1, X2)}
Scc:
{ cons#(mark X1, X2) -> cons#(X1, X2),
cons#(ok X1, ok X2) -> cons#(X1, X2)}
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open
SCC (5):
Strict:
{proper# cons(X1, X2) -> proper# X1,
proper# and(X1, X2) -> proper# X1,
proper# length X -> proper# X,
proper# s X -> proper# X,
proper# take(X1, X2) -> proper# 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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open
SCC (6):
Strict:
{active# cons(X1, X2) -> active# X1,
active# and(X1, X2) -> active# X1,
active# length X -> active# X,
active# s X -> active# X,
active# take(X1, X2) -> active# X1,
active# take(X1, X2) -> active# X2}
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open
SCC (3):
Strict:
{ take#(X1, mark X2) -> take#(X1, X2),
take#(mark X1, X2) -> take#(X1, X2),
take#(ok X1, ok X2) -> take#(X1, X2)}
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open
SCC (2):
Strict:
{s# mark X -> s# X,
s# ok X -> s# 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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open
SCC (2):
Strict:
{length# mark X -> length# X,
length# ok X -> length# 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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open
SCC (2):
Strict:
{ and#(mark X1, X2) -> and#(X1, X2),
and#(ok X1, ok X2) -> and#(X1, X2)}
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open
SCC (2):
Strict:
{ cons#(mark X1, X2) -> cons#(X1, X2),
cons#(ok X1, ok X2) -> cons#(X1, X2)}
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,
active take(X1, X2) -> take(X1, active X2),
active take(X1, X2) -> take(active X1, X2),
active take(0(), IL) -> mark nil(),
active take(s M, cons(N, IL)) -> mark cons(N, take(M, IL)),
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,
take(X1, mark X2) -> mark take(X1, X2),
take(mark X1, X2) -> mark take(X1, X2),
take(ok X1, ok X2) -> ok take(X1, X2),
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,
proper take(X1, X2) -> take(proper X1, proper X2),
top mark X -> top proper X,
top ok X -> top active X}
Open