(STRATEGY
    INNERMOST)

(VAR
    @l @x @xs @y @ys)
(DATATYPES
    A = µX.< ::(X, X), nil, #false, #true, #EQ, #GT, #LT, #0, #neg(X), #pos(X), #s(X) >)
(SIGNATURES
    #less :: [A x A] -> A
    findMin :: [A] -> A
    findMin#1 :: [A] -> A
    findMin#2 :: [A x A] -> A
    findMin#3 :: [A x A x A x A] -> A
    minSort :: [A] -> A
    minSort#1 :: [A] -> A
    #cklt :: [A] -> A
    #compare :: [A x A] -> A)
(RULES
    #less(@x,@y) ->
      #cklt(#compare(@x,@y))
    findMin(@l) -> findMin#1(@l)
    findMin#1(::(@x,@xs)) ->
      findMin#2(findMin(@xs),@x)
    findMin#1(nil()) -> nil()
    findMin#2(::(@y,@ys),@x) ->
      findMin#3(#less(@x,@y)
               ,@x
               ,@y
               ,@ys)
    findMin#2(nil(),@x) -> ::(@x
                             ,nil())
    findMin#3(#false(),@x,@y,@ys) ->
      ::(@y,::(@x,@ys))
    findMin#3(#true(),@x,@y,@ys) ->
      ::(@x,::(@y,@ys))
    minSort(@l) ->
      minSort#1(findMin(@l))
    minSort#1(::(@x,@xs)) -> ::(@x
                               ,minSort(@xs))
    minSort#1(nil()) -> nil()
    #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))