(STRATEGY
    INNERMOST)

(VAR
    x1 x10 x16 x2 x3 x4 x5 x6 x8 x9)
(DATATYPES
    A = µX.< Cons(X, X), rev_l, step_x_f(X, X, X), fleft_op_e_xs_1, Nil >)
(SIGNATURES
    rev_l#2 :: [A x A] -> A
    step_x_f#1 :: [A x A x A x A] -> A
    foldr#3 :: [A] -> A
    main :: [A] -> A)
(RULES
    rev_l#2(x8,x10) -> Cons(x10,x8)
    step_x_f#1(rev_l()
              ,x5
              ,step_x_f(x2,x3,x4)
              ,x1) -> step_x_f#1(x2
                                ,x3
                                ,x4
                                ,rev_l#2(x1,x5))
    step_x_f#1(rev_l()
              ,x5
              ,fleft_op_e_xs_1()
              ,x3) -> rev_l#2(x3,x5)
    foldr#3(Nil()) ->
      fleft_op_e_xs_1()
    foldr#3(Cons(x16,x6)) ->
      step_x_f(rev_l()
              ,x16
              ,foldr#3(x6))
    main(Nil()) -> Nil()
    main(Cons(x8,x9)) ->
      step_x_f#1(rev_l()
                ,x8
                ,foldr#3(x9)
                ,Nil()))