(STRATEGY
    INNERMOST)

(VAR
    x1 x2 x3 x6 x9)
(DATATYPES
    A = µX.< compS_f(X), S(X), id, 0 >)
(SIGNATURES
    compS_f#1 :: [A x A] -> A
    iter#3 :: [A] -> A
    main :: [A] -> A)
(RULES
    compS_f#1(compS_f(x2),x1) ->
      compS_f#1(x2,S(x1))
    compS_f#1(id(),x3) -> S(x3)
    iter#3(0()) -> id()
    iter#3(S(x6)) ->
      compS_f(iter#3(x6))
    main(0()) -> 0()
    main(S(x9)) ->
      compS_f#1(iter#3(x9),0()))