MAYBE 265.88/67.41 MAYBE 265.88/67.41 265.88/67.41 Problem: 265.88/67.41 a__incr(nil()) -> nil() 265.88/67.41 a__incr(cons(X,L)) -> cons(s(mark(X)),incr(L)) 265.88/67.41 a__adx(nil()) -> nil() 265.88/67.41 a__adx(cons(X,L)) -> a__incr(cons(mark(X),adx(L))) 265.88/67.41 a__nats() -> a__adx(a__zeros()) 265.88/67.41 a__zeros() -> cons(0(),zeros()) 265.88/67.41 a__head(cons(X,L)) -> mark(X) 265.88/67.41 a__tail(cons(X,L)) -> mark(L) 265.88/67.41 mark(incr(X)) -> a__incr(mark(X)) 265.88/67.41 mark(adx(X)) -> a__adx(mark(X)) 265.88/67.41 mark(nats()) -> a__nats() 265.88/67.41 mark(zeros()) -> a__zeros() 265.88/67.41 mark(head(X)) -> a__head(mark(X)) 265.88/67.41 mark(tail(X)) -> a__tail(mark(X)) 265.88/67.41 mark(nil()) -> nil() 265.88/67.41 mark(cons(X1,X2)) -> cons(mark(X1),X2) 265.88/67.41 mark(s(X)) -> s(mark(X)) 265.88/67.41 mark(0()) -> 0() 265.88/67.41 a__incr(X) -> incr(X) 265.88/67.41 a__adx(X) -> adx(X) 265.88/67.41 a__nats() -> nats() 265.88/67.41 a__zeros() -> zeros() 265.88/67.41 a__head(X) -> head(X) 265.88/67.41 a__tail(X) -> tail(X) 265.88/67.41 265.88/67.41 Proof: 265.88/67.41 Open 265.88/67.42 EOF