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