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