YES
TRS:
 {                  g(A()) -> A(),
                    g(B()) -> A(),
                    g(B()) -> B(),
                    g(C()) -> A(),
                    g(C()) -> B(),
                    g(C()) -> C(),
           foldf(x, nil()) -> x,
      foldf(x, cons(y, z)) -> f(foldf(x, z), y),
                   f(t, x) -> f'(t, g(x)),
  f'(triple(a, b, c), A()) -> f''(foldf(triple(cons(A(), a), nil(), c), b)),
  f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
  f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
      f''(triple(a, b, c)) -> foldf(triple(a, b, nil()), c)}
 DP:
  Strict:
   {    foldf#(x, cons(y, z)) -> foldf#(x, z),
        foldf#(x, cons(y, z)) -> f#(foldf(x, z), y),
                     f#(t, x) -> g#(x),
                     f#(t, x) -> f'#(t, g(x)),
    f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b),
    f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)),
    f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()),
        f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c)}
  Weak:
  {                  g(A()) -> A(),
                     g(B()) -> A(),
                     g(B()) -> B(),
                     g(C()) -> A(),
                     g(C()) -> B(),
                     g(C()) -> C(),
            foldf(x, nil()) -> x,
       foldf(x, cons(y, z)) -> f(foldf(x, z), y),
                    f(t, x) -> f'(t, g(x)),
   f'(triple(a, b, c), A()) -> f''(foldf(triple(cons(A(), a), nil(), c), b)),
   f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
   f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
       f''(triple(a, b, c)) -> foldf(triple(a, b, nil()), c)}
  EDG:
   {(f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> f'#(t, g(x)))
    (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> g#(x))
    (f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b), foldf#(x, cons(y, z)) -> f#(foldf(x, z), y))
    (f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b), foldf#(x, cons(y, z)) -> foldf#(x, z))
    (f#(t, x) -> f'#(t, g(x)), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()))
    (f#(t, x) -> f'#(t, g(x)), f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)))
    (f#(t, x) -> f'#(t, g(x)), f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b))
    (f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c), foldf#(x, cons(y, z)) -> f#(foldf(x, z), y))
    (f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c), foldf#(x, cons(y, z)) -> foldf#(x, z))
    (foldf#(x, cons(y, z)) -> foldf#(x, z), foldf#(x, cons(y, z)) -> foldf#(x, z))
    (foldf#(x, cons(y, z)) -> foldf#(x, z), foldf#(x, cons(y, z)) -> f#(foldf(x, z), y))
    (f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)), f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c))
    (foldf#(x, cons(y, z)) -> f#(foldf(x, z), y), f#(t, x) -> g#(x))
    (foldf#(x, cons(y, z)) -> f#(foldf(x, z), y), f#(t, x) -> f'#(t, g(x)))}
   SCCS:
    Scc:
     {    foldf#(x, cons(y, z)) -> foldf#(x, z),
          foldf#(x, cons(y, z)) -> f#(foldf(x, z), y),
                       f#(t, x) -> f'#(t, g(x)),
      f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b),
      f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)),
      f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()),
          f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c)}
    SCC:
     Strict:
      {    foldf#(x, cons(y, z)) -> foldf#(x, z),
           foldf#(x, cons(y, z)) -> f#(foldf(x, z), y),
                        f#(t, x) -> f'#(t, g(x)),
       f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b),
       f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)),
       f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()),
           f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c)}
     Weak:
     {                  g(A()) -> A(),
                        g(B()) -> A(),
                        g(B()) -> B(),
                        g(C()) -> A(),
                        g(C()) -> B(),
                        g(C()) -> C(),
               foldf(x, nil()) -> x,
          foldf(x, cons(y, z)) -> f(foldf(x, z), y),
                       f(t, x) -> f'(t, g(x)),
      f'(triple(a, b, c), A()) -> f''(foldf(triple(cons(A(), a), nil(), c), b)),
      f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
      f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
          f''(triple(a, b, c)) -> foldf(triple(a, b, nil()), c)}
     POLY:
      Argument Filtering:
       pi(f''#) = 0, pi(f'') = 0, pi(triple) = [1,2], pi(f'#) = 0, pi(f') = [0], pi(cons) = [0,1], pi(f#) = 0, pi(f) = [0], pi(nil) = [], pi(foldf#) = [0,1], pi(foldf) = [0,1], pi(C) = [], pi(B) = [], pi(g) = [], pi(A) = []
      Usable Rules:
       {}
      Interpretation:
       [foldf#](x0, x1) = x0 + x1,
       [triple](x0, x1) = x0 + x1,
       [cons](x0, x1) = x0 + x1 + 1,
       [foldf](x0, x1) = x0 + x1,
       [nil] = 0
      Strict:
       {                 f#(t, x) -> f'#(t, g(x)),
        f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b),
        f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)),
        f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()),
            f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c)}
      Weak:
       {                  g(A()) -> A(),
                          g(B()) -> A(),
                          g(B()) -> B(),
                          g(C()) -> A(),
                          g(C()) -> B(),
                          g(C()) -> C(),
                 foldf(x, nil()) -> x,
            foldf(x, cons(y, z)) -> f(foldf(x, z), y),
                         f(t, x) -> f'(t, g(x)),
        f'(triple(a, b, c), A()) -> f''(foldf(triple(cons(A(), a), nil(), c), b)),
        f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
        f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
            f''(triple(a, b, c)) -> foldf(triple(a, b, nil()), c)}
      EDG:
       {(f#(t, x) -> f'#(t, g(x)), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()))
        (f#(t, x) -> f'#(t, g(x)), f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)))
        (f#(t, x) -> f'#(t, g(x)), f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b))
        (f'#(triple(a, b, c), A()) -> f''#(foldf(triple(cons(A(), a), nil(), c), b)), f''#(triple(a, b, c)) -> foldf#(triple(a, b, nil()), c))
        (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> f'#(t, g(x)))}
       SCCS:
        Scc:
         {                 f#(t, x) -> f'#(t, g(x)),
          f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())}
        SCC:
         Strict:
          {                 f#(t, x) -> f'#(t, g(x)),
           f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())}
         Weak:
         {                  g(A()) -> A(),
                            g(B()) -> A(),
                            g(B()) -> B(),
                            g(C()) -> A(),
                            g(C()) -> B(),
                            g(C()) -> C(),
                   foldf(x, nil()) -> x,
              foldf(x, cons(y, z)) -> f(foldf(x, z), y),
                           f(t, x) -> f'(t, g(x)),
          f'(triple(a, b, c), A()) -> f''(foldf(triple(cons(A(), a), nil(), c), b)),
          f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
          f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
              f''(triple(a, b, c)) -> foldf(triple(a, b, nil()), c)}
         POLY:
          Argument Filtering:
           pi(f'') = [], pi(triple) = [], pi(f'#) = 1, pi(f') = [], pi(cons) = [], pi(f#) = 1, pi(f) = [], pi(nil) = [], pi(foldf) = [], pi(C) = [], pi(B) = [], pi(g) = 0, pi(A) = []
          Usable Rules:
           {}
          Interpretation:
           [B] = 1,
           [A] = 0
          Strict:
           {f#(t, x) -> f'#(t, g(x))}
          Weak:
           {                  g(A()) -> A(),
                              g(B()) -> A(),
                              g(B()) -> B(),
                              g(C()) -> A(),
                              g(C()) -> B(),
                              g(C()) -> C(),
                     foldf(x, nil()) -> x,
                foldf(x, cons(y, z)) -> f(foldf(x, z), y),
                             f(t, x) -> f'(t, g(x)),
            f'(triple(a, b, c), A()) -> f''(foldf(triple(cons(A(), a), nil(), c), b)),
            f'(triple(a, b, c), B()) -> f(triple(a, b, c), A()),
            f'(triple(a, b, c), C()) -> triple(a, b, cons(C(), c)),
                f''(triple(a, b, c)) -> foldf(triple(a, b, nil()), c)}
          EDG:
           {}
           SCCS:
            
            Qed