YES

Problem:
 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),C()) -> triple(a,b,cons(C(),c))
 f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
 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)

Proof:
 DP Processor:
  DPs:
   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),B()) -> f#(triple(a,b,c),A())
   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)
  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),C()) -> triple(a,b,cons(C(),c))
   f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
   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)
  TDG Processor:
   DPs:
    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),B()) -> f#(triple(a,b,c),A())
    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)
   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),C()) -> triple(a,b,cons(C(),c))
    f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
    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)
   graph:
    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)
    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''#(foldf(triple(cons(A(),a),nil(),c),b)) ->
    f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
    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()) -> 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#(t,x) -> f'#(t,g(x)) ->
    f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
    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)
    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)
   Restore Modifier:
    DPs:
     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),B()) -> f#(triple(a,b,c),A())
     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)
    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),C()) -> triple(a,b,cons(C(),c))
     f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
     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)
    SCC Processor:
     #sccs: 1
     #rules: 7
     #arcs: 14/64
     DPs:
      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'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
      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))
     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),C()) -> triple(a,b,cons(C(),c))
      f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
      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)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [f''#](x0) = x0,
       
       [f'#](x0, x1) = x0,
       
       [f#](x0, x1) = x0 + x1,
       
       [foldf#](x0, x1) = x0 + x1,
       
       [f''](x0) = x0,
       
       [triple](x0, x1, x2) = x1 + x2,
       
       [f'](x0, x1) = x0 + 1,
       
       [f](x0, x1) = x0 + 1,
       
       [cons](x0, x1) = x0 + x1 + 1,
       
       [foldf](x0, x1) = x0 + x1,
       
       [nil] = 0,
       
       [C] = 0,
       
       [B] = 0,
       
       [g](x0) = 0,
       
       [A] = 0
      orientation:
       f''#(triple(a,b,c)) = b + c >= b + c = foldf#(triple(a,b,nil()),c)
       
       foldf#(x,cons(y,z)) = x + y + z + 1 >= x + z = foldf#(x,z)
       
       foldf#(x,cons(y,z)) = x + y + z + 1 >= x + y + z = f#(foldf(x,z),y)
       
       f#(t,x) = t + x >= t = f'#(t,g(x))
       
       f'#(triple(a,b,c),B()) = b + c >= b + c = f#(triple(a,b,c),A())
       
       f'#(triple(a,b,c),A()) = b + c >= b + c = foldf#(triple(cons(A(),a),nil(),c),b)
       
       f'#(triple(a,b,c),A()) = b + c >= b + c = f''#(foldf(triple(cons(A(),a),nil(),c),b))
       
       g(A()) = 0 >= 0 = A()
       
       g(B()) = 0 >= 0 = A()
       
       g(B()) = 0 >= 0 = B()
       
       g(C()) = 0 >= 0 = A()
       
       g(C()) = 0 >= 0 = B()
       
       g(C()) = 0 >= 0 = C()
       
       foldf(x,nil()) = x >= x = x
       
       foldf(x,cons(y,z)) = x + y + z + 1 >= x + z + 1 = f(foldf(x,z),y)
       
       f(t,x) = t + 1 >= t + 1 = f'(t,g(x))
       
       f'(triple(a,b,c),C()) = b + c + 1 >= b + c + 1 = triple(a,b,cons(C(),c))
       
       f'(triple(a,b,c),B()) = b + c + 1 >= b + c + 1 = f(triple(a,b,c),A())
       
       f'(triple(a,b,c),A()) = b + c + 1 >= b + c = f''(foldf(triple(cons(A(),a),nil(),c),b))
       
       f''(triple(a,b,c)) = b + c >= b + c = foldf(triple(a,b,nil()),c)
      problem:
       DPs:
        f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
        f#(t,x) -> f'#(t,g(x))
        f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
        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))
       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),C()) -> triple(a,b,cons(C(),c))
        f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
        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)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [f''#](x0) = x0,
        
        [f'#](x0, x1) = x1 + 1,
        
        [f#](x0, x1) = x1 + 1,
        
        [foldf#](x0, x1) = 0,
        
        [f''](x0) = 1,
        
        [triple](x0, x1, x2) = 0,
        
        [f'](x0, x1) = 1,
        
        [f](x0, x1) = 1,
        
        [cons](x0, x1) = 0,
        
        [foldf](x0, x1) = x0 + 1,
        
        [nil] = 0,
        
        [C] = 1,
        
        [B] = 1,
        
        [g](x0) = x0,
        
        [A] = 1
       orientation:
        f''#(triple(a,b,c)) = 0 >= 0 = foldf#(triple(a,b,nil()),c)
        
        f#(t,x) = x + 1 >= x + 1 = f'#(t,g(x))
        
        f'#(triple(a,b,c),B()) = 2 >= 2 = f#(triple(a,b,c),A())
        
        f'#(triple(a,b,c),A()) = 2 >= 0 = foldf#(triple(cons(A(),a),nil(),c),b)
        
        f'#(triple(a,b,c),A()) = 2 >= 1 = f''#(foldf(triple(cons(A(),a),nil(),c),b))
        
        g(A()) = 1 >= 1 = A()
        
        g(B()) = 1 >= 1 = A()
        
        g(B()) = 1 >= 1 = B()
        
        g(C()) = 1 >= 1 = A()
        
        g(C()) = 1 >= 1 = B()
        
        g(C()) = 1 >= 1 = C()
        
        foldf(x,nil()) = x + 1 >= x = x
        
        foldf(x,cons(y,z)) = x + 1 >= 1 = f(foldf(x,z),y)
        
        f(t,x) = 1 >= 1 = f'(t,g(x))
        
        f'(triple(a,b,c),C()) = 1 >= 0 = triple(a,b,cons(C(),c))
        
        f'(triple(a,b,c),B()) = 1 >= 1 = f(triple(a,b,c),A())
        
        f'(triple(a,b,c),A()) = 1 >= 1 = f''(foldf(triple(cons(A(),a),nil(),c),b))
        
        f''(triple(a,b,c)) = 1 >= 1 = foldf(triple(a,b,nil()),c)
       problem:
        DPs:
         f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
         f#(t,x) -> f'#(t,g(x))
         f'#(triple(a,b,c),B()) -> f#(triple(a,b,c),A())
        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),C()) -> triple(a,b,cons(C(),c))
         f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
         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)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [f''#](x0) = 0,
         
         [f'#](x0, x1) = x1,
         
         [f#](x0, x1) = x1,
         
         [foldf#](x0, x1) = 0,
         
         [f''](x0) = 0,
         
         [triple](x0, x1, x2) = 0,
         
         [f'](x0, x1) = x0,
         
         [f](x0, x1) = x0,
         
         [cons](x0, x1) = 1,
         
         [foldf](x0, x1) = x0,
         
         [nil] = 0,
         
         [C] = 1,
         
         [B] = 1,
         
         [g](x0) = x0,
         
         [A] = 0
        orientation:
         f''#(triple(a,b,c)) = 0 >= 0 = foldf#(triple(a,b,nil()),c)
         
         f#(t,x) = x >= x = f'#(t,g(x))
         
         f'#(triple(a,b,c),B()) = 1 >= 0 = f#(triple(a,b,c),A())
         
         g(A()) = 0 >= 0 = A()
         
         g(B()) = 1 >= 0 = A()
         
         g(B()) = 1 >= 1 = B()
         
         g(C()) = 1 >= 0 = A()
         
         g(C()) = 1 >= 1 = B()
         
         g(C()) = 1 >= 1 = C()
         
         foldf(x,nil()) = x >= x = x
         
         foldf(x,cons(y,z)) = x >= x = f(foldf(x,z),y)
         
         f(t,x) = t >= t = f'(t,g(x))
         
         f'(triple(a,b,c),C()) = 0 >= 0 = triple(a,b,cons(C(),c))
         
         f'(triple(a,b,c),B()) = 0 >= 0 = f(triple(a,b,c),A())
         
         f'(triple(a,b,c),A()) = 0 >= 0 = f''(foldf(triple(cons(A(),a),nil(),c),b))
         
         f''(triple(a,b,c)) = 0 >= 0 = foldf(triple(a,b,nil()),c)
        problem:
         DPs:
          f''#(triple(a,b,c)) -> foldf#(triple(a,b,nil()),c)
          f#(t,x) -> f'#(t,g(x))
         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),C()) -> triple(a,b,cons(C(),c))
          f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
          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)
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [f''#](x0) = 0,
          
          [f'#](x0, x1) = 0,
          
          [f#](x0, x1) = 1,
          
          [foldf#](x0, x1) = 0,
          
          [f''](x0) = 0,
          
          [triple](x0, x1, x2) = 0,
          
          [f'](x0, x1) = x0,
          
          [f](x0, x1) = x0,
          
          [cons](x0, x1) = 0,
          
          [foldf](x0, x1) = x0,
          
          [nil] = 0,
          
          [C] = 0,
          
          [B] = 0,
          
          [g](x0) = 0,
          
          [A] = 0
         orientation:
          f''#(triple(a,b,c)) = 0 >= 0 = foldf#(triple(a,b,nil()),c)
          
          f#(t,x) = 1 >= 0 = f'#(t,g(x))
          
          g(A()) = 0 >= 0 = A()
          
          g(B()) = 0 >= 0 = A()
          
          g(B()) = 0 >= 0 = B()
          
          g(C()) = 0 >= 0 = A()
          
          g(C()) = 0 >= 0 = B()
          
          g(C()) = 0 >= 0 = C()
          
          foldf(x,nil()) = x >= x = x
          
          foldf(x,cons(y,z)) = x >= x = f(foldf(x,z),y)
          
          f(t,x) = t >= t = f'(t,g(x))
          
          f'(triple(a,b,c),C()) = 0 >= 0 = triple(a,b,cons(C(),c))
          
          f'(triple(a,b,c),B()) = 0 >= 0 = f(triple(a,b,c),A())
          
          f'(triple(a,b,c),A()) = 0 >= 0 = f''(foldf(triple(cons(A(),a),nil(),c),b))
          
          f''(triple(a,b,c)) = 0 >= 0 = foldf(triple(a,b,nil()),c)
         problem:
          DPs:
           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),C()) -> triple(a,b,cons(C(),c))
           f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
           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)
         Matrix Interpretation Processor:
          dimension: 1
          interpretation:
           [f''#](x0) = 1,
           
           [foldf#](x0, x1) = 0,
           
           [f''](x0) = 0,
           
           [triple](x0, x1, x2) = 0,
           
           [f'](x0, x1) = x0,
           
           [f](x0, x1) = x0,
           
           [cons](x0, x1) = 0,
           
           [foldf](x0, x1) = x0,
           
           [nil] = 0,
           
           [C] = 0,
           
           [B] = 0,
           
           [g](x0) = 0,
           
           [A] = 0
          orientation:
           f''#(triple(a,b,c)) = 1 >= 0 = foldf#(triple(a,b,nil()),c)
           
           g(A()) = 0 >= 0 = A()
           
           g(B()) = 0 >= 0 = A()
           
           g(B()) = 0 >= 0 = B()
           
           g(C()) = 0 >= 0 = A()
           
           g(C()) = 0 >= 0 = B()
           
           g(C()) = 0 >= 0 = C()
           
           foldf(x,nil()) = x >= x = x
           
           foldf(x,cons(y,z)) = x >= x = f(foldf(x,z),y)
           
           f(t,x) = t >= t = f'(t,g(x))
           
           f'(triple(a,b,c),C()) = 0 >= 0 = triple(a,b,cons(C(),c))
           
           f'(triple(a,b,c),B()) = 0 >= 0 = f(triple(a,b,c),A())
           
           f'(triple(a,b,c),A()) = 0 >= 0 = f''(foldf(triple(cons(A(),a),nil(),c),b))
           
           f''(triple(a,b,c)) = 0 >= 0 = foldf(triple(a,b,nil()),c)
          problem:
           DPs:
            
           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),C()) -> triple(a,b,cons(C(),c))
            f'(triple(a,b,c),B()) -> f(triple(a,b,c),A())
            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)
          Qed