MAYBE 0.07/0.19 MAYBE 0.07/0.19 0.07/0.19 Problem: 0.07/0.19 isEmpty(empty()) -> true() 0.07/0.19 isEmpty(node(l,x,r)) -> false() 0.07/0.19 left(empty()) -> empty() 0.07/0.19 left(node(l,x,r)) -> l 0.07/0.19 right(empty()) -> empty() 0.07/0.19 right(node(l,x,r)) -> r 0.07/0.19 elem(node(l,x,r)) -> x 0.07/0.19 append(nil(),x) -> cons(x,nil()) 0.07/0.19 append(cons(y(),ys),x) -> cons(y(),append(ys,x)) 0.07/0.19 listify(n,xs) -> 0.07/0.19 if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)), 0.07/0.19 node(right(left(n)),elem(n),right(n))), 0.07/0.19 xs,append(xs,n)) 0.07/0.19 if(true(),b,n,m,xs,ys) -> xs 0.07/0.19 if(false(),false(),n,m,xs,ys) -> listify(m,xs) 0.07/0.19 if(false(),true(),n,m,xs,ys) -> listify(n,ys) 0.07/0.19 toList(n) -> listify(n,nil()) 0.07/0.19 0.07/0.19 Proof: 0.07/0.19 Open 0.07/0.19 EOF