MAYBE
MAYBE
TRS:
 {
                    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()),
                   f(t, x) -> f'(t, g(x)),
             foldC(t, 0()) -> t,
            foldC(t, s(n)) -> f(foldC(t, n), C()),
  f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b)),
  f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
  f'(triple(a, b, c), C()) -> triple(a, b, s(c)),
      f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
                      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()),
                     f(t, x) -> f'(t, g(x)),
               foldC(t, 0()) -> t,
              foldC(t, s(n)) -> f(foldC(t, n), C()),
    f'(triple(a, b, c), A()) -> f''(foldB(triple(s(a), 0(), c), b)),
    f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
    f'(triple(a, b, c), C()) -> triple(a, b, s(c)),
        f''(triple(a, b, c)) -> foldC(triple(a, b, 0()), c)
   }
  Fail