(STRATEGY
    INNERMOST)

(VAR
    x11 x2 x40 x23 x8 x4 x6 x16 x20 x12 x1)
(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)))