(STRATEGY
    INNERMOST)

(VAR
    x1 x10 x16 x2 x24 x3 x32 x5 x6
    x8)
(DATATYPES
    A = µX.< plus_x(X), comp_f_g(X, X), 0, id, Nil, Cons(X, X), S(X) >)
(SIGNATURES
    comp_f_g#1 :: [A x A x A] -> A
    map#2 :: [A] -> A
    plus_x#1 :: [A x A] -> A
    foldr_f#3 :: [A x A] -> A
    foldr#3 :: [A] -> A
    main :: [A] -> A)
(RULES
    comp_f_g#1(plus_x(x3)
              ,comp_f_g(x1,x2)
              ,0()) -> plus_x#1(x3
                               ,comp_f_g#1(x1,x2,0()))
    comp_f_g#1(plus_x(x3)
              ,id()
              ,0()) -> plus_x#1(x3,0())
    map#2(Nil()) -> Nil()
    map#2(Cons(x16,x6)) ->
      Cons(plus_x(x16),map#2(x6))
    plus_x#1(0(),x6) -> x6
    plus_x#1(S(x8),x10) ->
      S(plus_x#1(x8,x10))
    foldr_f#3(Nil(),0()) -> 0()
    foldr_f#3(Cons(x16,x5),x24) ->
      comp_f_g#1(x16,foldr#3(x5),x24)
    foldr#3(Nil()) -> id()
    foldr#3(Cons(x32,x6)) ->
      comp_f_g(x32,foldr#3(x6))
    main(x3) -> foldr_f#3(map#2(x3)
                         ,0()))