(STRATEGY
    INNERMOST)

(VAR
    x0 x1 x12 x2 x3 x4 x5 x6 x8)
(DATATYPES
    A = µX.< insert_ord(X), Nil, Cons(X, X), True, False, leq, 0, S(X) >)
(SIGNATURES
    fold#3 :: [A x A] -> A
    cond_insert_ord_x_ys_1 :: [A x A x A x A] -> A
    insert_ord#2 :: [A x A x A] -> A
    leq#2 :: [A x A] -> A
    main :: [A] -> A)
(RULES
    fold#3(insert_ord(x2),Nil()) ->
      Nil()
    fold#3(insert_ord(x6)
          ,Cons(x4,x2)) -> insert_ord#2(x6
                                       ,x4
                                       ,fold#3(insert_ord(x6),x2))
    cond_insert_ord_x_ys_1(True()
                          ,x3
                          ,x2
                          ,x1) -> Cons(x3,Cons(x2,x1))
    cond_insert_ord_x_ys_1(False()
                          ,x0
                          ,x5
                          ,x2) -> Cons(x5
                                      ,insert_ord#2(leq(),x0,x2))
    insert_ord#2(leq(),x2,Nil()) ->
      Cons(x2,Nil())
    insert_ord#2(leq()
                ,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(x3) ->
      fold#3(insert_ord(leq()),x3))