Problem:
 average(s(x),y) -> average(x,s(y))
 average(x,s(s(s(y)))) -> s(average(s(x),y))
 average(0(),0()) -> 0()
 average(0(),s(0())) -> 0()
 average(0(),s(s(0()))) -> s(0())

Proof:
 Complexity Transformation Processor:
  strict:
   average(s(x),y) -> average(x,s(y))
   average(x,s(s(s(y)))) -> s(average(s(x),y))
   average(0(),0()) -> 0()
   average(0(),s(0())) -> 0()
   average(0(),s(s(0()))) -> s(0())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [0] = 0,
     
     [average](x0, x1) = x0 + x1 + 11,
     
     [s](x0) = x0
    orientation:
     average(s(x),y) = x + y + 11 >= x + y + 11 = average(x,s(y))
     
     average(x,s(s(s(y)))) = x + y + 11 >= x + y + 11 = s(average(s(x),y))
     
     average(0(),0()) = 11 >= 0 = 0()
     
     average(0(),s(0())) = 11 >= 0 = 0()
     
     average(0(),s(s(0()))) = 11 >= 0 = s(0())
    problem:
     strict:
      average(s(x),y) -> average(x,s(y))
      average(x,s(s(s(y)))) -> s(average(s(x),y))
     weak:
      average(0(),0()) -> 0()
      average(0(),s(0())) -> 0()
      average(0(),s(s(0()))) -> s(0())
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [0] = 0,
       
       [average](x0, x1) = x0 + x1,
       
       [s](x0) = x0 + 9
      orientation:
       average(s(x),y) = x + y + 9 >= x + y + 9 = average(x,s(y))
       
       average(x,s(s(s(y)))) = x + y + 27 >= x + y + 18 = s(average(s(x),y))
       
       average(0(),0()) = 0 >= 0 = 0()
       
       average(0(),s(0())) = 9 >= 0 = 0()
       
       average(0(),s(s(0()))) = 18 >= 9 = s(0())
      problem:
       strict:
        average(s(x),y) -> average(x,s(y))
       weak:
        average(x,s(s(s(y)))) -> s(average(s(x),y))
        average(0(),0()) -> 0()
        average(0(),s(0())) -> 0()
        average(0(),s(s(0()))) -> s(0())
      Matrix Interpretation Processor:
       dimension: 3
       max_matrix:
        [1 0 1]
        [0 0 0]
        [0 0 1]
        interpretation:
               [0]
         [0] = [0]
               [0],
         
                             [1 0 1]     [1 0 0]  
         [average](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                             [0 0 1]     [0 0 1]  ,
         
                   [1 0 0]     [1]
         [s](x0) = [0 0 0]x0 + [0]
                   [0 0 1]     [1]
        orientation:
                           [1 0 1]    [1 0 0]    [2]    [1 0 1]    [1 0 0]    [1]                  
         average(s(x),y) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = average(x,s(y))
                           [0 0 1]    [0 0 1]    [1]    [0 0 1]    [0 0 1]    [1]                  
         
                                 [1 0 1]    [1 0 0]    [3]    [1 0 1]    [1 0 0]    [3]                     
         average(x,s(s(s(y)))) = [0 0 0]x + [0 0 0]y + [0] >= [0 0 0]x + [0 0 0]y + [0] = s(average(s(x),y))
                                 [0 0 1]    [0 0 1]    [3]    [0 0 1]    [0 0 1]    [2]                     
         
                            [0]    [0]      
         average(0(),0()) = [0] >= [0] = 0()
                            [0]    [0]      
         
                               [1]    [0]      
         average(0(),s(0())) = [0] >= [0] = 0()
                               [1]    [0]      
         
                                  [2]    [1]         
         average(0(),s(s(0()))) = [0] >= [0] = s(0())
                                  [2]    [1]         
        problem:
         strict:
          
         weak:
          average(s(x),y) -> average(x,s(y))
          average(x,s(s(s(y)))) -> s(average(s(x),y))
          average(0(),0()) -> 0()
          average(0(),s(0())) -> 0()
          average(0(),s(s(0()))) -> s(0())
        Qed