(VAR
    ls pivot rs x xs y ys z zs)
(RULES
    greater(x,y) -> ckgt(compare(x,y))
    if(true, x, y) -> x
    if(false, x, y) -> y

    quicksort(nil) -> nil
    quicksort(::(z,zs)) -> quicksort'(z,split(z,zs))
    quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),::(z,quicksort(ys)))
    
    split(pivot,nil) -> pair(nil,nil)
    split(pivot,nil)              -> pair(nil,nil)
    split(pivot,::(x,xs))         -> split'(>(x,pivot),x,split(pivot,xs))
    split'(true, x, pair(ls,rs))  -> pair(ls,::(x,rs))
    split'(false, x, pair(ls,rs)) -> pair(::(x,ls),rs)

    append(nil,ys) -> ys
    append(::(x,xs),ys) -> ::(x,append(xs,ys))

    ckgt(EQ) ->= false
    ckgt(GT) ->= true
    ckgt(LT) ->= false
    compare(0,0) ->= EQ
    compare(0,neg(y)) ->= GT
    compare(0,pos(y)) ->= LT
    compare(0,s(y)) ->= LT
    compare(neg(x),0) ->= LT
    compare(neg(x),neg(y)) ->= compare(y,x)
    compare(neg(x),pos(y)) ->= LT
    compare(pos(x),0) ->= GT
    compare(pos(x),neg(y)) ->= GT
    compare(pos(x),pos(y)) ->= compare(x,y)
    compare(s(x),0) ->= GT
    compare(s(x),s(y)) ->= compare(x,y))
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'quicksort.raml', c.f. http://raml.tcs.ifi.lmu.de/)