MAYBE

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:
 Complexity Transformation Processor:
  strict:
   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)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [f''](x0) = x0 + 1,
     
     [triple](x0, x1, x2) = x0 + x1 + x2 + 1,
     
     [f'](x0, x1) = x0 + x1 + 1,
     
     [f](x0, x1) = x0 + x1,
     
     [cons](x0, x1) = x0 + x1,
     
     [foldf](x0, x1) = x0 + x1,
     
     [nil] = 0,
     
     [C] = 1,
     
     [B] = 0,
     
     [g](x0) = x0,
     
     [A] = 0
    orientation:
     g(A()) = 0 >= 0 = A()
     
     g(B()) = 0 >= 0 = A()
     
     g(B()) = 0 >= 0 = B()
     
     g(C()) = 1 >= 0 = A()
     
     g(C()) = 1 >= 0 = B()
     
     g(C()) = 1 >= 1 = C()
     
     foldf(x,nil()) = x >= x = x
     
     foldf(x,cons(y,z)) = x + y + z >= x + y + z = f(foldf(x,z),y)
     
     f(t,x) = t + x >= t + x + 1 = f'(t,g(x))
     
     f'(triple(a,b,c),C()) = a + b + c + 3 >= a + b + c + 2 = triple(a,b,cons(C(),c))
     
     f'(triple(a,b,c),B()) = a + b + c + 2 >= a + b + c + 1 = f(triple(a,b,c),A())
     
     f'(triple(a,b,c),A()) = a + b + c + 2 >= a + b + c + 2 = f''(foldf(triple(cons(A(),a),nil(),c),b))
     
     f''(triple(a,b,c)) = a + b + c + 2 >= a + b + c + 1 = foldf(triple(a,b,nil()),c)
    problem:
     strict:
      g(A()) -> A()
      g(B()) -> A()
      g(B()) -> 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),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
     weak:
      g(C()) -> A()
      g(C()) -> B()
      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)) -> foldf(triple(a,b,nil()),c)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [f''](x0) = x0 + 1,
       
       [triple](x0, x1, x2) = x0 + x1 + x2,
       
       [f'](x0, x1) = x0 + x1,
       
       [f](x0, x1) = x0 + x1,
       
       [cons](x0, x1) = x0 + x1,
       
       [foldf](x0, x1) = x0 + x1,
       
       [nil] = 1,
       
       [C] = 0,
       
       [B] = 1,
       
       [g](x0) = x0 + 1,
       
       [A] = 1
      orientation:
       g(A()) = 2 >= 1 = A()
       
       g(B()) = 2 >= 1 = A()
       
       g(B()) = 2 >= 1 = B()
       
       g(C()) = 1 >= 0 = C()
       
       foldf(x,nil()) = x + 1 >= x = x
       
       foldf(x,cons(y,z)) = x + y + z >= x + y + z = f(foldf(x,z),y)
       
       f(t,x) = t + x >= t + x + 1 = f'(t,g(x))
       
       f'(triple(a,b,c),A()) = a + b + c + 1 >= a + b + c + 3 = f''(foldf(triple(cons(A(),a),nil(),c),b))
       
       g(C()) = 1 >= 1 = A()
       
       g(C()) = 1 >= 1 = B()
       
       f'(triple(a,b,c),C()) = a + b + c >= a + b + c = triple(a,b,cons(C(),c))
       
       f'(triple(a,b,c),B()) = a + b + c + 1 >= a + b + c + 1 = f(triple(a,b,c),A())
       
       f''(triple(a,b,c)) = a + b + c + 1 >= a + b + c + 1 = foldf(triple(a,b,nil()),c)
      problem:
       strict:
        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))
       weak:
        g(A()) -> A()
        g(B()) -> A()
        g(B()) -> B()
        g(C()) -> C()
        foldf(x,nil()) -> x
        g(C()) -> A()
        g(C()) -> B()
        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)) -> foldf(triple(a,b,nil()),c)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [f''](x0) = x0,
         
         [triple](x0, x1, x2) = x0 + x1 + x2 + 1,
         
         [f'](x0, x1) = x0 + x1 + 1,
         
         [f](x0, x1) = x0 + x1 + 1,
         
         [cons](x0, x1) = x0 + x1,
         
         [foldf](x0, x1) = x0 + x1,
         
         [nil] = 0,
         
         [C] = 0,
         
         [B] = 0,
         
         [g](x0) = x0,
         
         [A] = 0
        orientation:
         foldf(x,cons(y,z)) = x + y + z >= x + y + z + 1 = f(foldf(x,z),y)
         
         f(t,x) = t + x + 1 >= t + x + 1 = f'(t,g(x))
         
         f'(triple(a,b,c),A()) = a + b + c + 2 >= a + b + c + 1 = 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 = C()
         
         foldf(x,nil()) = x >= x = x
         
         g(C()) = 0 >= 0 = A()
         
         g(C()) = 0 >= 0 = B()
         
         f'(triple(a,b,c),C()) = a + b + c + 2 >= a + b + c + 1 = triple(a,b,cons(C(),c))
         
         f'(triple(a,b,c),B()) = a + b + c + 2 >= a + b + c + 2 = f(triple(a,b,c),A())
         
         f''(triple(a,b,c)) = a + b + c + 1 >= a + b + c + 1 = foldf(triple(a,b,nil()),c)
        problem:
         strict:
          foldf(x,cons(y,z)) -> f(foldf(x,z),y)
          f(t,x) -> f'(t,g(x))
         weak:
          f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
          g(A()) -> A()
          g(B()) -> A()
          g(B()) -> B()
          g(C()) -> C()
          foldf(x,nil()) -> x
          g(C()) -> A()
          g(C()) -> B()
          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)) -> foldf(triple(a,b,nil()),c)
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [f''](x0) = x0,
           
           [triple](x0, x1, x2) = x0 + x1 + x2,
           
           [f'](x0, x1) = x0 + x1 + 1,
           
           [f](x0, x1) = x0 + x1,
           
           [cons](x0, x1) = x0 + x1 + 1,
           
           [foldf](x0, x1) = x0 + x1,
           
           [nil] = 0,
           
           [C] = 1,
           
           [B] = 0,
           
           [g](x0) = x0,
           
           [A] = 0
          orientation:
           foldf(x,cons(y,z)) = x + y + z + 1 >= x + y + z = f(foldf(x,z),y)
           
           f(t,x) = t + x >= t + x + 1 = f'(t,g(x))
           
           f'(triple(a,b,c),A()) = a + b + c + 1 >= a + b + c + 1 = 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()) = 1 >= 1 = C()
           
           foldf(x,nil()) = x >= x = x
           
           g(C()) = 1 >= 0 = A()
           
           g(C()) = 1 >= 0 = B()
           
           f'(triple(a,b,c),C()) = a + b + c + 2 >= a + b + c + 2 = triple(a,b,cons(C(),c))
           
           f'(triple(a,b,c),B()) = a + b + c + 1 >= a + b + c = f(triple(a,b,c),A())
           
           f''(triple(a,b,c)) = a + b + c >= a + b + c = foldf(triple(a,b,nil()),c)
          problem:
           strict:
            f(t,x) -> f'(t,g(x))
           weak:
            foldf(x,cons(y,z)) -> f(foldf(x,z),y)
            f'(triple(a,b,c),A()) -> f''(foldf(triple(cons(A(),a),nil(),c),b))
            g(A()) -> A()
            g(B()) -> A()
            g(B()) -> B()
            g(C()) -> C()
            foldf(x,nil()) -> x
            g(C()) -> A()
            g(C()) -> B()
            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)) -> foldf(triple(a,b,nil()),c)
          Open