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