YES
Time: 0.032356
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:
  DP:
   {    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)}
  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)}
  EDG:
   {(foldf#(x, cons(y, z)) -> foldf#(x, z), foldf#(x, cons(y, z)) -> f#(foldf(x, z), y))
    (foldf#(x, cons(y, z)) -> foldf#(x, z), foldf#(x, cons(y, z)) -> foldf#(x, z))
    (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) -> f'#(t, g x))
    (foldf#(x, cons(y, z)) -> f#(foldf(x, z), y), 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), A()) -> foldf#(triple(cons(A(), a), nil(), c), b))
    (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), B()) -> f#(triple(a, b, c), A()))
    (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> 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) -> foldf#(triple(a, b, nil()), c), foldf#(x, cons(y, z)) -> foldf#(x, z))
    (f''# triple(a, b, c) -> foldf#(triple(a, b, nil()), c), foldf#(x, cons(y, z)) -> f#(foldf(x, z), y))}
   SCCS (1):
    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 (7):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [triple](x0, x1, x2) = x0 + x1,
       
       [foldf](x0, x1) = x0 + x1,
       
       [f](x0, x1) = x0 + x1,
       
       [cons](x0, x1) = x0 + x1,
       
       [f'](x0, x1) = x0 + x1,
       
       [g](x0) = x0,
       
       [f''](x0) = x0,
       
       [A] = 1,
       
       [B] = 1,
       
       [C] = 1,
       
       [nil] = 0,
       
       [foldf#](x0, x1) = x0 + x1,
       
       [f#](x0, x1) = x0 + x1,
       
       [f'#](x0, x1) = x0 + x1,
       
       [f''#](x0) = x0
      Strict:
       f''# triple(a, b, c) -> foldf#(triple(a, b, nil()), c)
       0 + 0a + 1b + 1c >= 0 + 0a + 1b + 1c
       f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())
       1 + 0a + 1b + 1c >= 1 + 0a + 1b + 1c
       f'#(triple(a, b, c), A()) -> f''# foldf(triple(cons(A(), a), nil(), c), b)
       1 + 0a + 1b + 1c >= 0 + 0a + 1b + 1c
       f'#(triple(a, b, c), A()) -> foldf#(triple(cons(A(), a), nil(), c), b)
       1 + 0a + 1b + 1c >= 0 + 0a + 1b + 1c
       f#(t, x) -> f'#(t, g x)
       0 + 1x + 1t >= 0 + 1x + 1t
       foldf#(x, cons(y, z)) -> f#(foldf(x, z), y)
       0 + 1x + 1z + 1y >= 0 + 1x + 1z + 1y
       foldf#(x, cons(y, z)) -> foldf#(x, z)
       0 + 1x + 1z + 1y >= 0 + 1x + 1z
      Weak:
       
     EDG:
      {(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)) -> f#(foldf(x, z), y), f#(t, x) -> f'#(t, g x))
       (f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()))
       (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> f'#(t, g x))
       (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))}
      SCCS (2):
       Scc:
        {                 f#(t, x) -> f'#(t, g x),
         f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())}
       Scc:
        {foldf#(x, cons(y, z)) -> foldf#(x, z)}
       SCC (2):
        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:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [triple](x0, x1, x2) = 0,
          
          [foldf](x0, x1) = x0 + 1,
          
          [f](x0, x1) = x0 + 1,
          
          [cons](x0, x1) = 1,
          
          [f'](x0, x1) = 0,
          
          [g](x0) = x0,
          
          [f''](x0) = 0,
          
          [A] = 0,
          
          [B] = 1,
          
          [C] = 1,
          
          [nil] = 1,
          
          [f#](x0, x1) = x0 + x1,
          
          [f'#](x0, x1) = x0
         Strict:
          f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())
          1 + 0a + 0b + 0c >= 0 + 0a + 0b + 0c
          f#(t, x) -> f'#(t, g x)
          0 + 1x + 1t >= 0 + 1x + 0t
         Weak:
          
        EDG:
         {}
         SCCS (0):
          
          Qed
      SCC (1):
       Strict:
        {foldf#(x, cons(y, z)) -> foldf#(x, z)}
       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)}
       SPSC:
        Simple Projection:
         pi(foldf#) = 1
        Strict:
         {}
        Qed