in nat-list.maude

fmod NAT-ORD-LIST is
   protecting NAT-LIST .

   sorts OrdList NeOrdList .
   subsort NeOrdList < OrdList NeList < List .

   op insertion-sort : List -> OrdList .
   op insert-list : OrdList Nat -> OrdList .

   op mergesort : List -> OrdList .
   op merge : OrdList OrdList -> OrdList .

   op quicksort : List -> OrdList .
   op leq-elems : List Nat -> List .
   op gr-elems : List Nat -> List .

   vars N M : Nat .
   vars L L' : List .
   vars OL OL' : OrdList .
   var NEOL : NeOrdList .

   mb [] : OrdList .
   mb N : [] : NeOrdList .
   cmb N : NEOL : NeOrdList if N <= head(NEOL) .

   eq insertion-sort([]) = [] .
   eq insertion-sort(N : L) = insert-list(insertion-sort(L), N) .

   eq insert-list([], M) = M : [] .
   ceq insert-list(N : OL, M) = M : N : OL if M <= N .
   ceq insert-list(N : OL, M) = N : insert-list(OL, M) if M > N .

   eq mergesort([]) = [] .
   eq mergesort(N : []) = N : [] .
   ceq mergesort(L) = merge(mergesort(take (length(L) div s(s(0))) from L),
                            mergesort(throw (length(L) div s(s(0))) from L))
       if length(L) > s(0) .

   eq merge(OL, []) = OL .
   eq merge([], OL) = OL .
   ceq merge(N : OL, M : OL') = N : merge(OL, M : OL') if N <= M .
   ceq merge(N : OL, M : OL') = M : merge(N : OL, OL') if N > M .

   eq quicksort([]) = [] .
   eq quicksort(N : L) 
     = quicksort(leq-elems(L,N)) ++ (N : quicksort(gr-elems(L,N))) .

   eq leq-elems([], M) = [] .
   ceq leq-elems(N : L, M) = N : leq-elems(L, M) if N <= M .
   ceq leq-elems(N : L, M) = leq-elems(L, M) if N > M .
   eq gr-elems([], M) = [] .
   ceq gr-elems(N : L, M) = gr-elems(L, M) if N <= M .
   ceq gr-elems(N : L, M) = N : gr-elems(L, M) if N > M .
endfm

red insertion-sort(s(s(s(s(0)))) : s(s(s(0))) : s(s(0)) : s(0) : 0 : []) .
***(
reduce in NAT-ORD-LIST : insertion-sort(s(s(s(s(
    0)))) : s(s(s(0))) : s(s(0)) : s(0) : 0 : []) .
rewrites: 123 in -10ms cpu (0ms real) (~ rewrites/second)
result NeOrdList: 0 : s(0) : s(s(0)) : s(s(s(0))) : s(s(s(s(0))))
    : []
)

red mergesort(s(s(s(s(0)))) : s(s(s(0))) : s(s(0)) : s(0) : 0 : []) .
***(
reduce in NAT-ORD-LIST : mergesort(s(s(s(s(0)))) : s(s(s(
    0))) : s(s(0)) : s(0) : 0 : []) .
rewrites: 317 in -10ms cpu (0ms real) (~ rewrites/second)
result NeOrdList: 0 : s(0) : s(s(0)) : s(s(s(0))) : s(s(s(s(0))))
    : []
)

red quicksort(s(s(s(s(0)))) : s(s(s(0))) : s(s(0)) : s(0) : 0 : []) .
***(
reduce in NAT-ORD-LIST : quicksort(s(s(s(s(0)))) : s(s(s(
    0))) : s(s(0)) : s(0) : 0 : []) .
rewrites: 134 in -10ms cpu (0ms real) (~ rewrites/second)
result NeOrdList: 0 : s(0) : s(s(0)) : s(s(s(0))) : s(s(s(s(0))))
    : []
)