MAYBE 0.18/0.20 MAYBE 0.18/0.20 0.18/0.20 Problem: 0.18/0.20 le(s(x),0()) -> false() 0.18/0.20 le(0(),y) -> true() 0.18/0.20 le(s(x),s(y)) -> le(x,y) 0.18/0.20 double(0()) -> 0() 0.18/0.20 double(s(x)) -> s(s(double(x))) 0.18/0.20 log(0()) -> logError() 0.18/0.20 log(s(x)) -> loop(s(x),s(0()),0()) 0.18/0.20 loop(x,s(y),z) -> if(le(x,s(y)),x,s(y),z) 0.18/0.20 if(true(),x,y,z) -> z 0.18/0.20 if(false(),x,y,z) -> loop(x,double(y),s(z)) 0.18/0.20 maplog(xs) -> mapIter(xs,nil()) 0.18/0.20 mapIter(xs,ys) -> ifmap(isempty(xs),xs,ys) 0.18/0.20 ifmap(true(),xs,ys) -> ys 0.18/0.20 ifmap(false(),xs,ys) -> mapIter(droplast(xs),cons(log(last(xs)),ys)) 0.18/0.20 isempty(nil()) -> true() 0.18/0.20 isempty(cons(x,xs)) -> false() 0.18/0.20 last(nil()) -> error() 0.18/0.20 last(cons(x,nil())) -> x 0.18/0.20 last(cons(x,cons(y,xs))) -> last(cons(y,xs)) 0.18/0.20 droplast(nil()) -> nil() 0.18/0.20 droplast(cons(x,nil())) -> nil() 0.18/0.20 droplast(cons(x,cons(y,xs))) -> cons(x,droplast(cons(y,xs))) 0.18/0.20 a() -> b() 0.18/0.20 a() -> c() 0.18/0.20 0.18/0.20 Proof: 0.18/0.20 Open 0.18/0.20 EOF