(VAR x y z ) (RULES le(s(x), 0) -> false le(0, y) -> true le(s(x), s(y)) -> le(x, y) double(0) -> 0 double(s(x)) -> s(s(double(x))) log(0) -> logError log(s(x)) -> loop(s(x), s(0), 0) loop(x, s(y), z) -> if(le(x, s(y)), x, s(y), z) if(true, x, y, z) -> z if(false, x, y, z) -> loop(x, double(y), s(z)) )