MAYBE 0.09/0.18 MAYBE 0.09/0.18 0.09/0.18 Problem: 0.09/0.18 minus(x,0()) -> x 0.09/0.18 minus(s(x),s(y)) -> minus(x,y) 0.09/0.18 quot(0(),s(y)) -> 0() 0.09/0.18 quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) 0.09/0.18 app(nil(),y) -> y 0.09/0.18 app(add(n,x),y) -> add(n,app(x,y)) 0.09/0.18 reverse(nil()) -> nil() 0.09/0.18 reverse(add(n,x)) -> app(reverse(x),add(n,nil())) 0.09/0.18 shuffle(nil()) -> nil() 0.09/0.18 shuffle(add(n,x)) -> add(n,shuffle(reverse(x))) 0.09/0.18 concat(leaf(),y) -> y 0.09/0.18 concat(cons(u,v),y) -> cons(u,concat(v,y)) 0.09/0.18 less_leaves(x,leaf()) -> false() 0.09/0.18 less_leaves(leaf(),cons(w,z)) -> true() 0.09/0.18 less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) 0.09/0.18 0.09/0.18 Proof: 0.09/0.18 Open 0.09/0.18 EOF