MAYBE 0.18/0.20 MAYBE 0.18/0.20 0.18/0.20 Problem: 0.18/0.20 qsort(xs) -> qs(half(length(xs)),xs) 0.18/0.20 qs(n,nil()) -> nil() 0.18/0.20 qs(n,cons(x,xs)) -> 0.18/0.20 append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(get(n,cons(x,xs)), 0.18/0.20 qs(half(n), 0.18/0.20 filterhigh 0.18/0.20 ( 0.18/0.20 get(n,cons(x,xs)),cons(x,xs))))) 0.18/0.20 filterlow(n,nil()) -> nil() 0.18/0.20 filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) 0.18/0.20 if1(true(),n,x,xs) -> filterlow(n,xs) 0.18/0.20 if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) 0.18/0.20 filterhigh(n,nil()) -> nil() 0.18/0.20 filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) 0.18/0.20 if2(true(),n,x,xs) -> filterhigh(n,xs) 0.18/0.20 if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) 0.18/0.20 ge(x,0()) -> true() 0.18/0.20 ge(0(),s(x)) -> false() 0.18/0.20 ge(s(x),s(y)) -> ge(x,y) 0.18/0.20 append(nil(),ys()) -> ys() 0.18/0.20 append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) 0.18/0.20 length(nil()) -> 0() 0.18/0.20 length(cons(x,xs)) -> s(length(xs)) 0.18/0.20 half(0()) -> 0() 0.18/0.20 half(s(0())) -> 0() 0.18/0.20 half(s(s(x))) -> s(half(x)) 0.18/0.20 get(n,nil()) -> 0() 0.18/0.20 get(n,cons(x,nil())) -> x 0.18/0.20 get(0(),cons(x,cons(y,xs))) -> x 0.18/0.20 get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs)) 0.18/0.20 0.18/0.20 Proof: 0.18/0.20 Open 0.18/0.20 EOF