(STRATEGY
    INNERMOST)

(VAR
    a b c n t x)
(DATATYPES
    A = µX.< A, B, C, 0, s(X), triple(X, X, X) >)
(SIGNATURES
    g :: [A] -> A
    foldB :: [A x A] -> A
    foldC :: [A x A] -> A
    f :: [A x A] -> A
    f' :: [A x A] -> A
    f'' :: [A] -> A)
(RULES
    g(A()) -> A()
    g(B()) -> A()
    g(B()) -> B()
    g(C()) -> A()
    g(C()) -> B()
    g(C()) -> C()
    foldB(t,0()) -> t
    foldB(t,s(n)) -> f(foldB(t,n)
                      ,B())
    foldC(t,0()) -> t
    foldC(t,s(n)) -> f(foldC(t,n)
                      ,C())
    f(t,x) -> f'(t,g(x))
    f'(triple(a,b,c),C()) ->
      triple(a,b,s(c))
    f'(triple(a,b,c),B()) ->
      f(triple(a,b,c),A())
    f'(triple(a,b,c),A()) ->
      f''(foldB(triple(s(a),0(),c),b))
    f''(triple(a,b,c)) ->
      foldC(triple(a,b,0()),c))