(VAR x xs y ys)
(RULES
    <(x,y) -> #cklt(#compare(x,y))

    merge(nil,ys)            -> ys
    merge(::(x,xs),nil)      -> ::(x,xs)
    merge(::(x,xs),::(y,ys)) -> ifmerge(<(x,y),x,xs,y,ys)
    ifmerge(true,x,xs,y,ys)  -> ::(x,merge(xs,::(y,ys)))
    ifmerge(false,x,xs,y,ys) -> ::(y,merge(::(x,xs),ys))

    msplit(nil)             -> pair(nil,nil)
    msplit(::(x,nil))       -> pair(::(x,nil),nil)
    msplit(::(x,::(y,ys)))  -> msplit'(x,y,msplit(ys))
    msplit'(x,y,pair(xs,ys)) -> pair(::(x,xs),::(y,ys))

    mergesort(nil)            -> nil
    mergesort(::(x,nil))      -> ::(x,nil)
    mergesort(::(x,::(y,ys))) -> mergesort'(msplit(::(x,::(y,ys))))
    mergesort'(pair(xs,ys))   -> merge(mergesort(xs),mergesort(ys))
    
    #cklt(#EQ()) ->= #false
    #cklt(#GT()) ->= #false
    #cklt(#LT()) ->= true
    #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)
)