MAYBE 254.28/64.30 MAYBE 254.28/64.31 254.28/64.31 Problem: 254.28/64.31 active(zeros()) -> mark(cons(0(),zeros())) 254.28/64.31 active(and(tt(),X)) -> mark(X) 254.28/64.31 active(length(nil())) -> mark(0()) 254.28/64.31 active(length(cons(N,L))) -> mark(s(length(L))) 254.28/64.31 active(take(0(),IL)) -> mark(nil()) 254.28/64.31 active(take(s(M),cons(N,IL))) -> mark(cons(N,take(M,IL))) 254.28/64.31 mark(zeros()) -> active(zeros()) 254.28/64.31 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 254.28/64.31 mark(0()) -> active(0()) 254.28/64.31 mark(and(X1,X2)) -> active(and(mark(X1),X2)) 254.28/64.31 mark(tt()) -> active(tt()) 254.28/64.31 mark(length(X)) -> active(length(mark(X))) 254.28/64.31 mark(nil()) -> active(nil()) 254.28/64.31 mark(s(X)) -> active(s(mark(X))) 254.28/64.31 mark(take(X1,X2)) -> active(take(mark(X1),mark(X2))) 254.28/64.31 cons(mark(X1),X2) -> cons(X1,X2) 254.28/64.31 cons(X1,mark(X2)) -> cons(X1,X2) 254.28/64.31 cons(active(X1),X2) -> cons(X1,X2) 254.28/64.31 cons(X1,active(X2)) -> cons(X1,X2) 254.28/64.31 and(mark(X1),X2) -> and(X1,X2) 254.28/64.31 and(X1,mark(X2)) -> and(X1,X2) 254.28/64.31 and(active(X1),X2) -> and(X1,X2) 254.28/64.31 and(X1,active(X2)) -> and(X1,X2) 254.28/64.31 length(mark(X)) -> length(X) 254.28/64.31 length(active(X)) -> length(X) 254.28/64.31 s(mark(X)) -> s(X) 254.28/64.31 s(active(X)) -> s(X) 254.28/64.31 take(mark(X1),X2) -> take(X1,X2) 254.28/64.31 take(X1,mark(X2)) -> take(X1,X2) 254.28/64.31 take(active(X1),X2) -> take(X1,X2) 254.28/64.31 take(X1,active(X2)) -> take(X1,X2) 254.28/64.31 254.28/64.31 Proof: 254.28/64.31 Open 254.28/64.31 EOF