YES
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),
           fold(t, x, 0()) -> t,
          fold(t, x, s(n)) -> f(fold(t, x, n), x)}
 DP:
  Strict:
   {          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),
            fold#(t, x, s(n)) -> f#(fold(t, x, n), x),
            fold#(t, x, s(n)) -> fold#(t, x, n)}
  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),
            fold(t, x, 0()) -> t,
           fold(t, x, s(n)) -> f(fold(t, x, n), x)}
  EDG:
   {(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)) -> foldB#(t, n), foldB#(t, s(n)) -> f#(foldB(t, n), B()))
    (foldB#(t, s(n)) -> foldB#(t, n), foldB#(t, s(n)) -> foldB#(t, n))
    (f''#(triple(a, b, c)) -> foldC#(triple(a, b, 0()), c), foldC#(t, s(n)) -> foldC#(t, n))
    (f''#(triple(a, b, c)) -> foldC#(triple(a, b, 0()), c), foldC#(t, s(n)) -> f#(foldC(t, n), C()))
    (foldB#(t, s(n)) -> f#(foldB(t, n), B()), f#(t, x) -> f'#(t, g(x)))
    (foldB#(t, s(n)) -> f#(foldB(t, n), B()), 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))
    (fold#(t, x, s(n)) -> fold#(t, x, n), fold#(t, x, s(n)) -> fold#(t, x, n))
    (fold#(t, x, s(n)) -> fold#(t, x, n), fold#(t, x, s(n)) -> f#(fold(t, x, n), x))
    (fold#(t, x, s(n)) -> f#(fold(t, x, n), x), f#(t, x) -> g#(x))
    (fold#(t, x, s(n)) -> f#(fold(t, x, n), x), f#(t, x) -> f'#(t, g(x)))
    (foldC#(t, s(n)) -> f#(foldC(t, n), C()), f#(t, x) -> g#(x))
    (foldC#(t, s(n)) -> f#(foldC(t, n), C()), f#(t, x) -> f'#(t, g(x)))
    (f'#(triple(a, b, c), A()) -> foldB#(triple(s(a), 0(), c), b), foldB#(t, s(n)) -> foldB#(t, n))
    (f'#(triple(a, b, c), A()) -> foldB#(triple(s(a), 0(), c), b), foldB#(t, s(n)) -> f#(foldB(t, n), B()))
    (foldC#(t, s(n)) -> foldC#(t, n), foldC#(t, s(n)) -> f#(foldC(t, n), C()))
    (foldC#(t, s(n)) -> foldC#(t, n), foldC#(t, s(n)) -> foldC#(t, n))
    (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), A()) -> f''#(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:
    Scc:
     {fold#(t, x, s(n)) -> fold#(t, x, n)}
    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:
     Strict:
      {fold#(t, x, s(n)) -> fold#(t, x, n)}
     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),
               fold(t, x, 0()) -> t,
              fold(t, x, s(n)) -> f(fold(t, x, n), x)}
     SPSC:
      Simple Projection:
       pi(fold#) = 2
      Strict:
       {}
      Qed
    SCC:
     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),
               fold(t, x, 0()) -> t,
              fold(t, x, s(n)) -> f(fold(t, x, n), x)}
     POLY:
      Argument Filtering:
       pi(fold) = 1, pi(f''#) = 0, pi(f'') = 0, pi(triple) = 2, pi(f'#) = 0, pi(f') = [0,1], pi(foldC#) = [0,1], pi(foldC) = [0,1], pi(s) = [0], pi(f#) = 0, pi(f) = [0,1], pi(0) = [], pi(foldB#) = 0, pi(foldB) = 0, pi(C) = [], pi(B) = [], pi(g) = 0, pi(A) = []
      Usable Rules:
       {}
      Interpretation:
       [foldC#](x0, x1) = x0 + x1,
       [foldC](x0, x1) = x0 + x1,
       [s](x0) = x0 + 1,
       [0] = 0
      Strict:
       {          foldB#(t, s(n)) -> foldB#(t, n),
                  foldB#(t, s(n)) -> f#(foldB(t, n), 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()) -> 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),
                 fold(t, x, 0()) -> t,
                fold(t, x, s(n)) -> f(fold(t, x, n), x)}
      EDG:
       {(foldB#(t, s(n)) -> foldB#(t, n), foldB#(t, s(n)) -> f#(foldB(t, n), B()))
        (foldB#(t, s(n)) -> foldB#(t, n), foldB#(t, s(n)) -> foldB#(t, n))
        (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))
        (f'#(triple(a, b, c), B()) -> f#(triple(a, b, c), A()), f#(t, x) -> f'#(t, g(x)))
        (foldB#(t, s(n)) -> f#(foldB(t, n), B()), f#(t, x) -> f'#(t, 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))}
       SCCS:
        Scc:
         {          foldB#(t, s(n)) -> foldB#(t, n),
                    foldB#(t, s(n)) -> f#(foldB(t, n), 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), B()) -> f#(triple(a, b, c), A())}
        SCC:
         Strict:
          {          foldB#(t, s(n)) -> foldB#(t, n),
                     foldB#(t, s(n)) -> f#(foldB(t, n), 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), 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),
                   fold(t, x, 0()) -> t,
                  fold(t, x, s(n)) -> f(fold(t, x, n), x)}
         POLY:
          Argument Filtering:
           pi(fold) = [], pi(f'') = 0, pi(triple) = 1, pi(f'#) = 0, pi(f') = 0, pi(foldC) = 0, pi(s) = [0], pi(f#) = 0, pi(f) = [0,1], pi(0) = [], pi(foldB#) = [0,1], pi(foldB) = [0,1], pi(C) = [], pi(B) = [], pi(g) = [], pi(A) = []
          Usable Rules:
           {}
          Interpretation:
           [foldB#](x0, x1) = x0 + x1,
           [foldB](x0, x1) = x0 + x1,
           [s](x0) = x0 + 1,
           [0] = 0
          Strict:
           {                 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), 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),
                     fold(t, x, 0()) -> t,
                    fold(t, x, s(n)) -> f(fold(t, x, n), x)}
          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()) -> foldB#(triple(s(a), 0(), c), b))
            (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(),
                         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),
                       fold(t, x, 0()) -> t,
                      fold(t, x, s(n)) -> f(fold(t, x, n), x)}
             POLY:
              Argument Filtering:
               pi(fold) = [], pi(f'') = [], pi(triple) = [], pi(f'#) = 1, pi(f') = [], pi(foldC) = [], pi(s) = [], pi(f#) = 1, pi(f) = [], pi(0) = [], pi(foldB) = [], 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(),
                           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),
                         fold(t, x, 0()) -> t,
                        fold(t, x, s(n)) -> f(fold(t, x, n), x)}
              EDG:
               {}
               SCCS:
                
                Qed