(GOAL COMPLEXITY)
(STARTTERM CONSTRUCTOR-BASED)
(STRATEGY INNERMOST)
(STRATEGY
    INNERMOST)

(VAR
    x y z)
(DATATYPES
    A = µX.< nil, .(X, X), if(X, X, X), <=(X, X), =(X, X) >)
(SIGNATURES
    msort :: [A] -> A
    min :: [A x A] -> A
    del :: [A x A] -> A)
(RULES
    msort(nil()) -> nil()
    msort(.(x,y)) -> .(min(x,y)
                      ,msort(del(min(x,y),.(x,y))))
    min(x,nil()) -> x
    min(x,.(y,z)) -> if(<=(x,y)
                       ,min(x,z)
                       ,min(y,z))
    del(x,nil()) -> nil()
    del(x,.(y,z)) -> if(=(x,y)
                       ,z
                       ,.(y,del(x,z))))