MAYBE 238.43/60.34 MAYBE 238.43/60.34 238.43/60.34 Problem: 238.43/60.34 active(zeros()) -> mark(cons(0(),zeros())) 238.43/60.34 active(U11(tt(),L)) -> mark(U12(tt(),L)) 238.43/60.34 active(U12(tt(),L)) -> mark(s(length(L))) 238.43/60.34 active(length(nil())) -> mark(0()) 238.43/60.34 active(length(cons(N,L))) -> mark(U11(tt(),L)) 238.43/60.34 mark(zeros()) -> active(zeros()) 238.43/60.34 mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) 238.43/60.34 mark(0()) -> active(0()) 238.43/60.34 mark(U11(X1,X2)) -> active(U11(mark(X1),X2)) 238.43/60.34 mark(tt()) -> active(tt()) 238.43/60.34 mark(U12(X1,X2)) -> active(U12(mark(X1),X2)) 238.43/60.34 mark(s(X)) -> active(s(mark(X))) 238.43/60.34 mark(length(X)) -> active(length(mark(X))) 238.43/60.34 mark(nil()) -> active(nil()) 238.43/60.34 cons(mark(X1),X2) -> cons(X1,X2) 238.43/60.34 cons(X1,mark(X2)) -> cons(X1,X2) 238.43/60.34 cons(active(X1),X2) -> cons(X1,X2) 238.43/60.34 cons(X1,active(X2)) -> cons(X1,X2) 238.43/60.34 U11(mark(X1),X2) -> U11(X1,X2) 238.43/60.34 U11(X1,mark(X2)) -> U11(X1,X2) 238.43/60.34 U11(active(X1),X2) -> U11(X1,X2) 238.43/60.34 U11(X1,active(X2)) -> U11(X1,X2) 238.43/60.34 U12(mark(X1),X2) -> U12(X1,X2) 238.43/60.34 U12(X1,mark(X2)) -> U12(X1,X2) 238.43/60.34 U12(active(X1),X2) -> U12(X1,X2) 238.43/60.34 U12(X1,active(X2)) -> U12(X1,X2) 238.43/60.34 s(mark(X)) -> s(X) 238.43/60.34 s(active(X)) -> s(X) 238.43/60.34 length(mark(X)) -> length(X) 238.43/60.34 length(active(X)) -> length(X) 238.43/60.34 238.43/60.34 Proof: 238.43/60.34 Open 238.43/60.34 EOF