MAYBE 0.08/0.19 MAYBE 0.08/0.19 0.08/0.19 Problem: 0.08/0.19 qsort(nil()) -> nil() 0.08/0.19 qsort(cons(x,xs)) -> 0.08/0.19 append(qsort(filterlow(x,cons(x,xs))),cons(x,qsort(filterhigh(x,cons(x,xs))))) 0.08/0.19 filterlow(n,nil()) -> nil() 0.08/0.19 filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs) 0.08/0.19 if1(true(),n,x,xs) -> filterlow(n,xs) 0.08/0.19 if1(false(),n,x,xs) -> cons(x,filterlow(n,xs)) 0.08/0.19 filterhigh(n,nil()) -> nil() 0.08/0.19 filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs) 0.08/0.19 if2(true(),n,x,xs) -> filterhigh(n,xs) 0.08/0.19 if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs)) 0.08/0.19 ge(x,0()) -> true() 0.08/0.19 ge(0(),s(x)) -> false() 0.08/0.19 ge(s(x),s(y)) -> ge(x,y) 0.08/0.19 append(nil(),ys()) -> ys() 0.08/0.19 append(cons(x,xs),ys()) -> cons(x,append(xs,ys())) 0.08/0.19 0.08/0.19 Proof: 0.08/0.19 Open 0.08/0.19 EOF