(STRATEGY
    INNERMOST)

(VAR
    x12 x14 x2 x4 x5 x6 x8)
(DATATYPES
    A = µX.< 0, S(X), plus_x(X), Nil, Cons(X, X) >)
(SIGNATURES
    plus_x#1 :: [A x A] -> A
    map#2 :: [A x A] -> A
    main :: [A x A] -> A)
(RULES
    plus_x#1(0(),x8) -> x8
    plus_x#1(S(x12),x14) ->
      S(plus_x#1(x12,x14))
    map#2(plus_x(x2),Nil()) -> Nil()
    map#2(plus_x(x6),Cons(x4,x2)) ->
      Cons(plus_x#1(x6,x4)
          ,map#2(plus_x(x6),x2))
    main(x5,x12) ->
      map#2(plus_x(x12),x5))