YES
Time: 0.036655
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)}
 DP:
  DP:
   {           foldB#(t, s n) -> foldB#(t, n),
               foldB#(t, s n) -> f#(foldB(t, n), B()),
                     f#(t, x) -> g# x,
                     f#(t, x) -> f'#(t, g x),
               foldC#(t, s n) -> f#(foldC(t, n), C()),
               foldC#(t, s n) -> foldC#(t, n),
    f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b),
    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) -> foldC#(triple(a, b, 0()), c)}
  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)}
  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''# foldB(triple(s a, 0(), c), b))
    (f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b))
    (f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b), foldB#(t, s n) -> f#(foldB(t, n), B()))
    (f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b), foldB#(t, s n) -> foldB#(t, n))
    (foldC#(t, s n) -> foldC#(t, n), foldC#(t, s n) -> foldC#(t, n))
    (foldC#(t, s n) -> foldC#(t, n), foldC#(t, s n) -> f#(foldC(t, n), C()))
    (foldC#(t, s n) -> f#(foldC(t, n), C()), f#(t, x) -> f'#(t, g x))
    (foldC#(t, s n) -> f#(foldC(t, n), C()), 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), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> g# x)
    (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))
    (foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> g# x)
    (foldB#(t, s n) -> f#(foldB(t, n), B()), f#(t, x) -> f'#(t, g x))
    (foldB#(t, s n) -> foldB#(t, n), foldB#(t, s n) -> foldB#(t, n))
    (foldB#(t, s n) -> foldB#(t, n), foldB#(t, s n) -> f#(foldB(t, n), B()))
    (f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c), foldC#(t, s n) -> f#(foldC(t, n), C()))
    (f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c), foldC#(t, s n) -> foldC#(t, n))}
   SCCS (1):
    Scc:
     {           foldB#(t, s n) -> foldB#(t, n),
                 foldB#(t, s n) -> f#(foldB(t, n), B()),
                       f#(t, x) -> f'#(t, g x),
                 foldC#(t, s n) -> f#(foldC(t, n), C()),
                 foldC#(t, s n) -> foldC#(t, n),
      f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b),
      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) -> foldC#(triple(a, b, 0()), c)}
    SCC (9):
     Strict:
      {           foldB#(t, s n) -> foldB#(t, n),
                  foldB#(t, s n) -> f#(foldB(t, n), B()),
                        f#(t, x) -> f'#(t, g x),
                  foldC#(t, s n) -> f#(foldC(t, n), C()),
                  foldC#(t, s n) -> foldC#(t, n),
       f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b),
       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) -> foldC#(triple(a, b, 0()), c)}
     Weak:
     {                   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)}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [triple](x0, x1, x2) = x0 + x1,
       
       [foldB](x0, x1) = x0 + x1,
       
       [f](x0, x1) = x0 + 1,
       
       [foldC](x0, x1) = x0 + x1,
       
       [f'](x0, x1) = x0 + 1,
       
       [g](x0) = 0,
       
       [s](x0) = x0 + 1,
       
       [f''](x0) = x0 + 1,
       
       [A] = 0,
       
       [B] = 0,
       
       [C] = 0,
       
       [0] = 0,
       
       [foldB#](x0, x1) = x0 + x1 + 1,
       
       [f#](x0, x1) = x0 + 1,
       
       [foldC#](x0, x1) = x0 + x1,
       
       [f'#](x0, x1) = x0 + 1,
       
       [f''#](x0) = x0
      Strict:
       f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), 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''# foldB(triple(s a, 0(), c), b)
       1 + 0a + 1b + 1c >= 0 + 0a + 1b + 1c
       f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b)
       1 + 0a + 1b + 1c >= 1 + 0a + 1b + 1c
       foldC#(t, s n) -> foldC#(t, n)
       1 + 1t + 1n >= 0 + 1t + 1n
       foldC#(t, s n) -> f#(foldC(t, n), C())
       1 + 1t + 1n >= 1 + 1t + 1n
       f#(t, x) -> f'#(t, g x)
       1 + 1t + 0x >= 1 + 1t + 0x
       foldB#(t, s n) -> f#(foldB(t, n), B())
       2 + 1t + 1n >= 1 + 1t + 1n
       foldB#(t, s n) -> foldB#(t, n)
       2 + 1t + 1n >= 1 + 1t + 1n
      Weak:
       
     EDG:
      {(f''# triple(a, b, c) -> foldC#(triple(a, b, 0()), c), foldC#(t, s n) -> f#(foldC(t, n), C()))
       (foldC#(t, s n) -> f#(foldC(t, n), C()), 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#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), A()) -> foldB#(triple(s a, 0(), c), b))
       (f#(t, x) -> f'#(t, g x), f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()))}
      SCCS (1):
       Scc:
        {                 f#(t, x) -> f'#(t, g x),
         f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A())}
       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(),
                    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)}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [triple](x0, x1, x2) = x0,
          
          [foldB](x0, x1) = x0 + x1 + 1,
          
          [f](x0, x1) = 0,
          
          [foldC](x0, x1) = x0 + 1,
          
          [f'](x0, x1) = 0,
          
          [g](x0) = x0,
          
          [s](x0) = 1,
          
          [f''](x0) = 0,
          
          [A] = 0,
          
          [B] = 1,
          
          [C] = 1,
          
          [0] = 1,
          
          [f#](x0, x1) = x0,
          
          [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 + 0t + 1x >= 0 + 0t + 1x
         Weak:
          
        EDG:
         {}
         SCCS (0):
          
          Qed