MAYBE 0.07/0.19 MAYBE 0.07/0.19 0.07/0.19 Problem: 0.07/0.19 nthtail(n,l) -> cond(ge(n,length(l)),n,l) 0.07/0.19 cond(true(),n,l) -> l 0.07/0.19 cond(false(),n,l) -> tail(nthtail(s(n),l)) 0.07/0.19 tail(nil()) -> nil() 0.07/0.19 tail(cons(x,l)) -> l 0.07/0.19 length(nil()) -> 0() 0.07/0.19 length(cons(x,l)) -> s(length(l)) 0.07/0.19 ge(u,0()) -> true() 0.07/0.19 ge(0(),s(v)) -> false() 0.07/0.19 ge(s(u),s(v)) -> ge(u,v) 0.07/0.19 0.07/0.19 Proof: 0.07/0.19 Open 0.07/0.19 EOF