(STRATEGY
    INNERMOST)

(VAR
    x1 x11 x12 x16 x2 x20 x23 x4 x40
    x6 x8)
(DATATYPES
    A = µX.< Cons(X, X), 0, S(X), M(X), Nil >)
(SIGNATURES
    cond_scanr_f_z_xs_1 :: [A x A] -> A
    scanr#3 :: [A] -> A
    foldl#3 :: [A x A] -> A
    minus#2 :: [A x A] -> A
    plus#2 :: [A x A] -> A
    max#2 :: [A x A] -> A
    main :: [A] -> A)
(RULES
    cond_scanr_f_z_xs_1(Cons(0()
                            ,x11)
                       ,0()) -> Cons(0(),Cons(0(),x11))
    cond_scanr_f_z_xs_1(Cons(S(x2)
                            ,x11)
                       ,0()) -> Cons(S(x2)
                                    ,Cons(S(x2),x11))
    cond_scanr_f_z_xs_1(Cons(0()
                            ,x11)
                       ,M(x2)) -> Cons(0()
                                      ,Cons(0(),x11))
    cond_scanr_f_z_xs_1(Cons(S(x40)
                            ,x23)
                       ,M(0())) -> Cons(S(x40)
                                       ,Cons(S(x40),x23))
    cond_scanr_f_z_xs_1(Cons(S(x8)
                            ,x23)
                       ,M(S(x4))) -> Cons(minus#2(x8
                                                 ,x4)
                                         ,Cons(S(x8),x23))
    cond_scanr_f_z_xs_1(Cons(0()
                            ,x11)
                       ,S(x2)) -> Cons(S(x2)
                                      ,Cons(0(),x11))
    cond_scanr_f_z_xs_1(Cons(S(x2)
                            ,x11)
                       ,S(x4)) -> Cons(plus#2(S(x4)
                                             ,S(x2))
                                      ,Cons(S(x2),x11))
    scanr#3(Nil()) -> Cons(0()
                          ,Nil())
    scanr#3(Cons(x4,x2)) ->
      cond_scanr_f_z_xs_1(scanr#3(x2)
                         ,x4)
    foldl#3(x2,Nil()) -> x2
    foldl#3(x6,Cons(x4,x2)) ->
      foldl#3(max#2(x6,x4),x2)
    minus#2(0(),x16) -> 0()
    minus#2(S(x20),0()) -> S(x20)
    minus#2(S(x4),S(x2)) ->
      minus#2(x4,x2)
    plus#2(0(),S(x2)) -> S(x2)
    plus#2(S(x4),S(x2)) ->
      S(plus#2(x4,S(x2)))
    max#2(0(),x8) -> x8
    max#2(S(x12),0()) -> S(x12)
    max#2(S(x4),S(x2)) -> S(max#2(x4
                                 ,x2))
    main(x1) -> foldl#3(0()
                       ,scanr#3(x1)))