(STRATEGY
    INNERMOST)

(VAR
    @_ @l @x @xs @y @ys)
(DATATYPES
    A = µX.< #0, #neg(X), #pos(X), #s(X), ::(X, X), nil, #false, #true, #unit, #EQ, #GT, #LT >)
(SIGNATURES
    #abs :: [A] -> A
    #less :: [A x A] -> A
    insert :: [A x A] -> A
    insert#1 :: [A x A] -> A
    insert#2 :: [A x A x A x A] -> A
    insertD :: [A x A] -> A
    insertD#1 :: [A x A] -> A
    insertD#2 :: [A x A x A x A] -> A
    insertionsort :: [A] -> A
    insertionsort#1 :: [A] -> A
    insertionsortD :: [A] -> A
    insertionsortD#1 :: [A] -> A
    testInsertionsort :: [A] -> A
    testInsertionsortD :: [A] -> A
    testList :: [A] -> A
    #cklt :: [A] -> A
    #compare :: [A x A] -> A)
(RULES
    #abs(#0()) -> #0()
    #abs(#neg(@x)) -> #pos(@x)
    #abs(#pos(@x)) -> #pos(@x)
    #abs(#s(@x)) -> #pos(#s(@x))
    #less(@x,@y) ->
      #cklt(#compare(@x,@y))
    insert(@x,@l) -> insert#1(@l,@x)
    insert#1(::(@y,@ys),@x) ->
      insert#2(#less(@y,@x),@x,@y,@ys)
    insert#1(nil(),@x) -> ::(@x
                            ,nil())
    insert#2(#false(),@x,@y,@ys) ->
      ::(@x,::(@y,@ys))
    insert#2(#true(),@x,@y,@ys) ->
      ::(@y,insert(@x,@ys))
    insertD(@x,@l) -> insertD#1(@l
                               ,@x)
    insertD#1(::(@y,@ys),@x) ->
      insertD#2(#less(@y,@x)
               ,@x
               ,@y
               ,@ys)
    insertD#1(nil(),@x) -> ::(@x
                             ,nil())
    insertD#2(#false(),@x,@y,@ys) ->
      ::(@x,::(@y,@ys))
    insertD#2(#true(),@x,@y,@ys) ->
      ::(@y,insertD(@x,@ys))
    insertionsort(@l) ->
      insertionsort#1(@l)
    insertionsort#1(::(@x,@xs)) ->
      insert(@x,insertionsort(@xs))
    insertionsort#1(nil()) -> nil()
    insertionsortD(@l) ->
      insertionsortD#1(@l)
    insertionsortD#1(::(@x,@xs)) ->
      insertD(@x,insertionsortD(@xs))
    insertionsortD#1(nil()) -> nil()
    testInsertionsort(@x) ->
      insertionsort(testList(#unit()))
    testInsertionsortD(@x) ->
      insertionsortD(testList(#unit()))
    testList(@_) -> ::(#abs(#0())
                      ,::(#abs(#pos(#s(#s(#s(#s(#0()))))))
                         ,::(#abs(#pos(#s(#s(#s(#s(#s(#0())))))))
                            ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0())))))))))))
                               ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0())))))))))
                                  ,::(#abs(#pos(#s(#0())))
                                     ,::(#abs(#pos(#s(#s(#0()))))
                                        ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0()))))))))))
                                           ,::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0()))))))))
                                              ,::(#abs(#pos(#s(#s(#s(#0())))))
                                                 ,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))