(STRATEGY
    INNERMOST)

(VAR
    x1 x12 x2 x3 x4 x6 x8)
(DATATYPES
    A = µX.< Nil, Cons(X, X), True, False, 0, S(X) >)
(SIGNATURES
    sort#2 :: [A] -> A
    cond_insert_ord_x_ys_1 :: [A x A x A x A] -> A
    insert#3 :: [A x A] -> A
    leq#2 :: [A x A] -> A
    main :: [A] -> A)
(RULES
    sort#2(Nil()) -> Nil()
    sort#2(Cons(x4,x2)) ->
      insert#3(x4,sort#2(x2))
    cond_insert_ord_x_ys_1(True()
                          ,x3
                          ,x2
                          ,x1) -> Cons(x3,Cons(x2,x1))
    cond_insert_ord_x_ys_1(False()
                          ,x3
                          ,x2
                          ,x1) -> Cons(x2,insert#3(x3,x1))
    insert#3(x2,Nil()) -> Cons(x2
                              ,Nil())
    insert#3(x6,Cons(x4,x2)) ->
      cond_insert_ord_x_ys_1(leq#2(x6
                                  ,x4)
                            ,x6
                            ,x4
                            ,x2)
    leq#2(0(),x8) -> True()
    leq#2(S(x12),0()) -> False()
    leq#2(S(x4),S(x2)) -> leq#2(x4
                               ,x2)
    main(x1) -> sort#2(x1))