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)
  EDG 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)) -> foldf#(x,z)
    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),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),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)) -> foldf#(x,z)
    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#(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()) -> 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))
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y) ->
    f#(t,x) -> g#(x)
    foldf#(x,cons(y,z)) -> f#(foldf(x,z),y) ->
    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)
   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)) -> 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),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
     foldf#(x,cons(y,z)) -> foldf#(x,z)
     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) = x0,
      
      [f'#](x0, x1) = x0,
      
      [f#](x0, x1) = x0,
      
      [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) = 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 + z + 1 >= x + z = f#(foldf(x,z),y)
      
      f#(t,x) = t >= t = f'#(t,g(x))
      
      f'#(triple(a,b,c),A()) = b + c >= b + c = f''#(foldf(triple(cons(A(),a),nil(),c),b))
      
      f'#(triple(a,b,c),A()) = b + c >= b + c = foldf#(triple(cons(A(),a),nil(),c),b)
      
      foldf#(x,cons(y,z)) = x + z + 1 >= x + z = foldf#(x,z)
      
      f'#(triple(a,b,c),B()) = b + c >= b + c = f#(triple(a,b,c),A())
      
      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 + 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),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
       f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
       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) = x0 + 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) = x0,
       
       [foldf](x0, x1) = x0 + 1,
       
       [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) = t + x + 1 >= x = f'#(t,g(x))
       
       f'#(triple(a,b,c),A()) = 0 >= 0 = f''#(foldf(triple(cons(A(),a),nil(),c),b))
       
       f'#(triple(a,b,c),A()) = 0 >= 0 = foldf#(triple(cons(A(),a),nil(),c),b)
       
       f'#(triple(a,b,c),B()) = 1 >= 1 = 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 + 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'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
        f'#(triple(a,b,c),A()) -> foldf#(triple(cons(A(),a),nil(),c),b)
        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) = 1,
        
        [f'#](x0, x1) = x1,
        
        [f#](x0, x1) = 0,
        
        [foldf#](x0, x1) = 1,
        
        [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] = 1,
        
        [B] = 1,
        
        [g](x0) = 1,
        
        [A] = 1
       orientation:
        f''#(triple(a,b,c)) = 1 >= 1 = foldf#(triple(a,b,nil()),c)
        
        f'#(triple(a,b,c),A()) = 1 >= 1 = f''#(foldf(triple(cons(A(),a),nil(),c),b))
        
        f'#(triple(a,b,c),A()) = 1 >= 1 = foldf#(triple(cons(A(),a),nil(),c),b)
        
        f'#(triple(a,b,c),B()) = 1 >= 0 = f#(triple(a,b,c),A())
        
        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 >= 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'#(triple(a,b,c),A()) -> f''#(foldf(triple(cons(A(),a),nil(),c),b))
         f'#(triple(a,b,c),A()) -> 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) = 1,
         
         [foldf#](x0, x1) = 0,
         
         [f''](x0) = 1,
         
         [triple](x0, x1, x2) = 0,
         
         [f'](x0, x1) = x1,
         
         [f](x0, x1) = 1,
         
         [cons](x0, x1) = 0,
         
         [foldf](x0, x1) = x0 + 1,
         
         [nil] = 0,
         
         [C] = 0,
         
         [B] = 1,
         
         [g](x0) = 1,
         
         [A] = 1
        orientation:
         f''#(triple(a,b,c)) = 0 >= 0 = foldf#(triple(a,b,nil()),c)
         
         f'#(triple(a,b,c),A()) = 1 >= 1 = f''#(foldf(triple(cons(A(),a),nil(),c),b))
         
         f'#(triple(a,b,c),A()) = 1 >= 0 = 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 >= 0 = 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()) = 0 >= 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'#(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) = 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'#(triple(a,b,c),A()) = 1 >= 0 = 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 >= 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)
         Subterm Criterion Processor:
          simple projection:
           pi(foldf#) = 1
           pi(f''#) = 0
          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